diff --git a/Archive/Imo/Imo1960Q1.lean b/Archive/Imo/Imo1960Q1.lean index 5b6a4a08aea0e..37d6fa2534f39 100644 --- a/Archive/Imo/Imo1960Q1.lean +++ b/Archive/Imo/Imo1960Q1.lean @@ -95,7 +95,8 @@ theorem right_direction {n : ℕ} : ProblemPredicate n → SolutionPredicate n : have := searchUpTo_start iterate 82 replace := - searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num) + searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num1; rfl) + (by norm_num <;> decide) exact searchUpTo_end this #align imo1960_q1.right_direction Imo1960Q1.right_direction diff --git a/Archive/Imo/Imo1962Q1.lean b/Archive/Imo/Imo1962Q1.lean index 951ab2d688130..bb3a51932bb05 100644 --- a/Archive/Imo/Imo1962Q1.lean +++ b/Archive/Imo/Imo1962Q1.lean @@ -132,6 +132,7 @@ Now we combine these cases to show that 153846 is the smallest solution. theorem satisfied_by_153846 : ProblemPredicate 153846 := by norm_num [ProblemPredicate] + decide #align imo1962_q1.satisfied_by_153846 Imo1962Q1.satisfied_by_153846 theorem no_smaller_solutions (n : ℕ) (h1 : ProblemPredicate n) : n ≥ 153846 := by diff --git a/Archive/Imo/Imo1964Q1.lean b/Archive/Imo/Imo1964Q1.lean index 0811661468c43..d0376117a076c 100644 --- a/Archive/Imo/Imo1964Q1.lean +++ b/Archive/Imo/Imo1964Q1.lean @@ -34,7 +34,7 @@ theorem two_pow_mod_seven (n : ℕ) : 2 ^ n ≡ 2 ^ (n % 3) [MOD 7] := let t := n % 3 calc 2 ^ n = 2 ^ (3 * (n / 3) + t) := by rw [Nat.div_add_mod] _ = (2 ^ 3) ^ (n / 3) * 2 ^ t := by rw [pow_add, pow_mul] - _ ≡ 1 ^ (n / 3) * 2 ^ t [MOD 7] := by gcongr; norm_num + _ ≡ 1 ^ (n / 3) * 2 ^ t [MOD 7] := by gcongr; decide _ = 2 ^ t := by ring /-! @@ -68,5 +68,5 @@ theorem imo1964_q1b (n : ℕ) : ¬7 ∣ 2 ^ n + 1 := by have H : 2 ^ t + 1 ≡ 0 [MOD 7] · calc 2 ^ t + 1 ≡ 2 ^ n + 1 [MOD 7 ] := by gcongr ?_ + 1; exact (two_pow_mod_seven n).symm _ ≡ 0 [MOD 7] := h.modEq_zero_nat - interval_cases t <;> norm_num at H + interval_cases t <;> contradiction #align imo1964_q1b imo1964_q1b diff --git a/Archive/Imo/Imo1981Q3.lean b/Archive/Imo/Imo1981Q3.lean index 5b0765b4a9cf9..1a136a674c3ed 100644 --- a/Archive/Imo/Imo1981Q3.lean +++ b/Archive/Imo/Imo1981Q3.lean @@ -129,7 +129,7 @@ theorem imp_fib {n : ℕ} : ∀ m : ℕ, NatPredicate N m n → ∃ k : ℕ, m = obtain (rfl : 1 = n) | (h4 : 1 < n) := (succ_le_iff.mpr h2.n_pos).eq_or_lt · use 1 have h5 : 1 ≤ m := succ_le_iff.mpr h2.m_pos - simpa [fib_one, fib_two] using (h3.antisymm h5 : m = 1) + simpa [fib_one, fib_two, (by decide : 1 + 1 = 2)] using (h3.antisymm h5 : m = 1) · obtain (rfl : m = n) | (h6 : m < n) := h3.eq_or_lt · exact absurd h2.eq_imp_1 (Nat.ne_of_gt h4) · have h7 : NatPredicate N (n - m) m := h2.reduction h4 @@ -205,5 +205,7 @@ theorem imo1981_q3 : IsGreatest (specifiedSet 1981) 3524578 := by have := fun h => @solution_greatest 1981 16 h 3524578 norm_num at this apply this - norm_num [ProblemPredicate_iff] + · decide + · decide + · norm_num [ProblemPredicate_iff]; decide #align imo1981_q3 imo1981_q3 diff --git a/Archive/Imo/Imo2005Q4.lean b/Archive/Imo/Imo2005Q4.lean index 56be75dd551a7..7e9272d4a0556 100644 --- a/Archive/Imo/Imo2005Q4.lean +++ b/Archive/Imo/Imo2005Q4.lean @@ -29,7 +29,7 @@ def a (n : ℕ) : ℤ := theorem find_specified_factor {p : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) (hp3 : p ≠ 3) : ↑p ∣ a (p - 2) := by -- Since `p` is neither `2` nor `3`, it is coprime with `2`, `3`, and `6` - rw [Ne.def, ← Nat.prime_dvd_prime_iff_eq hp (by norm_num), ← Nat.Prime.coprime_iff_not_dvd hp] + rw [Ne.def, ← Nat.prime_dvd_prime_iff_eq hp (by decide), ← Nat.Prime.coprime_iff_not_dvd hp] at hp2 hp3 have : Int.gcd p 6 = 1 := Nat.coprime_mul_iff_right.2 ⟨hp2, hp3⟩ -- Nat arithmetic needed to deal with powers @@ -71,10 +71,10 @@ theorem imo2005_q4 {k : ℕ} (hk : 0 < k) : (∀ n : ℕ, 1 ≤ n → IsCoprime -- For `p = 2` and `p = 3`, take `n = 1` and `n = 2`, respectively by_cases hp2 : p = 2 · rw [hp2] at h - apply h 1 <;> norm_num + apply h 1 <;> decide by_cases hp3 : p = 3 · rw [hp3] at h - apply h 2 <;> norm_num + apply h 2 <;> decide -- Otherwise, take `n = p - 2` refine h (p - 2) ?_ (find_specified_factor hp hp2 hp3) calc diff --git a/Archive/Imo/Imo2019Q1.lean b/Archive/Imo/Imo2019Q1.lean index 6e486889066d0..2bcd5a9f405b9 100644 --- a/Archive/Imo/Imo2019Q1.lean +++ b/Archive/Imo/Imo2019Q1.lean @@ -27,7 +27,7 @@ theorem imo2019_q1 (f : ℤ → ℤ) : (∀ a b : ℤ, f (2 * a) + 2 * f b = f (f (a + b))) ↔ f = 0 ∨ ∃ c, f = fun x => 2 * x + c := by constructor; swap -- easy way: f(x)=0 and f(x)=2x+c work. - · rintro (rfl | ⟨c, rfl⟩) <;> intros <;> simp only [Pi.zero_apply]; ring + · rintro (rfl | ⟨c, rfl⟩) <;> intros <;> norm_num; ring -- hard way. intro hf -- functional equation diff --git a/Archive/Imo/Imo2019Q2.lean b/Archive/Imo/Imo2019Q2.lean index c301c615ed3ad..3c2131796191b 100644 --- a/Archive/Imo/Imo2019Q2.lean +++ b/Archive/Imo/Imo2019Q2.lean @@ -442,7 +442,7 @@ theorem not_collinear_QPA₂ : ¬Collinear ℝ ({cfg.Q, cfg.P, cfg.A₂} : Set P have h : Cospherical ({cfg.B, cfg.A, cfg.A₂} : Set Pt) := by refine' cfg.triangleABC.circumsphere.cospherical.subset _ simp only [Set.insert_subset_iff, cfg.A_mem_circumsphere, cfg.B_mem_circumsphere, - cfg.A₂_mem_circumsphere, Sphere.mem_coe, Set.singleton_subset_iff] + cfg.A₂_mem_circumsphere, Sphere.mem_coe, Set.singleton_subset_iff, and_true] exact h.affineIndependent_of_ne cfg.A_ne_B.symm cfg.A₂_ne_B.symm cfg.A₂_ne_A.symm #align imo2019_q2.imo2019q2_cfg.not_collinear_QPA₂ Imo2019Q2.Imo2019q2Cfg.not_collinear_QPA₂ diff --git a/Archive/Imo/Imo2019Q4.lean b/Archive/Imo/Imo2019Q4.lean index b52f6085c03ce..edde9fc8f8d3e 100644 --- a/Archive/Imo/Imo2019Q4.lean +++ b/Archive/Imo/Imo2019Q4.lean @@ -65,7 +65,7 @@ theorem upper_bound {k n : ℕ} (hk : k > 0) _ ≤ k ! := by gcongr clear h h2 induction' n, hn using Nat.le_induction with n' hn' IH - · norm_num + · decide let A := ∑ i in range n', i have le_sum : ∑ i in range 6, i ≤ A · apply sum_le_sum_of_subset @@ -87,8 +87,7 @@ theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) : -- The implication `←` holds. constructor swap - · rintro (h | h) <;> simp [Prod.ext_iff] at h <;> rcases h with ⟨rfl, rfl⟩ <;> - norm_num [prod_range_succ, succ_mul] + · rintro (h | h) <;> simp [Prod.ext_iff] at h <;> rcases h with ⟨rfl, rfl⟩ <;> decide intro h -- We know that n < 6. have := Imo2019Q4.upper_bound hk h @@ -101,9 +100,9 @@ theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) : exact h; rw [h]; norm_num all_goals exfalso; norm_num [prod_range_succ] at h; norm_cast at h -- n = 3 - · refine' monotone_factorial.ne_of_lt_of_lt_nat 5 _ _ _ h <;> norm_num + · refine' monotone_factorial.ne_of_lt_of_lt_nat 5 _ _ _ h <;> decide -- n = 4 - · refine' monotone_factorial.ne_of_lt_of_lt_nat 7 _ _ _ h <;> norm_num + · refine' monotone_factorial.ne_of_lt_of_lt_nat 7 _ _ _ h <;> decide -- n = 5 - · refine' monotone_factorial.ne_of_lt_of_lt_nat 10 _ _ _ h <;> norm_num + · refine' monotone_factorial.ne_of_lt_of_lt_nat 10 _ _ _ h <;> decide #align imo2019_q4 imo2019_q4 diff --git a/Archive/MiuLanguage/DecisionNec.lean b/Archive/MiuLanguage/DecisionNec.lean index 89f01eb056d6e..ac22effdd4b50 100644 --- a/Archive/MiuLanguage/DecisionNec.lean +++ b/Archive/MiuLanguage/DecisionNec.lean @@ -61,7 +61,7 @@ theorem mod3_eq_1_or_mod3_eq_2 {a b : ℕ} (h1 : a % 3 = 1 ∨ a % 3 = 2) · rw [h2]; exact h1 · cases' h1 with h1 h1 · right; simp [h2, mul_mod, h1, Nat.succ_lt_succ] - · left; simp [h2, mul_mod, h1] + · left; simp only [h2, mul_mod, h1, mod_mod]; decide #align miu.mod3_eq_1_or_mod3_eq_2 Miu.mod3_eq_1_or_mod3_eq_2 /-- `count_equiv_one_or_two_mod3_of_derivable` shows any derivable string must have a `count I` that @@ -80,7 +80,7 @@ theorem count_equiv_one_or_two_mod3_of_derivable (en : Miustr) : simp_rw [count_cons_self, count_nil, count_cons, ite_false, add_right_comm, add_mod_right] simp · left; rw [count_append, count_append, count_append] - simp only [ne_eq, count_cons_of_ne, count_nil, add_zero] + simp only [ne_eq, not_false_eq_true, count_cons_of_ne, count_nil, add_zero] #align miu.count_equiv_one_or_two_mod3_of_derivable Miu.count_equiv_one_or_two_mod3_of_derivable /-- Using the above theorem, we solve the MU puzzle, showing that `"MU"` is not derivable. @@ -134,7 +134,7 @@ theorem goodm_of_rule1 (xs : Miustr) (h₁ : Derivable (xs ++ ↑[I])) (h₂ : G exact mhead · change ¬M ∈ tail (xs ++ ↑([I] ++ [U])) rw [← append_assoc, tail_append_singleton_of_ne_nil] - · simp_rw [mem_append, not_or, and_true]; exact nmtail + · simp_rw [mem_append, mem_singleton, or_false]; exact nmtail · exact append_ne_nil_of_ne_nil_left _ _ this #align miu.goodm_of_rule1 Miu.goodm_of_rule1 diff --git a/Archive/MiuLanguage/DecisionSuf.lean b/Archive/MiuLanguage/DecisionSuf.lean index 7f9fdaba0ac4a..6c7ff233e8c95 100644 --- a/Archive/MiuLanguage/DecisionSuf.lean +++ b/Archive/MiuLanguage/DecisionSuf.lean @@ -267,7 +267,7 @@ theorem count_I_eq_length_of_count_U_zero_and_neg_mem {ys : Miustr} (hu : count · simpa only [count] · rw [mem_cons, not_or] at hm; exact hm.2 · -- case `x = U` gives a contradiction. - exfalso; simp only [count, countP_cons_of_pos] at hu + exfalso; simp only [count, countP_cons_of_pos (· == U) _ (rfl : U == U)] at hu exact succ_ne_zero _ hu set_option linter.uppercaseLean3 false in #align miu.count_I_eq_length_of_count_U_zero_and_neg_mem Miu.count_I_eq_length_of_count_U_zero_and_neg_mem @@ -277,7 +277,8 @@ set_option linter.uppercaseLean3 false in theorem base_case_suf (en : Miustr) (h : Decstr en) (hu : count U en = 0) : Derivable en := by rcases h with ⟨⟨mhead, nmtail⟩, hi⟩ have : en ≠ nil := by - intro k; simp only [k, count, countP, if_false, zero_mod, zero_ne_one, false_or_iff] at hi + intro k + simp only [k, count, countP, countP.go, if_false, zero_mod, zero_ne_one, false_or_iff] at hi rcases exists_cons_of_ne_nil this with ⟨y, ys, rfl⟩ rcases mhead rsuffices ⟨c, rfl, hc⟩ : ∃ c, replicate c I = ys ∧ (c % 3 = 1 ∨ c % 3 = 2) @@ -331,7 +332,7 @@ theorem ind_hyp_suf (k : ℕ) (ys : Miustr) (hu : count U ys = succ k) (hdec : D rw [cons_append, cons_append] dsimp [tail] at nmtail ⊢ rw [mem_append] at nmtail - simpa only [mem_append, mem_cons, false_or_iff, or_false_iff] using nmtail + simpa only [append_assoc, cons_append, nil_append, mem_append, mem_cons, false_or] using nmtail · rw [count_append, count_append]; rw [← cons_append, count_append] at hic simp only [count_cons_self, count_nil, count_cons, if_false] at hic ⊢ rw [add_right_comm, add_mod_right]; exact hic diff --git a/Archive/Wiedijk100Theorems/AbelRuffini.lean b/Archive/Wiedijk100Theorems/AbelRuffini.lean index 72eb193a353d3..33efd6ea814d1 100644 --- a/Archive/Wiedijk100Theorems/AbelRuffini.lean +++ b/Archive/Wiedijk100Theorems/AbelRuffini.lean @@ -94,10 +94,11 @@ theorem irreducible_Phi (p : ℕ) (hp : p.Prime) (hpa : p ∣ a) (hpb : p ∣ b) rw [mem_span_singleton] rw [degree_Phi] at hn; norm_cast at hn interval_cases hn : n <;> - simp only [Φ, coeff_X_pow, coeff_C, Int.coe_nat_dvd.mpr, hpb, if_true, coeff_C_mul, if_false, - coeff_X_zero, hpa, coeff_add, zero_add, mul_zero, coeff_sub, add_zero, zero_sub, dvd_neg, - neg_zero, dvd_mul_of_dvd_left] + simp (config := {decide := true}) only [Φ, coeff_X_pow, coeff_C, Int.coe_nat_dvd.mpr, hpb, + if_true, coeff_C_mul, if_false, coeff_X_zero, hpa, coeff_add, zero_add, mul_zero, coeff_sub, + add_zero, zero_sub, dvd_neg, neg_zero, dvd_mul_of_dvd_left] · simp only [degree_Phi, ← WithBot.coe_zero, WithBot.coe_lt_coe, Nat.succ_pos'] + decide · rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton] exact mt Int.coe_nat_dvd.mp hp2b all_goals exact Monic.isPrimitive (monic_Phi a b) @@ -136,7 +137,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) : have hfa := calc f (-a) = (a : ℝ) ^ 2 - (a : ℝ) ^ 5 + b := by - norm_num [hf, ← sq, sub_eq_add_neg, add_comm, Odd.neg_pow] + norm_num [hf, ← sq, sub_eq_add_neg, add_comm, Odd.neg_pow (by decide : Odd 5)] _ ≤ (a : ℝ) ^ 2 - (a : ℝ) ^ 3 + (a - 1) := by refine' add_le_add (sub_le_sub_left (pow_le_pow ha _) _) _ <;> linarith _ = -((a : ℝ) - 1) ^ 2 * (a + 1) := by ring @@ -163,7 +164,7 @@ theorem complex_roots_Phi (h : (Φ ℚ a b).Separable) : Fintype.card ((Φ ℚ a theorem gal_Phi (hab : b < a) (h_irred : Irreducible (Φ ℚ a b)) : Bijective (galActionHom (Φ ℚ a b) ℂ) := by apply galActionHom_bijective_of_prime_degree' h_irred - · norm_num [natDegree_Phi] + · simp only [natDegree_Phi]; decide · rw [complex_roots_Phi a b h_irred.separable, Nat.succ_le_succ_iff] exact (real_roots_Phi_le a b).trans (Nat.le_succ 3) · simp_rw [complex_roots_Phi a b h_irred.separable, Nat.succ_le_succ_iff] @@ -181,7 +182,7 @@ theorem not_solvable_by_rad (p : ℕ) (x : ℂ) (hx : aeval x (Φ ℚ a b) = 0) #align abel_ruffini.not_solvable_by_rad AbelRuffini.not_solvable_by_rad theorem not_solvable_by_rad' (x : ℂ) (hx : aeval x (Φ ℚ 4 2) = 0) : ¬IsSolvableByRad ℚ x := by - apply not_solvable_by_rad 4 2 2 x hx <;> norm_num + apply not_solvable_by_rad 4 2 2 x hx <;> decide #align abel_ruffini.not_solvable_by_rad' AbelRuffini.not_solvable_by_rad' /-- **Abel-Ruffini Theorem** -/ diff --git a/Archive/Wiedijk100Theorems/BallotProblem.lean b/Archive/Wiedijk100Theorems/BallotProblem.lean index 84660e6e21d11..f7a5a95024821 100644 --- a/Archive/Wiedijk100Theorems/BallotProblem.lean +++ b/Archive/Wiedijk100Theorems/BallotProblem.lean @@ -221,7 +221,9 @@ theorem first_vote_pos : simp [ENNReal.div_self _ _] | 0, q + 1, _ => by rw [counted_left_zero, condCount_singleton] - simp + simp only [List.replicate, Nat.add_eq, add_zero, mem_setOf_eq, List.headI_cons, Nat.cast_zero, + ENNReal.zero_div, ite_eq_right_iff] + decide | p + 1, q + 1, _ => by simp_rw [counted_succ_succ] rw [← condCount_disjoint_union ((countedSequence_finite _ _).image _) diff --git a/Archive/Wiedijk100Theorems/BirthdayProblem.lean b/Archive/Wiedijk100Theorems/BirthdayProblem.lean index 4c3224823ebb2..016c949b9d7f4 100644 --- a/Archive/Wiedijk100Theorems/BirthdayProblem.lean +++ b/Archive/Wiedijk100Theorems/BirthdayProblem.lean @@ -30,6 +30,7 @@ local notation "‖" x "‖" => Fintype.card x theorem birthday : 2 * ‖Fin 23 ↪ Fin 365‖ < ‖Fin 23 → Fin 365‖ ∧ 2 * ‖Fin 22 ↪ Fin 365‖ > ‖Fin 22 → Fin 365‖ := by simp only [Nat.descFactorial, Fintype.card_fin, Fintype.card_embedding_eq, Fintype.card_fun] + norm_num #align theorems_100.birthday Theorems100.birthday section MeasureTheory @@ -76,7 +77,7 @@ theorem birthday_measure : exact Fintype.card_congr (Equiv.subtypeInjectiveEquivEmbedding _ _) · simp only [Fintype.card_embedding_eq, Fintype.card_fin, Nat.descFactorial] rw [this, ENNReal.lt_div_iff_mul_lt, mul_comm, mul_div, ENNReal.div_lt_iff] - rotate_left; (iterate 2 right; norm_num); (iterate 2 left; norm_num) + rotate_left; (iterate 2 right; norm_num); decide; (iterate 2 left; norm_num) norm_cast simp only [Fintype.card_pi] norm_num diff --git a/Archive/Wiedijk100Theorems/Konigsberg.lean b/Archive/Wiedijk100Theorems/Konigsberg.lean index 816ba1994e37b..a277213885050 100644 --- a/Archive/Wiedijk100Theorems/Konigsberg.lean +++ b/Archive/Wiedijk100Theorems/Konigsberg.lean @@ -75,7 +75,7 @@ lemma degree_eq_degree (v : Verts) : graph.degree v = degree v := by cases v <;> #align konigsberg.degree_eq_degree Konigsberg.degree_eq_degree lemma not_even_degree_iff (w : Verts) : ¬Even (degree w) ↔ w = V1 ∨ w = V2 ∨ w = V3 ∨ w = V4 := by - cases w <;> simp + cases w <;> decide lemma setOf_odd_degree_eq : {v | Odd (graph.degree v)} = {Verts.V1, Verts.V2, Verts.V3, Verts.V4} := by diff --git a/Archive/Wiedijk100Theorems/PerfectNumbers.lean b/Archive/Wiedijk100Theorems/PerfectNumbers.lean index ff1f483234934..c610c03973978 100644 --- a/Archive/Wiedijk100Theorems/PerfectNumbers.lean +++ b/Archive/Wiedijk100Theorems/PerfectNumbers.lean @@ -39,8 +39,8 @@ namespace Nat open Nat.ArithmeticFunction Finset theorem sigma_two_pow_eq_mersenne_succ (k : ℕ) : σ 1 (2 ^ k) = mersenne (k + 1) := by - simp [sigma_one_apply, mersenne, Nat.prime_two, show 2 = 1 + 1 from rfl, - ← geom_sum_mul_add 1 (k + 1)] + simp_rw [sigma_one_apply, mersenne, show 2 = 1 + 1 from rfl, ← geom_sum_mul_add 1 (k + 1)] + norm_num #align theorems_100.nat.sigma_two_pow_eq_mersenne_succ Theorems100.Nat.sigma_two_pow_eq_mersenne_succ /-- Euclid's theorem that Mersenne primes induce perfect numbers -/ diff --git a/Archive/ZagierTwoSquares.lean b/Archive/ZagierTwoSquares.lean index 686263c38918f..87dfcf5a23c7f 100644 --- a/Archive/ZagierTwoSquares.lean +++ b/Archive/ZagierTwoSquares.lean @@ -48,9 +48,10 @@ lemma zagierSet_lower_bound {x y z : ℕ} (h : (x, y, z) ∈ zagierSet k) : 0 < all_goals cases' (Nat.dvd_prime hk.out).1 (dvd_of_mul_left_eq _ h) with e e all_goals - simp only [e, self_eq_add_left, ne_eq, add_eq_zero, and_false, mul_eq_left₀] at h + simp only [e, self_eq_add_left, ne_eq, add_eq_zero, and_false, not_false_eq_true, + mul_eq_left₀] at h simp only [h, zero_add] at hk - exact hk.out + exact Nat.not_prime_one hk.out lemma zagierSet_upper_bound {x y z : ℕ} (h : (x, y, z) ∈ zagierSet k) : x ≤ k + 1 ∧ y ≤ k ∧ z ≤ k := by @@ -143,11 +144,12 @@ theorem eq_of_mem_fixedPoints {t : zagierSet k} (mem : t ∈ fixedPoints (comple rw [mem_fixedPoints_iff, complexInvo, Subtype.mk.injEq] at mem split_ifs at mem with less more <;> -- less (completely handled by the pre-applied `simp_all only`) - simp_all only [not_lt, Prod.mk.injEq, add_right_eq_self, mul_eq_zero, false_or] + simp_all only [not_lt, Prod.mk.injEq, add_right_eq_self, mul_eq_zero, false_or, + lt_self_iff_false] · -- more obtain ⟨_, _, _⟩ := mem; simp_all · -- middle (the one fixed point falls under this case) - simp only [zagierSet, Set.mem_setOf_eq] at h + simp [zagierSet, Set.mem_setOf_eq] at h replace mem := mem.1 rw [tsub_eq_iff_eq_add_of_le more, ← two_mul] at mem replace mem := (mul_left_cancel₀ two_ne_zero mem).symm @@ -194,3 +196,4 @@ theorem Nat.Prime.sq_add_sq' {p : ℕ} [h : Fact p.Prime] (hp : p % 4 = 1) : contrapose key rw [Set.not_nonempty_iff_eq_empty] at key simp_rw [key, Fintype.card_of_isEmpty, card_fixedPoints_eq_one] + decide diff --git a/Counterexamples/Cyclotomic105.lean b/Counterexamples/Cyclotomic105.lean index f05b5d44f1eba..07a1cd6df40d5 100644 --- a/Counterexamples/Cyclotomic105.lean +++ b/Counterexamples/Cyclotomic105.lean @@ -109,7 +109,7 @@ theorem cyclotomic_105 : #align counterexample.cyclotomic_105 Counterexample.cyclotomic_105 theorem coeff_cyclotomic_105 : coeff (cyclotomic 105 ℤ) 7 = -2 := by - simp [cyclotomic_105, coeff_X_pow, coeff_one, coeff_X_of_ne_one, coeff_bit0_mul, two_mul] + simp [cyclotomic_105, coeff_one, coeff_X_of_ne_one] #align counterexample.coeff_cyclotomic_105 Counterexample.coeff_cyclotomic_105 theorem not_forall_coeff_cyclotomic_neg_one_zero_one : diff --git a/Counterexamples/HomogeneousPrimeNotPrime.lean b/Counterexamples/HomogeneousPrimeNotPrime.lean index dd776d4703975..d3d2dcdb4aec1 100644 --- a/Counterexamples/HomogeneousPrimeNotPrime.lean +++ b/Counterexamples/HomogeneousPrimeNotPrime.lean @@ -175,7 +175,7 @@ theorem homogeneous_mem_or_mem {x y : R × R} (hx : SetLike.Homogeneous (grading -- Porting note: added `h2` for later use; the proof is hideous have h2 : Prime (2:R) := by unfold Prime - simp only [true_and] + refine ⟨by decide, by decide, ?_⟩ intro a b have aux2 : (Fin.mk 2 _ : R) = 2 := rfl have aux3 : (Fin.mk 3 _ : R) = -1 := rfl diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean index 3d8fe2eb70ea6..11db242cb6ec0 100644 --- a/Mathlib/Algebra/BigOperators/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Basic.lean @@ -2125,7 +2125,7 @@ theorem finset_sum_eq_sup_iff_disjoint {β : Type*} {i : Finset β} {f : β → · simp only [Finset.not_mem_empty, IsEmpty.forall_iff, imp_true_iff, Finset.sum_empty, Finset.sup_empty, bot_eq_zero, eq_self_iff_true] · simp_rw [Finset.sum_cons hz, Finset.sup_cons, Finset.mem_cons, Multiset.sup_eq_union, - forall_eq_or_imp, Ne.def, IsEmpty.forall_iff, true_and_iff, + forall_eq_or_imp, Ne.def, not_true_eq_false, IsEmpty.forall_iff, true_and_iff, imp_and, forall_and, ← hr, @eq_comm _ z] have := fun x (H : x ∈ i) => ne_of_mem_of_not_mem H hz simp (config := { contextual := true }) only [this, not_false_iff, true_imp_iff] @@ -2284,7 +2284,7 @@ theorem nat_abs_sum_le {ι : Type*} (s : Finset ι) (f : ι → ℤ) : (∑ i in s, f i).natAbs ≤ ∑ i in s, (f i).natAbs := by classical induction' s using Finset.induction_on with i s his IH - · simp only [Finset.sum_empty, Int.natAbs_zero] + · simp only [Finset.sum_empty, Int.natAbs_zero, le_refl] · simp only [his, Finset.sum_insert, not_false_iff] exact (Int.natAbs_add_le _ _).trans (add_le_add le_rfl IH) #align nat_abs_sum_le nat_abs_sum_le diff --git a/Mathlib/Algebra/CharP/Basic.lean b/Mathlib/Algebra/CharP/Basic.lean index 1189f3e12fb17..4b35b9a12c0b8 100644 --- a/Mathlib/Algebra/CharP/Basic.lean +++ b/Mathlib/Algebra/CharP/Basic.lean @@ -718,8 +718,8 @@ theorem Int.cast_injOn_of_ringChar_ne_two {R : Type*} [NonAssocRing R] [Nontrivi rintro _ (rfl | rfl | rfl) _ (rfl | rfl | rfl) h <;> simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢ - · exact (Ring.neg_one_ne_one_of_char_ne_two hR).symm h - · exact (Ring.neg_one_ne_one_of_char_ne_two hR) h + · exact ((Ring.neg_one_ne_one_of_char_ne_two hR).symm h).elim + · exact ((Ring.neg_one_ne_one_of_char_ne_two hR) h).elim #align int.cast_inj_on_of_ring_char_ne_two Int.cast_injOn_of_ringChar_ne_two end diff --git a/Mathlib/Algebra/GeomSum.lean b/Mathlib/Algebra/GeomSum.lean index e5aec67a3a769..32abc46ecd2a4 100644 --- a/Mathlib/Algebra/GeomSum.lean +++ b/Mathlib/Algebra/GeomSum.lean @@ -483,7 +483,7 @@ theorem geom_sum_alternating_of_le_neg_one [StrictOrderedRing α] (hx : x + 1 if Even n then (∑ i in range n, x ^ i) ≤ 0 else 1 ≤ ∑ i in range n, x ^ i := by have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx induction' n with n ih - · simp only [Nat.zero_eq, range_zero, sum_empty, le_refl, ite_true] + · simp only [Nat.zero_eq, range_zero, sum_empty, le_refl, ite_true, even_zero] simp only [Nat.even_add_one, geom_sum_succ] split_ifs at ih with h · rw [if_neg (not_not_intro h), le_add_iff_nonneg_left] @@ -497,7 +497,7 @@ theorem geom_sum_alternating_of_lt_neg_one [StrictOrderedRing α] (hx : x + 1 < if Even n then (∑ i in range n, x ^ i) < 0 else 1 < ∑ i in range n, x ^ i := by have hx0 : x < 0 := ((le_add_iff_nonneg_right _).2 zero_le_one).trans_lt hx refine' Nat.le_induction _ _ n (show 2 ≤ n from hn) - · simp only [geom_sum_two, lt_add_iff_pos_left, ite_true, gt_iff_lt, hx] + · simp only [geom_sum_two, lt_add_iff_pos_left, ite_true, gt_iff_lt, hx, even_two] clear hn intro n _ ihn simp only [Nat.even_add_one, geom_sum_succ] @@ -571,7 +571,7 @@ theorem geom_sum_eq_zero_iff_neg_one [LinearOrderedRing α] (hn : n ≠ 0) : have hx := eq_or_ne x (-1) cases' hx with hx hx · rw [hx, neg_one_geom_sum] - simp only [h hx, ne_eq, ite_eq_left_iff, one_ne_zero, not_forall, exists_prop, and_true] + simp only [h hx, ite_false, ne_eq, one_ne_zero, not_false_eq_true] · exact geom_sum_ne_zero hx hn #align geom_sum_eq_zero_iff_neg_one geom_sum_eq_zero_iff_neg_one diff --git a/Mathlib/Algebra/GroupPower/NegOnePow.lean b/Mathlib/Algebra/GroupPower/NegOnePow.lean index 06b6b2f499283..d53c1e0bf8040 100644 --- a/Mathlib/Algebra/GroupPower/NegOnePow.lean +++ b/Mathlib/Algebra/GroupPower/NegOnePow.lean @@ -56,6 +56,7 @@ lemma negOnePow_eq_one_iff (n : ℤ) : n.negOnePow = 1 ↔ Even n := by rw [Int.even_iff_not_odd] intro h' simp only [negOnePow_odd _ h'] at h + contradiction · exact negOnePow_even n lemma negOnePow_eq_neg_one_iff (n : ℤ) : n.negOnePow = -1 ↔ Odd n := by @@ -64,7 +65,7 @@ lemma negOnePow_eq_neg_one_iff (n : ℤ) : n.negOnePow = -1 ↔ Odd n := by rw [Int.odd_iff_not_even] intro h' rw [negOnePow_even _ h'] at h - simp only at h + contradiction · exact negOnePow_odd n @[simp] diff --git a/Mathlib/Algebra/Homology/Augment.lean b/Mathlib/Algebra/Homology/Augment.lean index fe2d9689017c8..b19030893c688 100644 --- a/Mathlib/Algebra/Homology/Augment.lean +++ b/Mathlib/Algebra/Homology/Augment.lean @@ -239,7 +239,7 @@ def augment (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d shape i j s := by simp at s rcases j with (_ | _ | j) <;> cases i <;> try simp - · simp at s + · contradiction · rw [C.shape] simp only [ComplexShape.up_Rel] contrapose! s diff --git a/Mathlib/Algebra/Homology/Exact.lean b/Mathlib/Algebra/Homology/Exact.lean index e2b84689772d6..3167d21fea54b 100644 --- a/Mathlib/Algebra/Homology/Exact.lean +++ b/Mathlib/Algebra/Homology/Exact.lean @@ -150,7 +150,7 @@ theorem imageToKernel_isIso_of_image_eq_kernel {A B C : V} (f : A ⟶ B) (g : B IsIso (imageToKernel f g (comp_eq_zero_of_image_eq_kernel f g p)) := by refine' ⟨⟨Subobject.ofLE _ _ p.ge, _⟩⟩ dsimp [imageToKernel] - simp only [Subobject.ofLE_comp_ofLE, Subobject.ofLE_refl] + simp only [Subobject.ofLE_comp_ofLE, Subobject.ofLE_refl, and_self] #align category_theory.image_to_kernel_is_iso_of_image_eq_kernel CategoryTheory.imageToKernel_isIso_of_image_eq_kernel -- We'll prove the converse later, when `V` is abelian. diff --git a/Mathlib/Algebra/Homology/Flip.lean b/Mathlib/Algebra/Homology/Flip.lean index 678caa3a87780..8e4ad84660353 100644 --- a/Mathlib/Algebra/Homology/Flip.lean +++ b/Mathlib/Algebra/Homology/Flip.lean @@ -39,7 +39,7 @@ def flipObj (C : HomologicalComplex (HomologicalComplex V c) c') : { X := fun j => (C.X j).X i d := fun j j' => (C.d j j').f i shape := fun j j' w => by - simp_all only [shape, zero_f] + simp_all only [not_false_eq_true, shape, zero_f] d_comp_d' := fun j₁ j₂ j₃ _ _ => congr_hom (C.d_comp_d j₁ j₂ j₃) i } d i i' := { f := fun j => (C.X j).d i i' diff --git a/Mathlib/Algebra/Homology/Homotopy.lean b/Mathlib/Algebra/Homology/Homotopy.lean index 55b7e688b2398..a0a7d0faf0a25 100644 --- a/Mathlib/Algebra/Homology/Homotopy.lean +++ b/Mathlib/Algebra/Homology/Homotopy.lean @@ -565,7 +565,7 @@ def mkInductive : Homotopy e 0 where · cases i · dsimp [fromNext, mkInductiveAux₂] rw [dif_neg] - simp only + decide · dsimp [fromNext] simp only [ChainComplex.next_nat_succ, dite_true] rw [mkInductiveAux₃ e zero comm_zero one comm_one succ] @@ -704,7 +704,7 @@ def mkCoinductive : Homotopy e 0 where · cases i · dsimp [toPrev, mkCoinductiveAux₂] rw [dif_neg] - simp only + decide · dsimp [toPrev] simp only [CochainComplex.prev_nat_succ, dite_true] rw [mkCoinductiveAux₃ e zero comm_zero one comm_one succ] diff --git a/Mathlib/Algebra/Homology/Single.lean b/Mathlib/Algebra/Homology/Single.lean index ed740c9a88d5a..56aa1491d15bb 100644 --- a/Mathlib/Algebra/Homology/Single.lean +++ b/Mathlib/Algebra/Homology/Single.lean @@ -265,7 +265,8 @@ def fromSingle₀Equiv (C : ChainComplex V ℕ) (X : V) : ((single₀ V).obj X comm' := fun i j h => by cases i <;> cases j <;> simp only [shape, ComplexShape.down_Rel, Nat.one_ne_zero, not_false_iff, - zero_comp, single₀_obj_X_d, Nat.zero_eq, add_eq_zero, comp_zero] } + zero_comp, single₀_obj_X_d, Nat.zero_eq, add_eq_zero, comp_zero, not_false_eq_true, + Nat.succ_ne_zero, and_self] } left_inv f := by ext i cases i diff --git a/Mathlib/Algebra/IsPrimePow.lean b/Mathlib/Algebra/IsPrimePow.lean index 8050955c70d8c..72ac069276671 100644 --- a/Mathlib/Algebra/IsPrimePow.lean +++ b/Mathlib/Algebra/IsPrimePow.lean @@ -101,7 +101,7 @@ theorem IsPrimePow.dvd {n m : ℕ} (hn : IsPrimePow n) (hm : m ∣ n) (hm₁ : m refine' ⟨p, i, hp, _, rfl⟩ apply Nat.pos_of_ne_zero rintro rfl - simp only [pow_zero, ne_eq] at hm₁ + simp only [pow_zero, ne_eq, not_true_eq_false] at hm₁ #align is_prime_pow.dvd IsPrimePow.dvd theorem Nat.disjoint_divisors_filter_isPrimePow {a b : ℕ} (hab : a.Coprime b) : diff --git a/Mathlib/Algebra/Order/Ring/WithTop.lean b/Mathlib/Algebra/Order/Ring/WithTop.lean index 34a4b6728f2a0..06d498ee8fb2e 100644 --- a/Mathlib/Algebra/Order/Ring/WithTop.lean +++ b/Mathlib/Algebra/Order/Ring/WithTop.lean @@ -67,7 +67,7 @@ theorem mul_eq_top_iff {a b : WithTop α} : a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ theorem mul_lt_top' [LT α] {a b : WithTop α} (ha : a < ⊤) (hb : b < ⊤) : a * b < ⊤ := by rw [WithTop.lt_top_iff_ne_top] at * - simp only [Ne.def, mul_eq_top_iff, *, and_false, false_and, false_or] + simp only [Ne.def, mul_eq_top_iff, *, and_false, false_and, or_self, not_false_eq_true] #align with_top.mul_lt_top' WithTop.mul_lt_top' theorem mul_lt_top [LT α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b < ⊤ := diff --git a/Mathlib/Algebra/Order/Sub/WithTop.lean b/Mathlib/Algebra/Order/Sub/WithTop.lean index 4baf09510cae5..dedf9ca024409 100644 --- a/Mathlib/Algebra/Order/Sub/WithTop.lean +++ b/Mathlib/Algebra/Order/Sub/WithTop.lean @@ -47,8 +47,8 @@ theorem sub_top {a : WithTop α} : a - ⊤ = 0 := by cases a <;> rfl @[simp] theorem sub_eq_top_iff {a b : WithTop α} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤ := by induction a using recTopCoe <;> induction b using recTopCoe <;> - simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, coe_ne_top, top_sub_coe, false_and, - Ne.def] + simp only [← coe_sub, coe_ne_top, sub_top, zero_ne_top, top_sub_coe, false_and, + Ne.def, not_true_eq_false, not_false_eq_true, and_false, and_self] #align with_top.sub_eq_top_iff WithTop.sub_eq_top_iff theorem map_sub [Sub β] [Zero β] {f : α → β} (h : ∀ x y, f (x - y) = f x - f y) (h₀ : f 0 = 0) : diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean index 0c4b786455629..747d7790b4cc6 100644 --- a/Mathlib/Algebra/Quaternion.lean +++ b/Mathlib/Algebra/Quaternion.lean @@ -1454,7 +1454,7 @@ section QuaternionAlgebra variable {R : Type*} (c₁ c₂ : R) private theorem pow_four [Infinite R] : #R ^ℕ 4 = #R := - power_nat_eq (aleph0_le_mk R) <| by simp + power_nat_eq (aleph0_le_mk R) <| by decide /-- The cardinality of a quaternion algebra, as a type. -/ theorem mk_quaternionAlgebra : #(ℍ[R,c₁,c₂]) = #R ^ℕ 4 := by diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean index 90e2e1ece6371..552e73d07efe7 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean @@ -638,8 +638,8 @@ lemma irreducible_polynomial [IsDomain R] : Irreducible W.polynomial := by apply (h1.symm.le.trans Cubic.degree_of_b_eq_zero').not_lt rcases Nat.WithBot.add_eq_three_iff.mp h0.symm with h | h | h | h -- porting note: replaced two `any_goals` proofs with two `iterate 2` proofs - iterate 2 rw [degree_add_eq_right_of_degree_lt] <;> simp only [h] - iterate 2 rw [degree_add_eq_left_of_degree_lt] <;> simp only [h] + iterate 2 rw [degree_add_eq_right_of_degree_lt] <;> simp only [h] <;> decide + iterate 2 rw [degree_add_eq_left_of_degree_lt] <;> simp only [h] <;> decide #align weierstrass_curve.irreducible_polynomial WeierstrassCurve.irreducible_polynomial -- porting note: removed `@[simp]` to avoid a `simpNF` linter error @@ -1029,7 +1029,7 @@ lemma norm_smul_basis (p q : R[X]) : simp_rw [Algebra.norm_eq_matrix_det <| CoordinateRing.basis W, Matrix.det_fin_two, Algebra.leftMulMatrix_eq_repr_mul, basis_zero, mul_one, basis_one, smul_basis_mul_Y, map_add, Finsupp.add_apply, map_smul, Finsupp.smul_apply, ← basis_zero, ← basis_one, - Basis.repr_self_apply, if_pos, if_neg, smul_eq_mul] + Basis.repr_self_apply, if_pos, one_ne_zero, if_false, smul_eq_mul] ring1 #align weierstrass_curve.coordinate_ring.norm_smul_basis WeierstrassCurve.CoordinateRing.norm_smul_basis diff --git a/Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean b/Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean index 25f486dc08c1f..9425f8d75b786 100644 --- a/Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean +++ b/Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean @@ -63,7 +63,7 @@ instance : ReflectsIsomorphisms (N₁ : SimplicialObject C ⥤ Karoubi (ChainCom b := fun i => inv (f.app (op [n])) ≫ X.σ i } simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp, PInfty_f_naturality_assoc, IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc, - SimplicialObject.σ_naturality, h₁, h₂, h₃]⟩ + SimplicialObject.σ_naturality, h₁, h₂, h₃, and_self]⟩ theorem compatibility_N₂_N₁_karoubi : N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor = diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean index eb538b796d39d..e127b31b63fb5 100644 --- a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean +++ b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean @@ -89,7 +89,7 @@ theorem splitLower_def [DecidableEq ι] {i x} (h : x ∈ Ioo (I.lower i) (I.uppe (forall_update_iff I.upper fun j y => I.lower j < y).2 ⟨h.1, fun j _ => I.lower_lt_upper _⟩) : I.splitLower i x = (⟨I.lower, update I.upper i x, h'⟩ : Box ι) := by - simp only [splitLower, mk'_eq_coe, min_eq_left h.2.le, update] + simp only [splitLower, mk'_eq_coe, min_eq_left h.2.le, update, and_self] #align box_integral.box.split_lower_def BoxIntegral.Box.splitLower_def /-- Given a box `I` and `x ∈ (I.lower i, I.upper i)`, the hyperplane `{y : ι → ℝ | y i = x}` splits @@ -130,7 +130,7 @@ theorem splitUpper_def [DecidableEq ι] {i x} (h : x ∈ Ioo (I.lower i) (I.uppe (forall_update_iff I.lower fun j y => y < I.upper j).2 ⟨h.2, fun j _ => I.lower_lt_upper _⟩) : I.splitUpper i x = (⟨update I.lower i x, I.upper, h'⟩ : Box ι) := by - simp only [splitUpper, mk'_eq_coe, max_eq_left h.1.le, update] + simp only [splitUpper, mk'_eq_coe, max_eq_left h.1.le, update, and_self] #align box_integral.box.split_upper_def BoxIntegral.Box.splitUpper_def theorem disjoint_splitLower_splitUpper (I : Box ι) (i : ι) (x : ℝ) : diff --git a/Mathlib/Analysis/ConstantSpeed.lean b/Mathlib/Analysis/ConstantSpeed.lean index c939c34fae203..46d6c05471fc5 100644 --- a/Mathlib/Analysis/ConstantSpeed.lean +++ b/Mathlib/Analysis/ConstantSpeed.lean @@ -227,7 +227,7 @@ theorem unique_unit_speed_on_Icc_zero {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) rw [← φst] at hf convert unique_unit_speed φm hfφ hf ⟨le_rfl, hs⟩ using 1 have : φ 0 = 0 := by - have hm : 0 ∈ φ '' Icc 0 s := by simp only [mem_Icc, le_refl, ht, φst] + have hm : 0 ∈ φ '' Icc 0 s := by simp only [φst, ht, mem_Icc, le_refl, and_self] obtain ⟨x, xs, hx⟩ := hm apply le_antisymm ((φm ⟨le_rfl, hs⟩ xs xs.1).trans_eq hx) _ have := φst ▸ mapsTo_image φ (Icc 0 s) diff --git a/Mathlib/Analysis/Convex/Between.lean b/Mathlib/Analysis/Convex/Between.lean index f270d72ef9f47..1921785735593 100644 --- a/Mathlib/Analysis/Convex/Between.lean +++ b/Mathlib/Analysis/Convex/Between.lean @@ -611,7 +611,8 @@ theorem sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair [NoZeroSMulDivisors R V] have hu : (Finset.univ : Finset (Fin 3)) = {i₁, i₂, i₃} := by clear h₁ h₂ h₁' h₂' -- Porting note: Originally `decide!` - fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ <;> simp at h₁₂ h₁₃ h₂₃ ⊢ + fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ + <;> simp (config := {decide := true}) at h₁₂ h₁₃ h₂₃ ⊢ have hp : p ∈ affineSpan R (Set.range t.points) := by have hle : line[R, t.points i₁, p₁] ≤ affineSpan R (Set.range t.points) := by refine' affineSpan_pair_le_of_mem_of_mem (mem_affineSpan R (Set.mem_range_self _)) _ diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean index b1767ce282203..b76484f857883 100644 --- a/Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean +++ b/Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean @@ -105,7 +105,7 @@ theorem strictConvexOn_zpow {m : ℤ} (hm₀ : m ≠ 0) (hm₁ : m ≠ 1) : rw [iter_deriv_zpow] refine' mul_pos _ (zpow_pos_of_pos hx _) norm_cast - refine' int_prod_range_pos (by simp only) fun hm => _ + refine' int_prod_range_pos (by decide) fun hm => _ rw [← Finset.coe_Ico] at hm norm_cast at hm fin_cases hm <;> simp_all -- Porting note: `simp_all` was `cc` diff --git a/Mathlib/Analysis/NormedSpace/ProdLp.lean b/Mathlib/Analysis/NormedSpace/ProdLp.lean index ab393528aa5c8..90329943f5a89 100644 --- a/Mathlib/Analysis/NormedSpace/ProdLp.lean +++ b/Mathlib/Analysis/NormedSpace/ProdLp.lean @@ -382,7 +382,7 @@ def prodPseudoMetricAux [PseudoMetricSpace α] [PseudoMetricSpace β] : ← PseudoMetricSpace.edist_dist] exact le_sup_right · refine ENNReal.toReal_le_of_le_ofReal ?_ ?_ - · simp only [ge_iff_le, le_sup_iff, dist_nonneg] + · simp only [ge_iff_le, le_sup_iff, dist_nonneg, or_self] · simp [edist, PseudoMetricSpace.edist_dist, ENNReal.ofReal_le_ofReal] · have h1 : edist f.fst g.fst ^ p.toReal ≠ ⊤ := ENNReal.rpow_ne_top_of_nonneg (zero_le_one.trans h) (edist_ne_top _ _) diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean index 56697c5fb4c4d..af3eb3731f038 100644 --- a/Mathlib/CategoryTheory/Category/Basic.lean +++ b/Mathlib/CategoryTheory/Category/Basic.lean @@ -117,6 +117,7 @@ use in auto-params. macro (name := aesop_cat) "aesop_cat" c:Aesop.tactic_clause* : tactic => `(tactic| aesop $c* (options := { introsTransparency? := some .default, terminal := true }) + (simp_options := { decide := true }) (rule_sets [$(Lean.mkIdent `CategoryTheory):ident])) /-- diff --git a/Mathlib/CategoryTheory/DifferentialObject.lean b/Mathlib/CategoryTheory/DifferentialObject.lean index e52f2713ca2d9..1e2da407c290b 100644 --- a/Mathlib/CategoryTheory/DifferentialObject.lean +++ b/Mathlib/CategoryTheory/DifferentialObject.lean @@ -200,8 +200,8 @@ def mapDifferentialObject (F : C ⥤ D) slice_lhs 2 3 => rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f] slice_lhs 1 2 => rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp] rw [Category.assoc] } - map_id := by intros; ext; simp - map_comp := by intros; ext; simp + map_id := by intros; ext; simp [autoParam] + map_comp := by intros; ext; simp [autoParam] #align category_theory.functor.map_differential_object CategoryTheory.Functor.mapDifferentialObject end Functor diff --git a/Mathlib/CategoryTheory/Elements.lean b/Mathlib/CategoryTheory/Elements.lean index 1b2b79c8817d4..e75472b543473 100644 --- a/Mathlib/CategoryTheory/Elements.lean +++ b/Mathlib/CategoryTheory/Elements.lean @@ -273,7 +273,7 @@ theorem costructuredArrow_yoneda_equivalence_naturality {F₁ F₂ : Cᵒᵖ ⥤ congr ext _ f simpa using congr_fun (α.naturality f.op).symm (unop X).snd - · aesop + · simp [autoParam] #align category_theory.category_of_elements.costructured_arrow_yoneda_equivalence_naturality CategoryTheory.CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality end CategoryOfElements diff --git a/Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean b/Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean index f2a2357610d3e..46a945db9e513 100644 --- a/Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean +++ b/Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean @@ -688,7 +688,7 @@ theorem full_empty : full ∅ = (⊥ : Subgroupoid C) := by @[simp] theorem full_univ : full Set.univ = (⊤ : Subgroupoid C) := by ext - simp only [mem_full_iff, mem_univ, mem_top] + simp only [mem_full_iff, mem_univ, and_self, mem_top] #align category_theory.subgroupoid.full_univ CategoryTheory.Subgroupoid.full_univ theorem full_mono {D E : Set C} (h : D ≤ E) : full D ≤ full E := by diff --git a/Mathlib/CategoryTheory/Sites/Types.lean b/Mathlib/CategoryTheory/Sites/Types.lean index b7d89512addcb..8bda080f4e657 100644 --- a/Mathlib/CategoryTheory/Sites/Types.lean +++ b/Mathlib/CategoryTheory/Sites/Types.lean @@ -191,7 +191,7 @@ theorem typesGrothendieckTopology_eq_canonical : have : (fun _ => ULift.up true) = fun _ => ULift.up false := (hs PUnit fun _ => x).isSeparatedFor.ext fun β f hf => funext fun y => hsx.elim <| S.2 hf fun _ => y - simp at this + simp [Function.funext_iff] at this #align category_theory.types_grothendieck_topology_eq_canonical CategoryTheory.typesGrothendieckTopology_eq_canonical end CategoryTheory diff --git a/Mathlib/Combinatorics/Additive/Behrend.lean b/Mathlib/Combinatorics/Additive/Behrend.lean index c88d0cc6ea789..dd56d00950d95 100644 --- a/Mathlib/Combinatorics/Additive/Behrend.lean +++ b/Mathlib/Combinatorics/Additive/Behrend.lean @@ -213,7 +213,7 @@ theorem sum_lt : (∑ i : Fin n, d * (2 * d + 1) ^ (i : ℕ)) < (2 * d + 1) ^ n theorem card_sphere_le_rothNumberNat (n d k : ℕ) : (sphere n d k).card ≤ rothNumberNat ((2 * d - 1) ^ n) := by cases n - · dsimp; refine' (card_le_univ _).trans_eq _; simp + · dsimp; refine' (card_le_univ _).trans_eq _; rfl cases d · simp refine' addSalemSpencer_image_sphere.le_rothNumberNat _ _ (card_image_of_injOn _) diff --git a/Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean b/Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean index bd302168245f8..0edfa6f513ebf 100644 --- a/Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean +++ b/Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean @@ -59,10 +59,11 @@ theorem IsLowerSet.le_card_inter_finset' (h𝒜 : IsLowerSet (𝒜 : Set (Finset induction' s using Finset.induction with a s hs ih generalizing 𝒜 ℬ · simp_rw [subset_empty, ← subset_singleton_iff', subset_singleton_iff] at h𝒜s hℬs obtain rfl | rfl := h𝒜s - · simp only [card_empty, empty_inter, mul_zero, zero_mul] + · simp only [card_empty, zero_mul, empty_inter, mul_zero, le_refl] obtain rfl | rfl := hℬs - · simp only [card_empty, inter_empty, mul_zero, zero_mul] - · simp only [card_empty, pow_zero, inter_singleton_of_mem, mem_singleton, card_singleton] + · simp only [card_empty, inter_empty, mul_zero, zero_mul, le_refl] + · simp only [card_empty, pow_zero, inter_singleton_of_mem, mem_singleton, card_singleton, + le_refl] rw [card_insert_of_not_mem hs, ← card_memberSubfamily_add_card_nonMemberSubfamily a 𝒜, ← card_memberSubfamily_add_card_nonMemberSubfamily a ℬ, add_mul, mul_add, mul_add, add_comm (_ * _), add_add_add_comm] diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean index 9f3142135f53b..49bd18175f02b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Clique.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Clique.lean @@ -210,7 +210,7 @@ theorem not_cliqueFree_card_of_top_embedding [Fintype α] (f : (⊤ : SimpleGrap theorem cliqueFree_bot (h : 2 ≤ n) : (⊥ : SimpleGraph α).CliqueFree n := by intro t ht have := le_trans h (isNClique_bot_iff.1 ht).1 - simp only at this + contradiction #align simple_graph.clique_free_bot SimpleGraph.cliqueFree_bot theorem CliqueFree.mono (h : m ≤ n) : G.CliqueFree m → G.CliqueFree n := by diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean index b66a6fe5e7a2f..1b4e68eab2a94 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean @@ -72,7 +72,7 @@ local notation3 "a" => (card α / P.parts.card - m * 4 ^ P.parts.card : ℕ) namespace SzemerediRegularity.Positivity private theorem eps_pos {ε : ℝ} {n : ℕ} (h : 100 ≤ (4 : ℝ) ^ n * ε ^ 5) : 0 < ε := - (Odd.pow_pos_iff (by norm_num)).mp + (Odd.pow_pos_iff (by decide)).mp (pos_of_mul_pos_right ((show 0 < (100 : ℝ) by norm_num).trans_le h) (by positivity)) private theorem m_pos [Nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card ≤ card α) : 0 < m := @@ -124,7 +124,7 @@ theorem eps_pow_five_pos (hPε : 100 ≤ (4 : ℝ) ^ P.parts.card * ε ^ 5) : #align szemeredi_regularity.eps_pow_five_pos SzemerediRegularity.eps_pow_five_pos theorem eps_pos (hPε : 100 ≤ (4 : ℝ) ^ P.parts.card * ε ^ 5) : 0 < ε := - (Odd.pow_pos_iff (by norm_num)).mp (eps_pow_five_pos hPε) + (Odd.pow_pos_iff (by decide)).mp (eps_pow_five_pos hPε) #align szemeredi_regularity.eps_pos SzemerediRegularity.eps_pos theorem hundred_div_ε_pow_five_le_m [Nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card ≤ card α) diff --git a/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean b/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean index 8c39f7aa9a2b0..656e03e16d171 100644 --- a/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean +++ b/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean @@ -225,7 +225,8 @@ theorem IsSRGWith.matrix_eq {α : Type*} [Semiring α] (h : G.IsSRGWith n k ℓ simp [commonNeighbors, ← neighborFinset_def, h.regular v] · simp only [Matrix.one_apply_ne' hn.symm, ne_eq, hn] by_cases ha : G.Adj v w <;> - simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one] + simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one, + not_true_eq_false, not_false_eq_true, and_false, and_self] · rw [h.of_adj v w ha] · rw [h.of_not_adj v w hn ha] diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean index 608d67ba074e7..ec26bfaaa6eda 100644 --- a/Mathlib/Combinatorics/Young/YoungDiagram.lean +++ b/Mathlib/Combinatorics/Young/YoungDiagram.lean @@ -499,7 +499,7 @@ theorem rowLens_length_ofRowLens {w : List ℕ} {hw : w.Sorted (· ≥ ·)} (hpo (ofRowLens w hw).rowLens.length = w.length := by simp only [length_rowLens, colLen, Nat.find_eq_iff, mem_cells, mem_ofRowLens, lt_self_iff_false, IsEmpty.exists_iff, Classical.not_not] - refine' ⟨True.intro, fun n hn => ⟨hn, hpos _ (List.get_mem _ _ hn)⟩⟩ + refine' ⟨not_false, fun n hn => ⟨hn, hpos _ (List.get_mem _ _ hn)⟩⟩ #align young_diagram.row_lens_length_of_row_lens YoungDiagram.rowLens_length_ofRowLens -- Porting note: use `List.get` instead of `List.nthLe` because it has been deprecated diff --git a/Mathlib/Computability/Ackermann.lean b/Mathlib/Computability/Ackermann.lean index 6c2fdde4e3475..2a4625465eeec 100644 --- a/Mathlib/Computability/Ackermann.lean +++ b/Mathlib/Computability/Ackermann.lean @@ -101,7 +101,7 @@ theorem ack_three (n : ℕ) : ack 3 n = 2 ^ (n + 3) - 3 := by Nat.mul_sub_left_distrib, ← Nat.sub_add_comm, two_mul 3, Nat.add_sub_add_right] have H : 2 * 3 ≤ 2 * 2 ^ 3 := by norm_num apply H.trans - simp [pow_le_pow] + simp [pow_le_pow (show 1 ≤ 2 by norm_num)] #align ack_three ack_three theorem ack_pos : ∀ m n, 0 < ack m n diff --git a/Mathlib/Computability/Halting.lean b/Mathlib/Computability/Halting.lean index 2a513d73756e4..9f60ef77c8412 100644 --- a/Mathlib/Computability/Halting.lean +++ b/Mathlib/Computability/Halting.lean @@ -378,7 +378,7 @@ theorem rfindOpt {n} {f : Vector ℕ (n + 1) → ℕ} (hf : @Partrec' (n + 1) f) exists_congr fun a => (and_congr (iff_of_eq _) Iff.rfl).trans (and_congr_right fun h => _) · congr funext n - cases f (n ::ᵥ v) <;> simp [Nat.succ_le_succ]; rfl + cases f (n ::ᵥ v) <;> simp [Nat.succ_le_succ] <;> rfl · have := Nat.rfind_spec h simp only [Part.coe_some, Part.mem_some_iff] at this revert this; cases' f (a ::ᵥ v) with c <;> intro this diff --git a/Mathlib/Computability/Primrec.lean b/Mathlib/Computability/Primrec.lean index fd573c762d535..5edab43f57ebe 100644 --- a/Mathlib/Computability/Primrec.lean +++ b/Mathlib/Computability/Primrec.lean @@ -837,7 +837,7 @@ theorem nat_mod : Primrec₂ ((· % ·) : ℕ → ℕ → ℕ) := theorem nat_bodd : Primrec Nat.bodd := (Primrec.beq.comp (nat_mod.comp .id (const 2)) (const 1)).of_eq fun n => by - cases H : n.bodd <;> simp [Nat.mod_two_of_bodd, H] + cases H : n.bodd <;> simp [Nat.mod_two_of_bodd, H]; rfl #align primrec.nat_bodd Primrec.nat_bodd theorem nat_div2 : Primrec Nat.div2 := diff --git a/Mathlib/Computability/TMComputable.lean b/Mathlib/Computability/TMComputable.lean index d414d6d2a6bf7..a79be2891b674 100644 --- a/Mathlib/Computability/TMComputable.lean +++ b/Mathlib/Computability/TMComputable.lean @@ -260,7 +260,7 @@ def idComputableInPolyTime {α : Type} (ea : FinEncoding α) : outputsFun _ := { steps := 1 evals_in_steps := rfl - steps_le_m := by simp only [Polynomial.eval_one] } + steps_le_m := by simp only [Polynomial.eval_one, le_refl] } #align turing.id_computable_in_poly_time Turing.idComputableInPolyTime instance inhabitedTM2ComputableInPolyTime : diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean index 2c3872c83fc5f..d16613bcbfc9c 100644 --- a/Mathlib/Computability/TMToPartrec.lean +++ b/Mathlib/Computability/TMToPartrec.lean @@ -1536,7 +1536,7 @@ theorem succ_ok {q s n} {c d : List Γ'} : simp only [Option.mem_def, TM2.stepAux, elim_main, decide_False, elim_update_main, ne_eq, Function.update_noteq, elim_rev, elim_update_rev, decide_True, Function.update_same, cond_true, cond_false] - convert unrev_ok using 2 + convert unrev_ok using 1 simp only [elim_update_rev, elim_rev, elim_main, List.reverseAux_nil, elim_update_main] rfl simp only [trNum, Num.succ, Num.succ'] diff --git a/Mathlib/Data/Bitvec/Lemmas.lean b/Mathlib/Data/Bitvec/Lemmas.lean index bc995d403f452..9e961fabc48f9 100644 --- a/Mathlib/Data/Bitvec/Lemmas.lean +++ b/Mathlib/Data/Bitvec/Lemmas.lean @@ -102,7 +102,7 @@ theorem toNat_lt {n : ℕ} (v : Bitvec n) : v.toNat < 2 ^ n := by -- Porting note: removed `ac_mono`, `mono` calls · rw [add_assoc] apply Nat.add_le_add_left - cases head <;> simp only + cases head <;> decide · rw [← left_distrib] rw [mul_comm _ 2] apply Nat.mul_le_mul_left @@ -112,14 +112,14 @@ theorem toNat_lt {n : ℕ} (v : Bitvec n) : v.toNat < 2 ^ n := by theorem addLsb_div_two {x b} : addLsb x b / 2 = x := by cases b <;> simp only [Nat.add_mul_div_left, addLsb, ← two_mul, add_comm, Nat.succ_pos', - Nat.mul_div_right, gt_iff_lt, zero_add, cond] + Nat.mul_div_right, gt_iff_lt, zero_add, zero_lt_two, cond] norm_num #align bitvec.add_lsb_div_two Bitvec.addLsb_div_two theorem decide_addLsb_mod_two {x b} : decide (addLsb x b % 2 = 1) = b := by cases b <;> simp only [Bool.decide_iff, Nat.add_mul_mod_self_left, addLsb, ← two_mul, add_comm, - Bool.decide_False, Nat.mul_mod_right, zero_add, cond, zero_ne_one] + Bool.decide_False, Nat.mul_mod_right, zero_add, cond, zero_ne_one]; rfl #align bitvec.to_bool_add_lsb_mod_two Bitvec.decide_addLsb_mod_two theorem ofNat_toNat {n : ℕ} (v : Bitvec n) : Bitvec.ofNat n v.toNat = v := by diff --git a/Mathlib/Data/Bool/Basic.lean b/Mathlib/Data/Bool/Basic.lean index aef4a844fb172..28b4753db3afc 100644 --- a/Mathlib/Data/Bool/Basic.lean +++ b/Mathlib/Data/Bool/Basic.lean @@ -323,7 +323,7 @@ theorem ofNat_le_ofNat {n m : Nat} (h : n ≤ m) : ofNat n ≤ ofNat m := by #align bool.of_nat_le_of_nat Bool.ofNat_le_ofNat theorem toNat_le_toNat {b₀ b₁ : Bool} (h : b₀ ≤ b₁) : toNat b₀ ≤ toNat b₁ := by - cases b₀ <;> cases b₁ <;> simp_all + cases b₀ <;> cases b₁ <;> simp_all (config := { decide := true }) #align bool.to_nat_le_to_nat Bool.toNat_le_toNat theorem ofNat_toNat (b : Bool) : ofNat (toNat b) = b := by diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean index fcb273d3dc9bb..bcb95ce0da54e 100644 --- a/Mathlib/Data/ENat/Basic.lean +++ b/Mathlib/Data/ENat/Basic.lean @@ -149,13 +149,17 @@ theorem coe_ne_top (a : ℕ) : (a : ℕ∞) ≠ ⊤ := theorem top_sub_coe (a : ℕ) : (⊤ : ℕ∞) - a = ⊤ := WithTop.top_sub_coe +@[simp] +theorem zero_lt_top : (0 : ℕ∞) < ⊤ := + WithTop.zero_lt_top + --Porting note: new theorem copied from `WithTop` theorem sub_top (a : ℕ∞) : a - ⊤ = 0 := WithTop.sub_top @[simp] theorem coe_toNat_eq_self : ENat.toNat (n : ℕ∞) = n ↔ n ≠ ⊤ := - ENat.recTopCoe (by simp) (fun _ => by simp [toNat_coe]) n + ENat.recTopCoe (by decide) (fun _ => by simp [toNat_coe]) n #align enat.coe_to_nat_eq_self ENat.coe_toNat_eq_self alias ⟨_, coe_toNat⟩ := coe_toNat_eq_self diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index 70f851cbbc952..65a13ab0d8f95 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -506,7 +506,7 @@ theorem val_one'' {n : ℕ} : ((1 : Fin (n + 1)) : ℕ) = 1 % (n + 1) := #align fin.mk_one Fin.mk_one instance nontrivial {n : ℕ} : Nontrivial (Fin (n + 2)) where - exists_pair_ne := ⟨0, 1, (ne_iff_vne 0 1).mpr (by simp only [val_one, val_zero])⟩ + exists_pair_ne := ⟨0, 1, (ne_iff_vne 0 1).mpr (by simp [val_one, val_zero])⟩ theorem nontrivial_iff_two_le : Nontrivial (Fin n) ↔ 2 ≤ n := by rcases n with (_ | _ | n) <;> @@ -1219,7 +1219,7 @@ theorem coe_fin_one (a : Fin 1) : (a : ℕ) = 0 := by simp [Subsingleton.elim a #align fin.coe_fin_one Fin.coe_fin_one lemma eq_one_of_neq_zero (i : Fin 2) (hi : i ≠ 0) : i = 1 := - fin_two_eq_of_eq_zero_iff (by simpa only [iff_false] using hi) + fin_two_eq_of_eq_zero_iff (by simpa only [one_eq_zero_iff, succ.injEq, iff_false] using hi) @[simp] theorem coe_neg_one : ↑(-1 : Fin (n + 1)) = n := by @@ -1268,7 +1268,7 @@ theorem coe_sub_iff_lt {n : ℕ} {a b : Fin n} : (↑(a - b) : ℕ) = n + a - b theorem lt_sub_one_iff {n : ℕ} {k : Fin (n + 2)} : k < k - 1 ↔ k = 0 := by rcases k with ⟨_ | k, hk⟩ simp only [zero_eq, zero_eta, zero_sub, lt_iff_val_lt_val, val_zero, coe_neg_one, add_pos_iff, - or_true] + _root_.zero_lt_one, or_true] have : (k + 1 + (n + 1)) % (n + 2) = k % (n + 2) := by rw [add_right_comm, add_assoc, add_mod_right] simp [lt_iff_val_lt_val, ext_iff, Fin.coe_sub, succ_eq_add_one, this, diff --git a/Mathlib/Data/Fin/Tuple/Monotone.lean b/Mathlib/Data/Fin/Tuple/Monotone.lean index 7c48630f7e14b..51d4c6d892045 100644 --- a/Mathlib/Data/Fin/Tuple/Monotone.lean +++ b/Mathlib/Data/Fin/Tuple/Monotone.lean @@ -38,12 +38,12 @@ theorem monotone_vecCons : Monotone (vecCons a f) ↔ a ≤ f 0 ∧ Monotone f : --Porting note: new lemma, in Lean3 would be proven by `Subsingleton.monotone` @[simp] -theorem monotone_vecEmpty : Monotone (vecCons a vecEmpty) +theorem monotone_vecEmpty : Monotone ![a] | ⟨0, _⟩, ⟨0, _⟩, _ => le_refl _ --Porting note: new lemma, in Lean3 would be proven by `Subsingleton.strictMono` @[simp] -theorem strictMono_vecEmpty : StrictMono (vecCons a vecEmpty) +theorem strictMono_vecEmpty : StrictMono ![a] | ⟨0, _⟩, ⟨0, _⟩, h => (irrefl _ h).elim @[simp] @@ -82,4 +82,5 @@ theorem Antitone.vecCons (hf : Antitone f) (ha : f 0 ≤ a) : Antitone (vecCons antitone_vecCons.2 ⟨ha, hf⟩ #align antitone.vec_cons Antitone.vecCons -example : Monotone ![1, 2, 2, 3] := by simp +-- NOTE: was "by simp", but simp lemmas were not being used +example : Monotone ![1, 2, 2, 3] := by decide diff --git a/Mathlib/Data/Finsupp/Defs.lean b/Mathlib/Data/Finsupp/Defs.lean index 1e0c9ef129aa3..7c5010e102a41 100644 --- a/Mathlib/Data/Finsupp/Defs.lean +++ b/Mathlib/Data/Finsupp/Defs.lean @@ -835,7 +835,7 @@ def embDomain (f : α ↪ β) (v : α →₀ M) : β →₀ M where · simp only [h, true_iff_iff, Ne.def] rw [← not_mem_support_iff, not_not] classical apply Finset.choose_mem - · simp only [h, Ne.def, ne_self_iff_false] + · simp only [h, Ne.def, ne_self_iff_false, not_true_eq_false] #align finsupp.emb_domain Finsupp.embDomain @[simp] diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean index 5df6f41d88edc..b39481fe6a610 100644 --- a/Mathlib/Data/Int/Bitwise.lean +++ b/Mathlib/Data/Int/Bitwise.lean @@ -53,7 +53,7 @@ theorem bodd_subNatNat (m n : ℕ) : bodd (subNatNat m n) = xor m.bodd n.bodd := @[simp] theorem bodd_negOfNat (n : ℕ) : bodd (negOfNat n) = n.bodd := by - cases n <;> simp + cases n <;> simp (config := {decide := true}) rfl #align int.bodd_neg_of_nat Int.bodd_negOfNat @@ -164,7 +164,7 @@ theorem bit_negSucc (b) (n : ℕ) : bit b -[n+1] = -[Nat.bit (not b) n+1] := by @[simp] theorem bodd_bit (b n) : bodd (bit b n) = b := by rw [bit_val] - cases b <;> cases bodd n <;> simp + cases b <;> cases bodd n <;> simp [(show bodd 2 = false by rfl)] #align int.bodd_bit Int.bodd_bit @[simp, deprecated] @@ -293,12 +293,12 @@ theorem bitwise_xor : bitwise xor = Int.xor := by theorem bitwise_bit (f : Bool → Bool → Bool) (a m b n) : bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) := by cases' m with m m <;> cases' n with n n <;> - simp only [bitwise, ofNat_eq_coe, bit_coe_nat, natBitwise, Bool.not_false, Bool.not_eq_false', + simp [bitwise, ofNat_eq_coe, bit_coe_nat, natBitwise, Bool.not_false, Bool.not_eq_false', bit_negSucc] - · by_cases h : f false false <;> simp [h] - · by_cases h : f false true <;> simp [h] - · by_cases h : f true false <;> simp [h] - · by_cases h : f true true <;> simp [h] + · by_cases h : f false false <;> simp (config := {decide := true}) [h] + · by_cases h : f false true <;> simp (config := {decide := true}) [h] + · by_cases h : f true false <;> simp (config := {decide := true}) [h] + · by_cases h : f true true <;> simp (config := {decide := true}) [h] #align int.bitwise_bit Int.bitwise_bit @[simp] diff --git a/Mathlib/Data/Int/Lemmas.lean b/Mathlib/Data/Int/Lemmas.lean index 55d5ca346a1af..5fa5f5943d0b9 100644 --- a/Mathlib/Data/Int/Lemmas.lean +++ b/Mathlib/Data/Int/Lemmas.lean @@ -122,7 +122,7 @@ attribute [local simp] Int.zero_div theorem div2_bit (b n) : div2 (bit b n) = n := by rw [bit_val, div2_val, add_comm, Int.add_mul_ediv_left, (_ : (_ / 2 : ℤ) = 0), zero_add] cases b - · simp + · decide · show ofNat _ = _ rw [Nat.div_eq_of_lt] <;> simp · decide diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean index a446a520cd44c..b0b3171818481 100644 --- a/Mathlib/Data/Int/ModEq.lean +++ b/Mathlib/Data/Int/ModEq.lean @@ -129,7 +129,7 @@ protected theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n obtain hc | rfl | hc := lt_trichotomy c 0 · rw [← neg_modEq_neg, ← modEq_neg, ← neg_mul, ← neg_mul, ← neg_mul] simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq] - · simp + · simp only [zero_mul]; rfl · simp only [ModEq, mul_emod_mul_of_pos _ _ hc, h.eq] #align int.modeq.mul_left' Int.ModEq.mul_left' diff --git a/Mathlib/Data/Int/Parity.lean b/Mathlib/Data/Int/Parity.lean index 6965c6a9c0470..d1961d01dd35f 100644 --- a/Mathlib/Data/Int/Parity.lean +++ b/Mathlib/Data/Int/Parity.lean @@ -27,6 +27,9 @@ theorem emod_two_ne_one : ¬n % 2 = 1 ↔ n % 2 = 0 := by cases' emod_two_eq_zero_or_one n with h h <;> simp [h] #align int.mod_two_ne_one Int.emod_two_ne_one +@[simp] +theorem one_emod_two : (1 : Int) % 2 = 1 := rfl + -- `EuclideanDomain.mod_eq_zero` uses (2 ∣ n) as normal form @[local simp] theorem emod_two_ne_zero : ¬n % 2 = 0 ↔ n % 2 = 1 := by @@ -102,6 +105,7 @@ theorem even_add : Even (m + n) ↔ (Even m ↔ Even n) := by cases' emod_two_eq_zero_or_one m with h₁ h₁ <;> cases' emod_two_eq_zero_or_one n with h₂ h₂ <;> simp [even_iff, h₁, h₂, Int.add_emod] + rfl #align int.even_add Int.even_add theorem even_add' : Even (m + n) ↔ (Odd m ↔ Odd n) := by @@ -279,8 +283,8 @@ theorem two_mul_ediv_two_of_odd (h : Odd n) : 2 * (n / 2) = n - 1 := -- Here are examples of how `parity_simps` can be used with `Int`. example (m n : ℤ) (h : Even m) : ¬Even (n + 3) ↔ Even (m ^ 2 + m + n) := by - simp [*, (by decide : ¬2 = 0), parity_simps] + simp (config := {decide := true}) [*, (by decide : ¬2 = 0), parity_simps] -example : ¬Even (25394535 : ℤ) := by simp +example : ¬Even (25394535 : ℤ) := by decide end Int diff --git a/Mathlib/Data/Int/Range.lean b/Mathlib/Data/Int/Range.lean index 91905365d8e9e..cc7e2b9ac47e1 100644 --- a/Mathlib/Data/Int/Range.lean +++ b/Mathlib/Data/Int/Range.lean @@ -49,7 +49,7 @@ instance decidableLELE (P : Int → Prop) [DecidablePred P] (m n : ℤ) : apply decidable_of_iff (∀ r ∈ range m (n + 1), P r) apply Iff.intro <;> intros h _ _ · intro _; apply h - simp_all only [mem_range_iff, and_imp, lt_add_one_iff] + simp_all only [mem_range_iff, and_imp, and_self, lt_add_one_iff] · simp_all only [mem_range_iff, and_imp, lt_add_one_iff] #align int.decidable_le_le Int.decidableLELE diff --git a/Mathlib/Data/Int/Units.lean b/Mathlib/Data/Int/Units.lean index 8667113994db0..5a69a99b1033f 100644 --- a/Mathlib/Data/Int/Units.lean +++ b/Mathlib/Data/Int/Units.lean @@ -122,7 +122,7 @@ theorem isUnit_add_isUnit_eq_isUnit_add_isUnit {a b c d : ℤ} (ha : IsUnit a) ( rw [isUnit_iff] at ha hb hc hd cases ha <;> cases hb <;> cases hc <;> cases hd <;> subst a <;> subst b <;> subst c <;> subst d <;> - simp + simp (config := {decide := true}) #align int.is_unit_add_is_unit_eq_is_unit_add_is_unit Int.isUnit_add_isUnit_eq_isUnit_add_isUnit theorem eq_one_or_neg_one_of_mul_eq_neg_one {z w : ℤ} (h : z * w = -1) : z = 1 ∨ z = -1 := diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 561d2d79515e8..35988ef5c14d4 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -2576,7 +2576,7 @@ theorem nthLe_succ_scanl {i : ℕ} {h : i + 1 < (scanl f b l).length} : induction i generalizing b l with | zero => cases l - · simp only [length, zero_add, scanl_nil] at h + · simp only [length, zero_eq, lt_self_iff_false] at h · simp [scanl_cons, singleton_append, nthLe_zero_scanl, nthLe_cons] | succ i hi => cases l @@ -3331,7 +3331,7 @@ theorem reduceOption_map {l : List (Option α)} {f : α → β} : reduceOption (map (Option.map f) l) = map f (reduceOption l) := by induction' l with hd tl hl · simp only [reduceOption_nil, map_nil] - ·cases hd <;> + · cases hd <;> simpa [true_and_iff, Option.map_some', map, eq_self_iff_true, reduceOption_cons_of_some] using hl #align list.reduce_option_map List.reduceOption_map @@ -3343,7 +3343,7 @@ theorem reduceOption_append (l l' : List (Option α)) : theorem reduceOption_length_le (l : List (Option α)) : l.reduceOption.length ≤ l.length := by induction' l with hd tl hl - · simp only [reduceOption_nil, length] + · simp [reduceOption_nil, length] · cases hd · exact Nat.le_succ_of_le hl · simpa only [length, add_le_add_iff_right, reduceOption_cons_of_some] using hl diff --git a/Mathlib/Data/List/BigOperators/Basic.lean b/Mathlib/Data/List/BigOperators/Basic.lean index 1c71ebd5a4233..a74654f436114 100644 --- a/Mathlib/Data/List/BigOperators/Basic.lean +++ b/Mathlib/Data/List/BigOperators/Basic.lean @@ -594,7 +594,7 @@ If desired, we could add a class stating that `default = 0`. /-- This relies on `default ℕ = 0`. -/ theorem headI_add_tail_sum (L : List ℕ) : L.headI + L.tail.sum = L.sum := by - cases L <;> simp + cases L <;> simp; rfl #align list.head_add_tail_sum List.headI_add_tail_sum /-- This relies on `default ℕ = 0`. -/ diff --git a/Mathlib/Data/List/Chain.lean b/Mathlib/Data/List/Chain.lean index 24ac55928b814..368b6cdf504f9 100644 --- a/Mathlib/Data/List/Chain.lean +++ b/Mathlib/Data/List/Chain.lean @@ -354,7 +354,7 @@ theorem chain'_iff_get {R} : ∀ {l : List α}, Chain' R l ↔ rw [← and_forall_succ, chain'_cons, chain'_iff_get] simp only [length_cons, get_cons_succ, Fin.zero_eta, get_cons_zero, zero_add, Fin.mk_one, get_cons_cons_one, succ_sub_succ_eq_sub, nonpos_iff_eq_zero, add_eq_zero_iff, and_false, - tsub_zero, add_pos_iff, or_true, forall_true_left, and_congr_right_iff] + tsub_zero, add_pos_iff, zero_lt_one, or_true, forall_true_left, and_congr_right_iff] dsimp [succ_sub_one] exact fun _ => ⟨fun h i hi => h i (Nat.lt_of_succ_lt_succ hi), fun h i hi => h i (Nat.succ_lt_succ hi)⟩ diff --git a/Mathlib/Data/List/Infix.lean b/Mathlib/Data/List/Infix.lean index 6eb0edaea1148..854bb961d43f4 100644 --- a/Mathlib/Data/List/Infix.lean +++ b/Mathlib/Data/List/Infix.lean @@ -259,7 +259,7 @@ theorem prefix_take_le_iff {L : List (List (Option α))} (hm : m < L.length) : | zero => refine' iff_of_false _ (zero_lt_succ _).not_le rw [take_zero, take_nil] - simp only [take] + simp only [take, not_false_eq_true] | succ n => simp only [length] at hm have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm) diff --git a/Mathlib/Data/List/Intervals.lean b/Mathlib/Data/List/Intervals.lean index 25136a1b3a160..a8fb8984e4e69 100644 --- a/Mathlib/Data/List/Intervals.lean +++ b/Mathlib/Data/List/Intervals.lean @@ -45,17 +45,17 @@ theorem zero_bot (n : ℕ) : Ico 0 n = range n := by rw [Ico, tsub_zero, range_e @[simp] theorem length (n m : ℕ) : length (Ico n m) = m - n := by dsimp [Ico] - simp only [length_range'] + simp [length_range', autoParam] #align list.Ico.length List.Ico.length theorem pairwise_lt (n m : ℕ) : Pairwise (· < ·) (Ico n m) := by dsimp [Ico] - simp only [pairwise_lt_range'] + simp [pairwise_lt_range', autoParam] #align list.Ico.pairwise_lt List.Ico.pairwise_lt theorem nodup (n m : ℕ) : Nodup (Ico n m) := by dsimp [Ico] - simp only [nodup_range'] + simp [nodup_range', autoParam] #align list.Ico.nodup List.Ico.nodup @[simp] diff --git a/Mathlib/Data/List/Lattice.lean b/Mathlib/Data/List/Lattice.lean index 5902bcaca37ad..b442e56bd2580 100644 --- a/Mathlib/Data/List/Lattice.lean +++ b/Mathlib/Data/List/Lattice.lean @@ -134,12 +134,12 @@ theorem inter_nil (l : List α) : [] ∩ l = [] := @[simp] theorem inter_cons_of_mem (l₁ : List α) (h : a ∈ l₂) : (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂ := by - simp only [Inter.inter, List.inter, filter_cons_of_pos, h] + simp [Inter.inter, List.inter, h] #align list.inter_cons_of_mem List.inter_cons_of_mem @[simp] theorem inter_cons_of_not_mem (l₁ : List α) (h : a ∉ l₂) : (a :: l₁) ∩ l₂ = l₁ ∩ l₂ := by - simp only [Inter.inter, List.inter, filter_cons_of_neg, h] + simp [Inter.inter, List.inter, h] #align list.inter_cons_of_not_mem List.inter_cons_of_not_mem theorem mem_of_mem_inter_left : a ∈ l₁ ∩ l₂ → a ∈ l₁ := diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean index dd1dc5d18d635..2f0bb734d5b3c 100644 --- a/Mathlib/Data/List/Perm.lean +++ b/Mathlib/Data/List/Perm.lean @@ -275,9 +275,11 @@ theorem filter_append_perm (p : α → Bool) (l : List α) : induction' l with x l ih · rfl · by_cases h : p x - · simp only [h, filter_cons_of_pos, filter_cons_of_neg, not_true, not_false_iff, cons_append] + · simp only [h, filter_cons_of_pos, filter_cons_of_neg, not_true, not_false_iff, cons_append, + decide_False] exact ih.cons x - · simp only [h, filter_cons_of_neg, not_false_iff, filter_cons_of_pos] + · simp only [h, filter_cons_of_neg, not_false_iff, filter_cons_of_pos, cons_append, + not_false_eq_true, decide_True] refine' Perm.trans _ (ih.cons x) exact perm_append_comm.trans (perm_append_comm.cons _) #align list.filter_append_perm List.filter_append_perm diff --git a/Mathlib/Data/List/Range.lean b/Mathlib/Data/List/Range.lean index 3825116af5511..16942639d2398 100644 --- a/Mathlib/Data/List/Range.lean +++ b/Mathlib/Data/List/Range.lean @@ -76,14 +76,15 @@ theorem nthLe_range'_1 {n m} (i) (H : i < (range' n m).length) : #align list.range_eq_nil List.range_eq_nil theorem pairwise_lt_range (n : ℕ) : Pairwise (· < ·) (range n) := by - simp only [range_eq_range', pairwise_lt_range'] + simp (config := {decide := true}) only [range_eq_range', pairwise_lt_range'] #align list.pairwise_lt_range List.pairwise_lt_range theorem pairwise_le_range (n : ℕ) : Pairwise (· ≤ ·) (range n) := Pairwise.imp (@le_of_lt ℕ _) (pairwise_lt_range _) #align list.pairwise_le_range List.pairwise_le_range -theorem nodup_range (n : ℕ) : Nodup (range n) := by simp only [range_eq_range', nodup_range'] +theorem nodup_range (n : ℕ) : Nodup (range n) := by + simp (config := {decide := true}) only [range_eq_range', nodup_range'] #align list.nodup_range List.nodup_range #align list.range_sublist List.range_sublist #align list.range_subset List.range_subset diff --git a/Mathlib/Data/List/Rdrop.lean b/Mathlib/Data/List/Rdrop.lean index f91c332d0f803..ab4856e998b08 100644 --- a/Mathlib/Data/List/Rdrop.lean +++ b/Mathlib/Data/List/Rdrop.lean @@ -229,10 +229,10 @@ theorem rtakeWhile_eq_nil_iff : rtakeWhile p l = [] ↔ ∀ hl : l ≠ [], ¬p ( · simp only [rtakeWhile, takeWhile, reverse_nil, true_iff] intro f; contradiction · simp only [rtakeWhile, reverse_append, takeWhile, reverse_eq_nil, getLast_append, ne_eq, - append_eq_nil, and_false, forall_true_left] + append_eq_nil, and_false, not_false_eq_true, forall_true_left] refine' ⟨fun h => _ , fun h => _⟩ - · intro pa; simp only [pa] at h - · simp only [h] + · intro pa; simp [pa] at h + · simp [h] #align list.rtake_while_eq_nil_iff List.rtakeWhile_eq_nil_iff theorem mem_rtakeWhile_imp {x : α} (hx : x ∈ rtakeWhile p l) : p x := by diff --git a/Mathlib/Data/MvPolynomial/Division.lean b/Mathlib/Data/MvPolynomial/Division.lean index b7ddacdc2f8bd..634ae6990b14a 100644 --- a/Mathlib/Data/MvPolynomial/Division.lean +++ b/Mathlib/Data/MvPolynomial/Division.lean @@ -232,8 +232,8 @@ theorem monomial_dvd_monomial {r s : R} {i j : σ →₀ ℕ} : · exact ⟨Or.inr hi, _, hj⟩ · exact ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩ -- Porting note: two goals remain at this point in Lean 4 - · simp_all only [or_true, dvd_mul_right] - · simp_all only [ite_self, le_refl, ite_true, dvd_mul_right] + · simp_all only [or_true, dvd_mul_right, and_self] + · simp_all only [ite_self, le_refl, ite_true, dvd_mul_right, or_false, and_self] · rintro ⟨h | hij, d, rfl⟩ · simp_rw [h, monomial_zero, dvd_zero] · refine' ⟨monomial (j - i) d, _⟩ @@ -252,7 +252,7 @@ theorem X_dvd_X [Nontrivial R] {i j : σ} : (X i : MvPolynomial σ R) ∣ (X j : MvPolynomial σ R) ↔ i = j := by refine' monomial_one_dvd_monomial_one.trans _ simp_rw [Finsupp.single_le_iff, Nat.one_le_iff_ne_zero, Finsupp.single_apply_ne_zero, - and_true_iff] + ne_eq, not_false_eq_true, and_true] set_option linter.uppercaseLean3 false in #align mv_polynomial.X_dvd_X MvPolynomial.X_dvd_X diff --git a/Mathlib/Data/MvPolynomial/Variables.lean b/Mathlib/Data/MvPolynomial/Variables.lean index b63a5e3b788b1..d6c217d4fe3c1 100644 --- a/Mathlib/Data/MvPolynomial/Variables.lean +++ b/Mathlib/Data/MvPolynomial/Variables.lean @@ -686,7 +686,7 @@ theorem totalDegree_smul_le [CommSemiring S] [DistribMulAction R S] (a : R) (f : theorem totalDegree_pow (a : MvPolynomial σ R) (n : ℕ) : (a ^ n).totalDegree ≤ n * a.totalDegree := by induction' n with n ih - · simp only [Nat.zero_eq, zero_mul, pow_zero, totalDegree_one] + · simp only [Nat.zero_eq, pow_zero, totalDegree_one, zero_mul, le_refl] rw [pow_succ] calc totalDegree (a * a ^ n) ≤ a.totalDegree + (a ^ n).totalDegree := totalDegree_mul _ _ diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean index e42b6dab81436..673f89a0cec19 100644 --- a/Mathlib/Data/Nat/Bitwise.lean +++ b/Mathlib/Data/Nat/Bitwise.lean @@ -86,8 +86,9 @@ lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by have h1 x : (x + x) % 2 = 0 := by rw [← two_mul, mul_comm]; apply mul_mod_left have h2 x : (x + x + 1) % 2 = 1 := by rw [← two_mul, add_comm]; apply add_mul_mod_self_left have h3 x : (x + x) / 2 = x := by rw [← two_mul, mul_comm]; apply mul_div_left _ zero_lt_two - have h4 x : (x + x + 1) / 2 = x := by rw [← two_mul, add_comm]; simp [add_mul_div_left] - cases a <;> cases b <;> simp [h1, h2, h3, h4] <;> split_ifs <;> simp_all + have h4 x : (x + x + 1) / 2 = x := by rw [← two_mul, add_comm]; simp [add_mul_div_left]; rfl + cases a <;> cases b <;> simp [h1, h2, h3, h4] <;> split_ifs + <;> simp_all (config := {decide := true}) #align nat.bitwise_bit Nat.bitwise_bit lemma bit_mod_two (a : Bool) (x : ℕ) : @@ -304,6 +305,7 @@ theorem testBit_two_pow_of_ne {n m : ℕ} (hm : n ≠ m) : testBit (2 ^ n) m = f rw [(rfl : succ 0 = 1)] simp only [ge_iff_le, tsub_le_iff_right, pow_succ, bodd_mul, Bool.and_eq_false_eq_eq_false_or_eq_false, or_true] + exact Or.inr rfl #align nat.test_bit_two_pow_of_ne Nat.testBit_two_pow_of_ne theorem testBit_two_pow (n m : ℕ) : testBit (2 ^ n) m = (n = m) := by @@ -349,8 +351,7 @@ theorem xor_comm (n m : ℕ) : n ^^^ m = m ^^^ n := #align nat.lxor_comm Nat.xor_comm @[simp] -theorem zero_xor (n : ℕ) : 0 ^^^ n = n := by - simp only [HXor.hXor, Xor.xor, xor, bitwise_zero_left, ite_true] +theorem zero_xor (n : ℕ) : 0 ^^^ n = n := by simp [HXor.hXor, Xor.xor, xor] #align nat.zero_lxor Nat.zero_xor @[simp] @@ -359,22 +360,22 @@ theorem xor_zero (n : ℕ) : n ^^^ 0 = n := by simp [HXor.hXor, Xor.xor, xor] @[simp] theorem zero_land (n : ℕ) : 0 &&& n = 0 := by - simp only [HAnd.hAnd, AndOp.and, land, bitwise_zero_left, ite_false]; + simp only [HAnd.hAnd, AndOp.and, land, bitwise_zero_left, ite_false, Bool.and_true]; #align nat.zero_land Nat.zero_land @[simp] theorem land_zero (n : ℕ) : n &&& 0 = 0 := by - simp only [HAnd.hAnd, AndOp.and, land, bitwise_zero_right, ite_false] + simp only [HAnd.hAnd, AndOp.and, land, bitwise_zero_right, ite_false, Bool.and_false] #align nat.land_zero Nat.land_zero @[simp] theorem zero_lor (n : ℕ) : 0 ||| n = n := by - simp only [HOr.hOr, OrOp.or, lor, bitwise_zero_left, ite_true] + simp only [HOr.hOr, OrOp.or, lor, bitwise_zero_left, ite_true, Bool.or_true] #align nat.zero_lor Nat.zero_lor @[simp] theorem lor_zero (n : ℕ) : n ||| 0 = n := by - simp only [HOr.hOr, OrOp.or, lor, bitwise_zero_right, ite_true] + simp only [HOr.hOr, OrOp.or, lor, bitwise_zero_right, ite_true, Bool.or_false] #align nat.lor_zero Nat.lor_zero diff --git a/Mathlib/Data/Nat/Choose/Multinomial.lean b/Mathlib/Data/Nat/Choose/Multinomial.lean index e36fa5b43e1c2..9f2ec24bf3956 100644 --- a/Mathlib/Data/Nat/Choose/Multinomial.lean +++ b/Mathlib/Data/Nat/Choose/Multinomial.lean @@ -126,7 +126,7 @@ theorem binomial_succ_succ [DecidableEq α] (h : a ≠ b) : multinomial {a, b} (Function.update f a (f a).succ) + multinomial {a, b} (Function.update f b (f b).succ) := by simp only [binomial_eq_choose, Function.update_apply, - h, Ne.def, ite_true, ite_false] + h, Ne.def, ite_true, ite_false, not_false_eq_true] rw [if_neg h.symm] rw [add_succ, choose_succ_succ, succ_add_eq_succ_add] ring diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean index 6bd1fa22bab23..5a25728bd1a40 100644 --- a/Mathlib/Data/Nat/Digits.lean +++ b/Mathlib/Data/Nat/Digits.lean @@ -357,6 +357,7 @@ theorem getLast_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) : · cases hm rfl rename ℕ => m simp only [digits_one, List.getLast_replicate_succ m 1] + exact Nat.one_ne_zero revert hm apply Nat.strongInductionOn m intro n IH hn @@ -569,7 +570,7 @@ theorem sub_one_mul_sum_div_pow_eq_sub_sum_digits · simp [ofDigits_one] · simp [lt_one_iff.mp h] cases L - · simp + · rfl · simp [ofDigits] theorem sub_one_mul_sum_log_div_pow_eq_sub_sum_digits (n : ℕ) : @@ -592,7 +593,7 @@ theorem sub_one_mul_sum_log_div_pow_eq_sub_sum_digits (n : ℕ) : theorem digits_two_eq_bits (n : ℕ) : digits 2 n = n.bits.map fun b => cond b 1 0 := by induction' n using Nat.binaryRecFromOne with b n h ih · simp - · simp + · rfl rw [bits_append_bit _ _ fun hn => absurd hn h] cases b · rw [digits_def' one_lt_two] @@ -689,7 +690,7 @@ theorem ofDigits_neg_one : theorem modEq_eleven_digits_sum (n : ℕ) : n ≡ ((digits 10 n).map fun n : ℕ => (n : ℤ)).alternatingSum [ZMOD 11] := by - have t := zmodeq_ofDigits_digits 11 10 (-1 : ℤ) (by unfold Int.ModEq; norm_num) n + have t := zmodeq_ofDigits_digits 11 10 (-1 : ℤ) (by unfold Int.ModEq; rfl) n rwa [ofDigits_neg_one] at t #align nat.modeq_eleven_digits_sum Nat.modEq_eleven_digits_sum diff --git a/Mathlib/Data/Nat/Factorial/BigOperators.lean b/Mathlib/Data/Nat/Factorial/BigOperators.lean index 64f65882c7a4f..642ba3f562abb 100644 --- a/Mathlib/Data/Nat/Factorial/BigOperators.lean +++ b/Mathlib/Data/Nat/Factorial/BigOperators.lean @@ -32,7 +32,7 @@ theorem prod_factorial_pos : 0 < ∏ i in s, (f i)! := theorem prod_factorial_dvd_factorial_sum : (∏ i in s, (f i)!) ∣ (∑ i in s, f i)! := by classical induction' s using Finset.induction with a' s' has ih - · simp only [Finset.sum_empty, Finset.prod_empty, factorial] + · simp only [prod_empty, factorial, dvd_refl] · simp only [Finset.prod_insert has, Finset.sum_insert has] refine' dvd_trans (mul_dvd_mul_left (f a')! ih) _ apply Nat.factorial_mul_factorial_dvd_factorial_add diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean index 07135e187cf6b..f2c25b4c51df4 100644 --- a/Mathlib/Data/Nat/Factorization/Basic.lean +++ b/Mathlib/Data/Nat/Factorization/Basic.lean @@ -115,11 +115,11 @@ theorem factorization_inj : Set.InjOn factorization { x : ℕ | x ≠ 0 } := fun #align nat.factorization_inj Nat.factorization_inj @[simp] -theorem factorization_zero : factorization 0 = 0 := by simp [factorization] +theorem factorization_zero : factorization 0 = 0 := by decide #align nat.factorization_zero Nat.factorization_zero @[simp] -theorem factorization_one : factorization 1 = 0 := by simp [factorization] +theorem factorization_one : factorization 1 = 0 := by decide #align nat.factorization_one Nat.factorization_one /-- The support of `n.factorization` is exactly `n.factors.toFinset` -/ diff --git a/Mathlib/Data/Nat/Hyperoperation.lean b/Mathlib/Data/Nat/Hyperoperation.lean index ad7d9bfcbf240..ad4daea7483e7 100644 --- a/Mathlib/Data/Nat/Hyperoperation.lean +++ b/Mathlib/Data/Nat/Hyperoperation.lean @@ -119,7 +119,7 @@ theorem hyperoperation_ge_four_zero (n k : ℕ) : hyperoperation (n + 4) 0 k = if Even k then 1 else 0 := by induction' k with kk kih · rw [hyperoperation_ge_three_eq_one] - simp only [even_zero, if_true] + simp only [Nat.zero_eq, even_zero, if_true] · rw [hyperoperation_recursion] rw [kih] simp_rw [Nat.even_add_one] diff --git a/Mathlib/Data/Nat/Log.lean b/Mathlib/Data/Nat/Log.lean index 66bd58ec8ce52..003252fd98157 100644 --- a/Mathlib/Data/Nat/Log.lean +++ b/Mathlib/Data/Nat/Log.lean @@ -142,7 +142,7 @@ theorem log_eq_iff {b m n : ℕ} (h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0) : · simpa only [log_of_left_le_one hb, hm.symm, false_iff_iff, not_and, not_lt] using le_trans (pow_le_pow_of_le_one' hb m.le_succ) · simpa only [log_zero_right, hm.symm, nonpos_iff_eq_zero, false_iff, not_and, not_lt, - add_pos_iff, or_true, pow_eq_zero_iff] using pow_eq_zero + add_pos_iff, zero_lt_one, or_true, pow_eq_zero_iff] using pow_eq_zero #align nat.log_eq_iff Nat.log_eq_iff theorem log_eq_of_pow_le_of_lt_pow {b m n : ℕ} (h₁ : b ^ m ≤ n) (h₂ : n < b ^ (m + 1)) : diff --git a/Mathlib/Data/Nat/ModEq.lean b/Mathlib/Data/Nat/ModEq.lean index da8a9bbea7bd7..4f0d0831b943d 100644 --- a/Mathlib/Data/Nat/ModEq.lean +++ b/Mathlib/Data/Nat/ModEq.lean @@ -526,7 +526,7 @@ theorem odd_of_mod_four_eq_three {n : ℕ} : n % 4 = 3 → n % 2 = 1 := by theorem odd_mod_four_iff {n : ℕ} : n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3 := have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → m = 1 ∨ m = 3 := by decide ⟨fun hn => - help (n % 4) (mod_lt n (by norm_num)) <| (mod_mod_of_dvd n (by norm_num : 2 ∣ 4)).trans hn, + help (n % 4) (mod_lt n (by norm_num)) <| (mod_mod_of_dvd n (by decide : 2 ∣ 4)).trans hn, fun h => Or.elim h odd_of_mod_four_eq_one odd_of_mod_four_eq_three⟩ #align nat.odd_mod_four_iff Nat.odd_mod_four_iff diff --git a/Mathlib/Data/Nat/Parity.lean b/Mathlib/Data/Nat/Parity.lean index fdfc1cf9f53c5..939f00cb1674f 100644 --- a/Mathlib/Data/Nat/Parity.lean +++ b/Mathlib/Data/Nat/Parity.lean @@ -278,9 +278,8 @@ end example (m n : ℕ) (h : Even m) : ¬Even (n + 3) ↔ Even (m ^ 2 + m + n) := by simp [*, two_ne_zero, parity_simps] -/- Porting note: the `simp` lemmas about `bit*` no longer apply, but `simp` in Lean 4 currently -simplifies decidable propositions. This may change in the future. -/ -example : ¬Even 25394535 := by simp only +/- Porting note: the `simp` lemmas about `bit*` no longer apply. -/ +example : ¬Even 25394535 := by decide end Nat diff --git a/Mathlib/Data/Nat/PartENat.lean b/Mathlib/Data/Nat/PartENat.lean index 2102afe448c68..0d3c069bdef5c 100644 --- a/Mathlib/Data/Nat/PartENat.lean +++ b/Mathlib/Data/Nat/PartENat.lean @@ -524,7 +524,7 @@ theorem add_eq_top_iff {a b : PartENat} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ := refine PartENat.casesOn a ?_ ?_ <;> refine PartENat.casesOn b ?_ ?_ <;> simp [top_add, add_top] - simp only [←Nat.cast_add, PartENat.natCast_ne_top, forall_const] + simp only [←Nat.cast_add, PartENat.natCast_ne_top, forall_const, not_false_eq_true] #align part_enat.add_eq_top_iff PartENat.add_eq_top_iff protected theorem add_right_cancel_iff {a b c : PartENat} (hc : c ≠ ⊤) : a + c = b + c ↔ a = b := by @@ -647,7 +647,7 @@ lemma ofENat_some (n : ℕ) : ofENat (Option.some n) = ↑n := rfl @[simp, norm_cast] theorem toWithTop_ofENat (n : ℕ∞) {_ : Decidable (n : PartENat).Dom} : toWithTop (↑n) = n := by induction n with - | none => simp + | none => simp; rfl | some n => simp only [toWithTop_natCast', ofENat_some] rfl diff --git a/Mathlib/Data/Nat/Sqrt.lean b/Mathlib/Data/Nat/Sqrt.lean index b59613067c3da..cbd3e6973d366 100644 --- a/Mathlib/Data/Nat/Sqrt.lean +++ b/Mathlib/Data/Nat/Sqrt.lean @@ -47,8 +47,8 @@ To turn this into a lean proof we need to manipulate, use properties of natural -/ private theorem sqrt_isSqrt (n : ℕ) : IsSqrt n (sqrt n) := by match n with - | 0 => simp [IsSqrt] - | 1 => simp [IsSqrt] + | 0 => simp [IsSqrt, sqrt] + | 1 => simp [IsSqrt, sqrt] | n + 2 => have h : ¬ (n + 2) ≤ 1 := by simp simp only [IsSqrt, sqrt, h, ite_false] diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean index 2efd9b9c22eab..c8675ce974d4b 100644 --- a/Mathlib/Data/Nat/Squarefree.lean +++ b/Mathlib/Data/Nat/Squarefree.lean @@ -254,7 +254,7 @@ instance : DecidablePred (Squarefree : ℕ → Prop) := fun _ => decidable_of_iff' _ squarefree_iff_minSqFac theorem squarefree_two : Squarefree 2 := by - rw [squarefree_iff_nodup_factors] <;> norm_num + rw [squarefree_iff_nodup_factors] <;> decide #align nat.squarefree_two Nat.squarefree_two theorem divisors_filter_squarefree_of_squarefree {n : ℕ} (hn : Squarefree n) : diff --git a/Mathlib/Data/Nat/WithBot.lean b/Mathlib/Data/Nat/WithBot.lean index f523f068f8d40..7de807e457a8a 100644 --- a/Mathlib/Data/Nat/WithBot.lean +++ b/Mathlib/Data/Nat/WithBot.lean @@ -34,7 +34,8 @@ theorem add_eq_zero_iff {n m : WithBot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0 := b theorem add_eq_one_iff {n m : WithBot ℕ} : n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0 := by rcases n, m with ⟨_ | _, _ | _⟩ - any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩; aesop + any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩; + aesop (simp_options := { decide := true }) repeat' erw [WithBot.coe_eq_coe] exact Nat.add_eq_one_iff #align nat.with_bot.add_eq_one_iff Nat.WithBot.add_eq_one_iff @@ -42,7 +43,8 @@ theorem add_eq_one_iff {n m : WithBot ℕ} : n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n theorem add_eq_two_iff {n m : WithBot ℕ} : n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0 := by rcases n, m with ⟨_ | _, _ | _⟩ - any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩; aesop + any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩; + aesop (simp_options := { decide := true }) repeat' erw [WithBot.coe_eq_coe] exact Nat.add_eq_two_iff #align nat.with_bot.add_eq_two_iff Nat.WithBot.add_eq_two_iff @@ -50,7 +52,8 @@ theorem add_eq_two_iff {n m : WithBot ℕ} : theorem add_eq_three_iff {n m : WithBot ℕ} : n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0 := by rcases n, m with ⟨_ | _, _ | _⟩ - any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩; aesop + any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩; + aesop (simp_options := { decide := true }) repeat' erw [WithBot.coe_eq_coe] exact Nat.add_eq_three_iff #align nat.with_bot.add_eq_three_iff Nat.WithBot.add_eq_three_iff diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean index a888f840872a6..8a57888b52aa2 100644 --- a/Mathlib/Data/Num/Lemmas.lean +++ b/Mathlib/Data/Num/Lemmas.lean @@ -250,7 +250,7 @@ theorem bit1_succ : ∀ n : Num, n.bit1.succ = n.succ.bit0 #align num.bit1_succ Num.bit1_succ theorem ofNat'_succ : ∀ {n}, ofNat' (n + 1) = ofNat' n + 1 := - @(Nat.binaryRec (by simp) fun b n ih => by + @(Nat.binaryRec (by simp; rfl) fun b n ih => by cases b · erw [ofNat'_bit true n, ofNat'_bit] simp only [← bit1_of_bit1, ← bit0_of_bit0, cond, _root_.bit1] diff --git a/Mathlib/Data/Option/Basic.lean b/Mathlib/Data/Option/Basic.lean index dc631e06da0ee..c9609459f7871 100644 --- a/Mathlib/Data/Option/Basic.lean +++ b/Mathlib/Data/Option/Basic.lean @@ -328,7 +328,7 @@ theorem getD_default_eq_iget [Inhabited α] (o : Option α) : @[simp] theorem guard_eq_some' {p : Prop} [Decidable p] (u) : _root_.guard p = some u ↔ p := by cases u - by_cases h : p <;> simp [_root_.guard, h] + by_cases h : p <;> simp [_root_.guard, h]; rfl #align option.guard_eq_some' Option.guard_eq_some' theorem liftOrGet_choice {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) : diff --git a/Mathlib/Data/Polynomial/Coeff.lean b/Mathlib/Data/Polynomial/Coeff.lean index 90079aff5cbf6..9ac343613bdfc 100644 --- a/Mathlib/Data/Polynomial/Coeff.lean +++ b/Mathlib/Data/Polynomial/Coeff.lean @@ -211,7 +211,7 @@ theorem support_binomial {k m : ℕ} (hkm : k ≠ m) {x y : R} (hx : x ≠ 0) (h apply subset_antisymm (support_binomial' k m x y) simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add, - add_zero, Ne.def, hx, hy] + add_zero, Ne.def, hx, hy, not_false_eq_true, and_true] #align polynomial.support_binomial Polynomial.support_binomial theorem support_trinomial {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0) @@ -221,7 +221,7 @@ theorem support_trinomial {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm.ne, if_neg hkm.ne', if_neg hmn.ne, if_neg hmn.ne', if_neg (hkm.trans hmn).ne, if_neg (hkm.trans hmn).ne', mul_zero, add_zero, - zero_add, Ne.def, hx, hy, hz] + zero_add, Ne.def, hx, hy, hz, not_false_eq_true, and_true] #align polynomial.support_trinomial Polynomial.support_trinomial theorem card_support_binomial {k m : ℕ} (h : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) : diff --git a/Mathlib/Data/Polynomial/Div.lean b/Mathlib/Data/Polynomial/Div.lean index a72a8076d7d33..0c7df6380fe60 100644 --- a/Mathlib/Data/Polynomial/Div.lean +++ b/Mathlib/Data/Polynomial/Div.lean @@ -74,7 +74,7 @@ theorem multiplicity_finite_of_degree_pos_of_monic (hp : (0 : WithBot ℕ) < deg have hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0 := hpn1.symm ▸ zn0.symm have hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0 := by simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_pow, one_mul, Ne.def, - hr0] + hr0, not_false_eq_true] have hnp : 0 < natDegree p := Nat.cast_lt.1 <| by rw [← degree_eq_natDegree hp0]; exact hp have := congr_arg natDegree hr diff --git a/Mathlib/Data/Polynomial/FieldDivision.lean b/Mathlib/Data/Polynomial/FieldDivision.lean index f0a7fc6b6eda8..5aff519ea1db8 100644 --- a/Mathlib/Data/Polynomial/FieldDivision.lean +++ b/Mathlib/Data/Polynomial/FieldDivision.lean @@ -176,7 +176,7 @@ theorem isUnit_iff_degree_eq_zero : IsUnit p ↔ degree p = 0 := ⟨degree_eq_zero_of_isUnit, fun h => have : degree p ≤ 0 := by simp [*, le_refl] have hc : coeff p 0 ≠ 0 := fun hc => by - rw [eq_C_of_degree_le_zero this, hc] at h; simp at h + rw [eq_C_of_degree_le_zero this, hc] at h; simp only [map_zero] at h; contradiction isUnit_iff_dvd_one.2 ⟨C (coeff p 0)⁻¹, by conv in p => rw [eq_C_of_degree_le_zero this] @@ -403,7 +403,7 @@ theorem exists_root_of_degree_eq_one (h : degree p = 1) : ∃ x, IsRoot p x := have : p.coeff 1 ≠ 0 := by have h' := natDegree_eq_of_degree_eq_some h change natDegree p = 1 at h'; rw [←h'] - exact mt leadingCoeff_eq_zero.1 fun h0 => by simp [h0] at h + exact mt leadingCoeff_eq_zero.1 fun h0 => by simp [h0] at h; contradiction conv in p => rw [eq_X_add_C_of_degree_le_one (show degree p ≤ 1 by rw [h])] simp [IsRoot, mul_div_cancel' _ this]⟩ #align polynomial.exists_root_of_degree_eq_one Polynomial.exists_root_of_degree_eq_one @@ -486,7 +486,7 @@ theorem prime_of_degree_eq_one (hp1 : degree p = 1) : Prime p := by classical have : Prime (normalize p) := Monic.prime_of_degree_eq_one (hp1 ▸ degree_normalize) - (monic_normalize fun hp0 => absurd hp1 (hp0.symm ▸ by simp)) + (monic_normalize fun hp0 => absurd hp1 (hp0.symm ▸ by simp only [degree_zero]; decide)) exact (normalize_associated _).prime this #align polynomial.prime_of_degree_eq_one Polynomial.prime_of_degree_eq_one diff --git a/Mathlib/Data/Polynomial/RingDivision.lean b/Mathlib/Data/Polynomial/RingDivision.lean index 3511a78bc1d7d..1af8098cc72be 100644 --- a/Mathlib/Data/Polynomial/RingDivision.lean +++ b/Mathlib/Data/Polynomial/RingDivision.lean @@ -1300,7 +1300,7 @@ theorem count_map_roots_of_injective [IsDomain A] [DecidableEq B] (p : A[X]) {f (p.roots.map f).count b ≤ rootMultiplicity b (p.map f) := by by_cases hp0 : p = 0 · simp only [hp0, roots_zero, Multiset.map_zero, Multiset.count_zero, Polynomial.map_zero, - rootMultiplicity_zero] + rootMultiplicity_zero, le_refl] · exact count_map_roots ((Polynomial.map_ne_zero_iff hf).mpr hp0) b #align polynomial.count_map_roots_of_injective Polynomial.count_map_roots_of_injective diff --git a/Mathlib/Data/Polynomial/UnitTrinomial.lean b/Mathlib/Data/Polynomial/UnitTrinomial.lean index f5a3dba04d03c..e91b47e0ff1dd 100644 --- a/Mathlib/Data/Polynomial/UnitTrinomial.lean +++ b/Mathlib/Data/Polynomial/UnitTrinomial.lean @@ -203,6 +203,7 @@ theorem isUnitTrinomial_iff' : sum_insert (mt mem_singleton.mp hmn.ne), sum_singleton, trinomial_leading_coeff' hkm hmn, trinomial_middle_coeff hkm hmn, trinomial_trailing_coeff' hkm hmn] simp_rw [← Units.val_pow_eq_pow_val, Int.units_sq] + decide · have key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1 := fun k hk => Int.sq_eq_one_of_sq_le_three ((single_le_sum (fun k _ => sq_nonneg (p.coeff k)) hk).trans hp.le) (mem_support_iff.mp hk) diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean index 785026a02536e..10e5c3c238590 100644 --- a/Mathlib/Data/Rat/Defs.lean +++ b/Mathlib/Data/Rat/Defs.lean @@ -240,14 +240,16 @@ theorem divInt_zero_one : 0 /. 1 = 0 := theorem divInt_one_one : 1 /. 1 = 1 := show divInt _ _ = _ by rw [divInt] - simp + simp [mkRat, normalize] + rfl #align rat.mk_one_one Rat.divInt_one_one @[simp] theorem divInt_neg_one_one : -1 /. 1 = -1 := show divInt _ _ = _ by rw [divInt] - simp + simp [mkRat, normalize] + rfl #align rat.mk_neg_one_one Rat.divInt_neg_one_one theorem divInt_one (n : ℤ) : n /. 1 = n := diff --git a/Mathlib/Data/Rat/Lemmas.lean b/Mathlib/Data/Rat/Lemmas.lean index 01ab28303b775..1a09e6d8b1a18 100644 --- a/Mathlib/Data/Rat/Lemmas.lean +++ b/Mathlib/Data/Rat/Lemmas.lean @@ -233,6 +233,7 @@ theorem coe_int_div_self (n : ℤ) : ((n / n : ℤ) : ℚ) = n / n := by by_cases hn : n = 0 · subst hn simp only [Int.cast_zero, Int.zero_div, zero_div] + rfl · have : (n : ℚ) ≠ 0 := by rwa [← coe_int_inj] at hn simp only [Int.ediv_self hn, Int.cast_one, Ne.def, not_false_iff, div_self this] #align rat.coe_int_div_self Rat.coe_int_div_self diff --git a/Mathlib/Data/Real/ENNReal.lean b/Mathlib/Data/Real/ENNReal.lean index 80f250f87af2f..185db4b78ccbc 100644 --- a/Mathlib/Data/Real/ENNReal.lean +++ b/Mathlib/Data/Real/ENNReal.lean @@ -343,6 +343,8 @@ theorem toReal_ofReal_eq_iff {a : ℝ} : (ENNReal.ofReal a).toReal = a ↔ 0 ≤ @[simp] theorem top_ne_one : ∞ ≠ 1 := top_ne_coe #align ennreal.top_ne_one ENNReal.top_ne_one +@[simp] theorem zero_lt_top : 0 < ∞ := coe_lt_top + @[simp, norm_cast] theorem coe_eq_coe : (↑r : ℝ≥0∞) = ↑q ↔ r = q := WithTop.coe_eq_coe #align ennreal.coe_eq_coe ENNReal.coe_eq_coe @@ -428,9 +430,11 @@ nonrec theorem one_lt_two : (1 : ℝ≥0∞) < 2 := coe_one ▸ coe_two ▸ by exact_mod_cast (one_lt_two : 1 < 2) #align ennreal.one_lt_two ENNReal.one_lt_two -theorem two_ne_top : (2 : ℝ≥0∞) ≠ ∞ := coe_ne_top +@[simp] theorem two_ne_top : (2 : ℝ≥0∞) ≠ ∞ := coe_ne_top #align ennreal.two_ne_top ENNReal.two_ne_top +@[simp] theorem two_lt_top : (2 : ℝ≥0∞) < ∞ := coe_lt_top + /-- `(1 : ℝ≥0∞) ≤ 1`, recorded as a `Fact` for use with `Lp` spaces. -/ instance _root_.fact_one_le_one_ennreal : Fact ((1 : ℝ≥0∞) ≤ 1) := ⟨le_rfl⟩ @@ -635,7 +639,7 @@ theorem mul_lt_top_iff {a b : ℝ≥0∞} : a * b < ∞ ↔ a < ∞ ∧ b < ∞ theorem mul_self_lt_top_iff {a : ℝ≥0∞} : a * a < ⊤ ↔ a < ⊤ := by rw [ENNReal.mul_lt_top_iff, and_self, or_self, or_iff_left_iff_imp] rintro rfl - norm_num + decide #align ennreal.mul_self_lt_top_iff ENNReal.mul_self_lt_top_iff theorem mul_pos_iff : 0 < a * b ↔ 0 < a ∧ 0 < b := @@ -651,7 +655,7 @@ theorem mul_pos (ha : a ≠ 0) (hb : b ≠ 0) : 0 < a * b := rcases n.eq_zero_or_pos with rfl | (hn : 0 < n) · simp · induction a using recTopCoe - · simp only [Ne.def, hn.ne', top_pow hn] + · simp only [Ne.def, hn.ne', top_pow hn, not_false_eq_true, and_self] · simp only [← coe_pow, coe_ne_top, false_and] #align ennreal.pow_eq_top_iff ENNReal.pow_eq_top_iff @@ -1793,7 +1797,8 @@ theorem add_thirds (a : ℝ≥0∞) : a / 3 + a / 3 + a / 3 = a := by @[simp] theorem div_pos_iff : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞ := by simp [pos_iff_ne_zero, not_or] #align ennreal.div_pos_iff ENNReal.div_pos_iff -protected theorem half_pos (h : a ≠ 0) : 0 < a / 2 := by simp [h] +protected theorem half_pos (h : a ≠ 0) : 0 < a / 2 := by + simp only [div_pos_iff, ne_eq, h, not_false_eq_true]; decide #align ennreal.half_pos ENNReal.half_pos protected theorem one_half_lt_one : (2⁻¹ : ℝ≥0∞) < 1 := @@ -1914,7 +1919,8 @@ theorem coe_zpow (hr : r ≠ 0) (n : ℤ) : (↑(r ^ n) : ℝ≥0∞) = (r : ℝ theorem zpow_pos (ha : a ≠ 0) (h'a : a ≠ ∞) (n : ℤ) : 0 < a ^ n := by cases n · exact ENNReal.pow_pos ha.bot_lt _ - · simp only [h'a, pow_eq_top_iff, zpow_negSucc, Ne.def, not_false, ENNReal.inv_pos, false_and] + · simp only [h'a, pow_eq_top_iff, zpow_negSucc, Ne.def, not_false, ENNReal.inv_pos, false_and, + not_false_eq_true] #align ennreal.zpow_pos ENNReal.zpow_pos theorem zpow_lt_top (ha : a ≠ 0) (h'a : a ≠ ∞) (n : ℤ) : a ^ n < ∞ := by diff --git a/Mathlib/Data/Real/Pi/Wallis.lean b/Mathlib/Data/Real/Pi/Wallis.lean index 72c1ced1777b3..89b3317cb4aa1 100644 --- a/Mathlib/Data/Real/Pi/Wallis.lean +++ b/Mathlib/Data/Real/Pi/Wallis.lean @@ -95,8 +95,8 @@ theorem le_W (k : ℕ) : ((2 : ℝ) * k + 1) / (2 * k + 2) * (π / 2) ≤ W k := rw [W_eq_integral_sin_pow_div_integral_sin_pow, le_div_iff (integral_sin_pow_pos _)] convert integral_sin_pow_succ_le (2 * k + 1) rw [integral_sin_pow (2 * k)] - simp only [sin_zero, zero_pow', Ne.def, Nat.succ_ne_zero, zero_mul, sin_pi, tsub_zero, zero_div, - zero_add] + simp only [sin_zero, ne_eq, add_eq_zero, and_false, not_false_eq_true, zero_pow', cos_zero, + mul_one, sin_pi, cos_pi, mul_neg, neg_zero, sub_self, zero_div, zero_add] norm_cast #align real.wallis.le_W Real.Wallis.le_W diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index 96b5e91c55dbc..54be95b67b4ee 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -555,7 +555,7 @@ theorem nonempty_of_ncard_ne_zero (hs : s.ncard ≠ 0) : s.Nonempty := by #align set.nonempty_of_ncard_ne_zero Set.nonempty_of_ncard_ne_zero @[simp] theorem ncard_singleton (a : α) : ({a} : Set α).ncard = 1 := by - simp [ncard_eq_toFinset_card] + simp [ncard, ncard_eq_toFinset_card] #align set.ncard_singleton Set.ncard_singleton theorem ncard_singleton_inter (a : α) (s : Set α) : ({a} ∩ s).ncard ≤ 1 := by diff --git a/Mathlib/Data/Sign.lean b/Mathlib/Data/Sign.lean index d51cd58790179..ae98a5158f3eb 100644 --- a/Mathlib/Data/Sign.lean +++ b/Mathlib/Data/Sign.lean @@ -34,7 +34,7 @@ namespace SignType -- Porting note: Added Fintype SignType manually instance : Fintype SignType := - Fintype.ofMultiset (zero :: neg :: pos :: List.nil) (fun x ↦ by cases x <;> simp only) + Fintype.ofMultiset (zero :: neg :: pos :: List.nil) (fun x ↦ by cases x <;> decide) instance : Zero SignType := ⟨zero⟩ @@ -155,7 +155,7 @@ def fin3Equiv : SignType ≃* Fin 3 where | ⟨2, _⟩ => by simp | ⟨n + 3, h⟩ => by simp at h map_mul' a b := by - cases a <;> cases b <;> simp + cases a <;> cases b <;> rfl #align sign_type.fin3_equiv SignType.fin3Equiv section CaseBashing diff --git a/Mathlib/Data/String/Basic.lean b/Mathlib/Data/String/Basic.lean index 633bb00b8c2a9..e1e2b6da63107 100644 --- a/Mathlib/Data/String/Basic.lean +++ b/Mathlib/Data/String/Basic.lean @@ -75,13 +75,13 @@ theorem ltb_cons_addChar (c : Char) (cs₁ cs₂ : List Char) (i₁ i₂ : Pos) theorem lt_iff_toList_lt : ∀ {s₁ s₂ : String}, s₁ < s₂ ↔ s₁.toList < s₂.toList | ⟨s₁⟩, ⟨s₂⟩ => show ltb ⟨⟨s₁⟩, 0⟩ ⟨⟨s₂⟩, 0⟩ ↔ s₁ < s₂ by induction s₁ generalizing s₂ <;> cases s₂ - · simp + · decide · rename_i c₂ cs₂; apply iff_of_true - · rw [ltb]; simp; apply ne_false_of_eq_true; apply decide_eq_true + · rw [ltb]; simp only [Iterator.hasNext, Iterator.curr] simp [endPos, utf8ByteSize, utf8ByteSize.go, csize_pos] · apply List.nil_lt_cons · rename_i c₁ cs₁ ih; apply iff_of_false - · rw [ltb]; simp + · rw [ltb]; simp [Iterator.hasNext, Iterator.curr] · apply not_lt_of_lt; apply List.nil_lt_cons · rename_i c₁ cs₁ ih c₂ cs₂; rw [ltb] simp [Iterator.hasNext, endPos, utf8ByteSize, utf8ByteSize.go, csize_pos, Iterator.curr, get, @@ -134,7 +134,7 @@ theorem asString_inv_toList (s : String) : s.toList.asString = s := theorem toList_nonempty : ∀ {s : String}, s ≠ "" → s.toList = s.head :: (s.drop 1).toList | ⟨s⟩, h => by cases s - · simp only at h + · simp only [ne_eq, not_true_eq_false] at h · rename_i c cs simp only [toList, List.cons.injEq] constructor <;> [rfl; simp [drop_eq]] diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean index a5b29bbd9a39c..c56e5ec81a1cc 100644 --- a/Mathlib/Data/ZMod/Basic.lean +++ b/Mathlib/Data/ZMod/Basic.lean @@ -853,7 +853,7 @@ theorem neg_one_ne_one {n : ℕ} [Fact (2 < n)] : (-1 : ZMod n) ≠ 1 := #align zmod.neg_one_ne_one ZMod.neg_one_ne_one theorem neg_eq_self_mod_two (a : ZMod 2) : -a = a := by - fin_cases a <;> apply Fin.ext <;> simp [Fin.coe_neg, Int.natMod] + fin_cases a <;> apply Fin.ext <;> simp [Fin.coe_neg, Int.natMod]; rfl #align zmod.neg_eq_self_mod_two ZMod.neg_eq_self_mod_two @[simp] diff --git a/Mathlib/Geometry/Euclidean/MongePoint.lean b/Mathlib/Geometry/Euclidean/MongePoint.lean index 9432a3a393167..ed39ed20f5d5f 100644 --- a/Mathlib/Geometry/Euclidean/MongePoint.lean +++ b/Mathlib/Geometry/Euclidean/MongePoint.lean @@ -474,16 +474,18 @@ theorem altitude_eq_mongePlane (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h (h₂₃ : i₂ ≠ i₃) : t.altitude i₁ = t.mongePlane i₂ i₃ := by have hs : ({i₂, i₃}ᶜ : Finset (Fin 3)) = {i₁} := by -- porting note: was `decide!` - fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ <;> simp at h₁₂ h₁₃ h₂₃ ⊢ + fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ + <;> simp (config := {decide := true}) at h₁₂ h₁₃ h₂₃ ⊢ have he : univ.erase i₁ = {i₂, i₃} := by -- porting note: was `decide!` - fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ <;> simp at h₁₂ h₁₃ h₂₃ ⊢ + fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ + <;> simp (config := {decide := true}) at h₁₂ h₁₃ h₂₃ ⊢ rw [mongePlane_def, altitude_def, direction_affineSpan, hs, he, centroid_singleton, coe_insert, coe_singleton, vectorSpan_image_eq_span_vsub_set_left_ne ℝ _ (Set.mem_insert i₂ _)] simp [h₂₃, Submodule.span_insert_eq_span] -- porting note: this didn't need the `congr` and the `fin_cases` congr - fin_cases i₂ <;> fin_cases i₃ <;> simp at h₂₃ ⊢ + fin_cases i₂ <;> fin_cases i₃ <;> simp (config := {decide := true}) at h₂₃ ⊢ #align affine.triangle.altitude_eq_monge_plane Affine.Triangle.altitude_eq_mongePlane /-- The orthocenter lies in the altitudes. -/ @@ -589,7 +591,8 @@ theorem altitude_replace_orthocenter_eq_affineSpan {t₁ t₂ : Triangle ℝ P} · have hu : (Finset.univ : Finset (Fin 3)) = {j₁, j₂, j₃} := by clear h₁ h₂ h₃ -- porting note: was `decide!` - fin_cases j₁ <;> fin_cases j₂ <;> fin_cases j₃ <;> simp at hj₁₂ hj₁₃ hj₂₃ ⊢ + fin_cases j₁ <;> fin_cases j₂ <;> fin_cases j₃ + <;> simp (config := {decide := true}) at hj₁₂ hj₁₃ hj₂₃ ⊢ rw [← Set.image_univ, ← Finset.coe_univ, hu, Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_insert_eq, Set.image_singleton, h₁, h₂, h₃, Set.insert_subset_iff, Set.insert_subset_iff, Set.singleton_subset_iff] @@ -604,7 +607,8 @@ theorem altitude_replace_orthocenter_eq_affineSpan {t₁ t₂ : Triangle ℝ P} have hu : Finset.univ.erase j₂ = {j₁, j₃} := by clear h₁ h₂ h₃ -- porting note: was `decide!` - fin_cases j₁ <;> fin_cases j₂ <;> fin_cases j₃ <;> simp at hj₁₂ hj₁₃ hj₂₃ ⊢ + fin_cases j₁ <;> fin_cases j₂ <;> fin_cases j₃ + <;> simp (config := {decide := true}) at hj₁₂ hj₁₃ hj₂₃ ⊢ rw [hu, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_singleton, h₁, h₃] have hle : (t₁.altitude i₃).directionᗮ ≤ line[ℝ, t₁.orthocenter, t₁.points i₃].directionᗮ := Submodule.orthogonal_le (direction_le (affineSpan_orthocenter_point_le_altitude _ _)) @@ -612,7 +616,8 @@ theorem altitude_replace_orthocenter_eq_affineSpan {t₁ t₂ : Triangle ℝ P} have hui : Finset.univ.erase i₃ = {i₁, i₂} := by clear hle h₂ h₃ -- porting note: was `decide!` - fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ <;> simp at hi₁₂ hi₁₃ hi₂₃ ⊢ + fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ + <;> simp (config := {decide := true}) at hi₁₂ hi₁₃ hi₂₃ ⊢ rw [hui, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_singleton] refine' vsub_mem_vectorSpan ℝ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _)) #align affine.triangle.altitude_replace_orthocenter_eq_affine_span Affine.Triangle.altitude_replace_orthocenter_eq_affineSpan @@ -783,7 +788,7 @@ theorem OrthocentricSystem.eq_insert_orthocenter {s : Set P} (ho : OrthocentricS ∃ j₁ : Fin 3, j₁ ≠ j₂ ∧ j₁ ≠ j₃ ∧ ∀ j : Fin 3, j = j₁ ∨ j = j₂ ∨ j = j₃ := by clear h₂ h₃ -- porting note: was `decide!` - fin_cases j₂ <;> fin_cases j₃ <;> simp at hj₂₃ ⊢ + fin_cases j₂ <;> fin_cases j₃ <;> simp (config := {decide := true}) at hj₂₃ ⊢ suffices h : t₀.points j₁ = t.orthocenter · have hui : (Set.univ : Set (Fin 3)) = {i₁, i₂, i₃} := by ext x; simpa using h₁₂₃ x have huj : (Set.univ : Set (Fin 3)) = {j₁, j₂, j₃} := by ext x; simpa using hj₁₂₃ x diff --git a/Mathlib/GroupTheory/CommutingProbability.lean b/Mathlib/GroupTheory/CommutingProbability.lean index 26b9363e0ad6d..11b4a6ef32cc0 100644 --- a/Mathlib/GroupTheory/CommutingProbability.lean +++ b/Mathlib/GroupTheory/CommutingProbability.lean @@ -209,13 +209,13 @@ theorem commProb_reciprocal (n : ℕ) : rcases Nat.even_or_odd n with h2 | h2 · have := div_two_lt h0 rw [reciprocalFactors_even h0 h2, commProb_cons, commProb_reciprocal (n / 2), - commProb_odd (by norm_num)] + commProb_odd (by decide)] field_simp [h0, h2.two_dvd] norm_num · have := div_four_lt h0 h1 rw [reciprocalFactors_odd h1 h2, commProb_cons, commProb_reciprocal (n / 4 + 1)] have key : n % 4 = 1 ∨ n % 4 = 3 := Nat.odd_mod_four_iff.mp (Nat.odd_iff.mp h2) - have hn : Odd (n % 4) := by rcases key with h | h <;> rw [h] <;> norm_num + have hn : Odd (n % 4) := by rcases key with h | h <;> rw [h] <;> decide rw [commProb_odd (hn.mul h2), div_mul_div_comm, mul_one, div_eq_div_iff, one_mul] <;> norm_cast · have h0 : (n % 4) ^ 2 + 3 = n % 4 * 4 := by rcases key with h | h <;> rw [h] <;> norm_num have h1 := (Nat.div_add_mod n 4).symm diff --git a/Mathlib/GroupTheory/FiniteAbelian.lean b/Mathlib/GroupTheory/FiniteAbelian.lean index 9ab087f7b8a49..64243cd968c62 100644 --- a/Mathlib/GroupTheory/FiniteAbelian.lean +++ b/Mathlib/GroupTheory/FiniteAbelian.lean @@ -75,7 +75,7 @@ theorem equiv_directSum_zmod_of_fintype [Finite G] : obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ := equiv_free_prod_directSum_zmod G cases' n with n · have : Unique (Fin Nat.zero →₀ ℤ) := - { uniq := by simp only [Nat.zero_eq, eq_iff_true_of_subsingleton] } + { uniq := by simp only [Nat.zero_eq, eq_iff_true_of_subsingleton]; trivial } exact ⟨ι, fι, p, hp, e, ⟨f.trans AddEquiv.uniqueProd⟩⟩ · haveI := @Fintype.prodLeft _ _ _ (Fintype.ofEquiv G f.toEquiv) _ exact diff --git a/Mathlib/GroupTheory/HNNExtension.lean b/Mathlib/GroupTheory/HNNExtension.lean index 58ac00238b7eb..0350fceacee4d 100644 --- a/Mathlib/GroupTheory/HNNExtension.lean +++ b/Mathlib/GroupTheory/HNNExtension.lean @@ -400,7 +400,7 @@ theorem not_cancels_of_cons_hyp (u : ℤˣ) (w : NormalWord d) theorem unitsSMul_cancels_iff (u : ℤˣ) (w : NormalWord d) : Cancels (-u) (unitsSMul φ u w) ↔ ¬ Cancels u w := by by_cases h : Cancels u w - · simp only [unitsSMul, dif_pos trivial, h, iff_false] + · simp only [unitsSMul, h, dite_true, not_true_eq_false, iff_false] induction w using consRecOn with | ofGroup => simp [Cancels, unitsSMulWithCancel] | cons g u' w h1 h2 _ => diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean index dd32762a884d4..a8682807bab05 100644 --- a/Mathlib/GroupTheory/OrderOfElement.lean +++ b/Mathlib/GroupTheory/OrderOfElement.lean @@ -1129,7 +1129,7 @@ theorem LinearOrderedRing.orderOf_le_two : orderOf x ≤ 2 := by cases' ne_or_eq |x| 1 with h h · simp [orderOf_abs_ne_one h] rcases eq_or_eq_neg_of_abs_eq h with (rfl | rfl) - · simp + · simp; decide apply orderOf_le_of_pow_eq_one <;> norm_num #align linear_ordered_ring.order_of_le_two LinearOrderedRing.orderOf_le_two diff --git a/Mathlib/GroupTheory/Perm/Fin.lean b/Mathlib/GroupTheory/Perm/Fin.lean index 7a73e7bfe41be..4a47675d6ae71 100644 --- a/Mathlib/GroupTheory/Perm/Fin.lean +++ b/Mathlib/GroupTheory/Perm/Fin.lean @@ -103,7 +103,7 @@ theorem finRotate_succ_eq_decomposeFin {n : ℕ} : @[simp] theorem sign_finRotate (n : ℕ) : Perm.sign (finRotate (n + 1)) = (-1) ^ n := by induction' n with n ih - · simp + · simp; rfl · rw [finRotate_succ_eq_decomposeFin] simp [ih, pow_succ] #align sign_fin_rotate sign_finRotate diff --git a/Mathlib/GroupTheory/SpecificGroups/Alternating.lean b/Mathlib/GroupTheory/SpecificGroups/Alternating.lean index 3dcf4048c87ee..6fd738905a9b1 100644 --- a/Mathlib/GroupTheory/SpecificGroups/Alternating.lean +++ b/Mathlib/GroupTheory/SpecificGroups/Alternating.lean @@ -262,6 +262,7 @@ theorem normalClosure_swap_mul_swap_five : ⟨finRotate 5, finRotate_bit1_mem_alternatingGroup (n := 2)⟩ := by rw [Subtype.ext_iff] simp only [Fin.val_mk, Subgroup.coe_mul, Subgroup.coe_inv, Fin.val_mk] + decide rw [eq_top_iff, ← normalClosure_finRotate_five] refine' normalClosure_le_normal _ rw [Set.singleton_subset_iff, SetLike.mem_coe, ← h5] @@ -280,7 +281,7 @@ theorem isConj_swap_mul_swap_of_cycleType_two {g : Perm (Fin 5)} (ha : g ∈ alt rw [← Multiset.eq_replicate_card] at h2 rw [← sum_cycleType, h2, Multiset.sum_replicate, smul_eq_mul] at h have h : Multiset.card g.cycleType ≤ 3 := - le_of_mul_le_mul_right (le_trans h (by simp only [card_fin]; ring_nf)) (by simp) + le_of_mul_le_mul_right (le_trans h (by simp only [card_fin]; ring_nf; decide)) (by simp) rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha norm_num at ha rw [pow_add, pow_mul, Int.units_pow_two, one_mul, Units.ext_iff, Units.val_one, @@ -299,7 +300,7 @@ theorem isConj_swap_mul_swap_of_cycleType_two {g : Perm (Fin 5)} (ha : g ∈ alt · rw [disjoint_iff_disjoint_support, support_swap h04, support_swap h13] decide · contrapose! ha - simp [h_1] + decide #align alternating_group.is_conj_swap_mul_swap_of_cycle_type_two alternatingGroup.isConj_swap_mul_swap_of_cycleType_two /-- Shows that $A_5$ is simple by taking an arbitrary non-identity element and showing by casework diff --git a/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean b/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean index 962092e3c2155..df50ccc519fcc 100644 --- a/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean +++ b/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean @@ -118,7 +118,7 @@ instance : Infinite (DihedralGroup 0) := DihedralGroup.fintypeHelper.infinite_iff.mp inferInstance instance : Nontrivial (DihedralGroup n) := - ⟨⟨r 0, sr 0, by simp_rw [ne_eq]⟩⟩ + ⟨⟨r 0, sr 0, by simp_rw [ne_eq, not_false_eq_true]⟩⟩ /-- If `0 < n`, then `DihedralGroup n` has `2n` elements. -/ @@ -161,7 +161,7 @@ theorem orderOf_sr (i : ZMod n) : orderOf (sr i) = 2 := by · rw [sq, sr_mul_self] · -- Porting note: Previous proof was `decide` revert n - simp_rw [one_def, ne_eq, forall_const] + simp_rw [one_def, ne_eq, forall_const, not_false_eq_true] #align dihedral_group.order_of_sr DihedralGroup.orderOf_sr /-- If `0 < n`, then `r 1` has order `n`. diff --git a/Mathlib/Init/Data/Nat/Lemmas.lean b/Mathlib/Init/Data/Nat/Lemmas.lean index e12c293e90f5b..40d911f717770 100644 --- a/Mathlib/Init/Data/Nat/Lemmas.lean +++ b/Mathlib/Init/Data/Nat/Lemmas.lean @@ -788,7 +788,7 @@ lemma to_digits_core_length (b : Nat) (h : 2 <= b) (f n e : Nat) rw [‹e = 0›] have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul] have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0) - simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length] + simp [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0)] /-- The core implementation of `Nat.repr` returns a String with length less than or equal to the number of digits in the decimal number (represented by `e`). For example, the decimal string diff --git a/Mathlib/Init/Order/Defs.lean b/Mathlib/Init/Order/Defs.lean index 71354059a3a5b..b823526c32e79 100644 --- a/Mathlib/Init/Order/Defs.lean +++ b/Mathlib/Init/Order/Defs.lean @@ -262,7 +262,7 @@ implicit arguments, requires us to unfold the defs and split the `if`s in the de macro "compareOfLessAndEq_rfl" : tactic => `(tactic| (intros a b; first | rfl | (simp only [compare, compareOfLessAndEq]; split_ifs <;> rfl) | - (induction a <;> induction b <;> simp only []))) + (induction a <;> induction b <;> simp (config := {decide := true}) only []))) /-- A linear order is reflexive, transitive, antisymmetric and total relation `≤`. We assume that every linear ordered type has decidable `(≤)`, `(<)`, and `(=)`. -/ @@ -436,16 +436,16 @@ theorem compare_eq_iff_eq {a b : α} : (compare a b = .eq) ↔ a = b := by case _ _ h => exact false_iff_iff.2 h theorem compare_le_iff_le {a b : α} : (compare a b ≠ .gt) ↔ a ≤ b := by - cases h : compare a b <;> simp only [] - · exact true_iff_iff.2 <| le_of_lt <| compare_lt_iff_lt.1 h - · exact true_iff_iff.2 <| le_of_eq <| compare_eq_iff_eq.1 h - · exact false_iff_iff.2 <| not_le_of_gt <| compare_gt_iff_gt.1 h + cases h : compare a b <;> simp + · exact le_of_lt <| compare_lt_iff_lt.1 h + · exact le_of_eq <| compare_eq_iff_eq.1 h + · exact compare_gt_iff_gt.1 h theorem compare_ge_iff_ge {a b : α} : (compare a b ≠ .lt) ↔ a ≥ b := by - cases h : compare a b <;> simp only [] - · exact false_iff_iff.2 <| (lt_iff_not_ge a b).1 <| compare_lt_iff_lt.1 h - · exact true_iff_iff.2 <| le_of_eq <| (·.symm) <| compare_eq_iff_eq.1 h - · exact true_iff_iff.2 <| le_of_lt <| compare_gt_iff_gt.1 h + cases h : compare a b <;> simp + · exact compare_lt_iff_lt.1 h + · exact le_of_eq <| (·.symm) <| compare_eq_iff_eq.1 h + · exact le_of_lt <| compare_gt_iff_gt.1 h theorem compare_iff (a b : α) {o : Ordering} : compare a b = o ↔ o.toRel a b := by cases o <;> simp only [Ordering.toRel] diff --git a/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean b/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean index 14819d2553db9..381e4f20e2fe0 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean @@ -479,7 +479,8 @@ theorem affineIndependent_iff_not_collinear_of_ne {p : Fin 3 → P} {i₁ i₂ i AffineIndependent k p ↔ ¬Collinear k ({p i₁, p i₂, p i₃} : Set P) := by have hu : (Finset.univ : Finset (Fin 3)) = {i₁, i₂, i₃} := by -- Porting note: Originally `by decide!` - fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ <;> simp only at h₁₂ h₁₃ h₂₃ ⊢ + fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ + <;> simp (config := {decide := true}) only at h₁₂ h₁₃ h₂₃ ⊢ rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu, Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair] #align affine_independent_iff_not_collinear_of_ne affineIndependent_iff_not_collinear_of_ne diff --git a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean index 3b32e603f4928..f162ad0dbda54 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean @@ -688,7 +688,7 @@ theorem affineIndependent_of_ne_of_mem_of_mem_of_not_mem {s : AffineSubspace k P refine' hp₃ ((AffineSubspace.le_def' _ s).1 _ p₃ h) simp_rw [affineSpan_le, Set.image_subset_iff, Set.subset_def, Set.mem_preimage] intro x - fin_cases x <;> simp [hp₁, hp₂] + fin_cases x <;> simp (config := {decide := true}) [hp₁, hp₂] #align affine_independent_of_ne_of_mem_of_mem_of_not_mem affineIndependent_of_ne_of_mem_of_mem_of_not_mem /-- If distinct points `p₁` and `p₃` lie in `s` but `p₂` does not, the three points are affinely diff --git a/Mathlib/LinearAlgebra/Determinant.lean b/Mathlib/LinearAlgebra/Determinant.lean index 18dd3b59db798..b8890e6f4f830 100644 --- a/Mathlib/LinearAlgebra/Determinant.lean +++ b/Mathlib/LinearAlgebra/Determinant.lean @@ -322,7 +322,7 @@ theorem det_conj {N : Type*} [AddCommGroup N] [Module A N] (f : M →ₗ[A] M) ( contrapose! H rcases H with ⟨s, ⟨b⟩⟩ exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩ - simp only [coe_det, H, H', MonoidHom.one_apply, dif_neg] + simp only [coe_det, H, H', MonoidHom.one_apply, dif_neg, not_false_eq_true] #align linear_map.det_conj LinearMap.det_conj /-- If a linear map is invertible, so is its determinant. -/ diff --git a/Mathlib/LinearAlgebra/Finrank.lean b/Mathlib/LinearAlgebra/Finrank.lean index 44b147bbc6c35..b1187d4359813 100644 --- a/Mathlib/LinearAlgebra/Finrank.lean +++ b/Mathlib/LinearAlgebra/Finrank.lean @@ -435,7 +435,7 @@ theorem linearIndependent_of_top_le_span_of_card_eq_finrank {ι : Type*} [Fintyp · refine' neg_mem (smul_mem _ _ (sum_mem fun k hk => _)) obtain ⟨k_ne_i, _⟩ := Finset.mem_erase.mp hk refine' smul_mem _ _ (subset_span ⟨k, _, rfl⟩) - simp_all only [Set.mem_univ, Set.mem_diff, Set.mem_singleton_iff] + simp_all only [Set.mem_univ, Set.mem_diff, Set.mem_singleton_iff, and_self, not_false_eq_true] -- To show `b i` is a weighted sum of the other `b j`s, we'll rewrite this sum -- to have the form of the assumption `dependent`. apply eq_neg_of_add_eq_zero_left diff --git a/Mathlib/LinearAlgebra/LinearPMap.lean b/Mathlib/LinearAlgebra/LinearPMap.lean index bb182f960c90a..917ea90d6ca8e 100644 --- a/Mathlib/LinearAlgebra/LinearPMap.lean +++ b/Mathlib/LinearAlgebra/LinearPMap.lean @@ -792,7 +792,7 @@ theorem graph_map_fst_eq_domain (f : E →ₗ.[R] F) : · rcases h with ⟨x, hx, _⟩ exact hx · use f ⟨x, h⟩ - simp only [h, exists_prop] + simp only [h, exists_const] theorem graph_map_snd_eq_range (f : E →ₗ.[R] F) : f.graph.map (LinearMap.snd R E F) = LinearMap.range f.toFun := by ext; simp diff --git a/Mathlib/LinearAlgebra/Matrix/Transvection.lean b/Mathlib/LinearAlgebra/Matrix/Transvection.lean index 48ba5b08e9e15..21d209adf9735 100644 --- a/Mathlib/LinearAlgebra/Matrix/Transvection.lean +++ b/Mathlib/LinearAlgebra/Matrix/Transvection.lean @@ -484,7 +484,8 @@ theorem mul_listTransvecRow_last_row (hM : M (inr unit) (inr unit) ≠ 0) (i : F rintro rfl cases i tauto - simp only [IH hnr.le, Ne.def, mul_transvection_apply_of_ne, Ne.symm h, inl.injEq] + simp only [IH hnr.le, Ne.def, mul_transvection_apply_of_ne, Ne.symm h, inl.injEq, + not_false_eq_true] rcases le_or_lt (n + 1) i with (hi | hi) · simp [hi, n.le_succ.trans hi, if_true] · rw [if_neg, if_neg] diff --git a/Mathlib/Logic/Embedding/Basic.lean b/Mathlib/Logic/Embedding/Basic.lean index 977d82afec1b7..5aac7a405c639 100644 --- a/Mathlib/Logic/Embedding/Basic.lean +++ b/Mathlib/Logic/Embedding/Basic.lean @@ -192,7 +192,7 @@ def setValue {α β} (f : α ↪ β) (a : α) (b : β) [∀ a', Decidable (a' = -- split_ifs at h <;> (try subst b) <;> (try simp only [f.injective.eq_iff] at *) <;> cc split_ifs at h with h₁ h₂ _ _ h₅ h₆ <;> (try subst b) <;> - (try simp only [f.injective.eq_iff] at *) + (try simp only [f.injective.eq_iff, not_true_eq_false] at *) · rw[h₁,h₂] · rw[h₁,h] · rw[h₅,←h] diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean index eef2f286c2576..6a6beae60542b 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean @@ -1645,8 +1645,7 @@ theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow [MeasurableSpace simp only [mem_singleton_iff, mem_union, mem_Ioo, mem_Ioi, mem_preimage] have H : f x = ∞ ∨ f x < ∞ := eq_or_lt_of_le le_top cases' H with H H - · simp only [H, eq_self_iff_true, or_false_iff, WithTop.zero_lt_top, not_top_lt, - and_false_iff] + · simp only [H, eq_self_iff_true, or_false_iff, zero_lt_top, not_top_lt, and_false_iff] · simp only [H, H.ne, and_true_iff, false_or_iff] · refine disjoint_left.2 fun x hx h'x => ?_ have : f x < ∞ := h'x.2.2 diff --git a/Mathlib/MeasureTheory/Covering/Besicovitch.lean b/Mathlib/MeasureTheory/Covering/Besicovitch.lean index 4044536644405..31b309490ea9e 100644 --- a/Mathlib/MeasureTheory/Covering/Besicovitch.lean +++ b/Mathlib/MeasureTheory/Covering/Besicovitch.lean @@ -928,7 +928,7 @@ theorem exists_closedBall_covering_tsum_measure_le (μ : Measure α) [SigmaFinit obtain ⟨u, su, u_open, μu⟩ : ∃ U, U ⊇ s ∧ IsOpen U ∧ μ U ≤ μ s + ε / 2 := Set.exists_isOpen_le_add _ _ (by - simpa only [or_false_iff, Ne.def, ENNReal.div_eq_zero_iff, ENNReal.one_ne_top] using hε) + simpa only [or_false, Ne.def, ENNReal.div_eq_zero_iff, ENNReal.two_ne_top] using hε) have : ∀ x ∈ s, ∃ R > 0, ball x R ⊆ u := fun x hx => Metric.mem_nhds_iff.1 (u_open.mem_nhds (su hx)) choose! R hR using this @@ -946,8 +946,8 @@ theorem exists_closedBall_covering_tsum_measure_le (μ : Measure α) [SigmaFinit obtain ⟨v, s'v, v_open, μv⟩ : ∃ v, v ⊇ s' ∧ IsOpen v ∧ μ v ≤ μ s' + ε / 2 / N := Set.exists_isOpen_le_add _ _ (by - simp only [hε, ENNReal.nat_ne_top, WithTop.mul_eq_top_iff, Ne.def, ENNReal.div_eq_zero_iff, - ENNReal.one_ne_top, not_false_iff, and_false_iff, false_and_iff, or_self_iff]) + simp only [ne_eq, ENNReal.div_eq_zero_iff, hε, ENNReal.two_ne_top, or_self, + ENNReal.nat_ne_top, not_false_eq_true]) have : ∀ x ∈ s', ∃ r1 ∈ f x ∩ Ioo (0 : ℝ) 1, closedBall x r1 ⊆ v := by intro x hx rcases Metric.mem_nhds_iff.1 (v_open.mem_nhds (s'v hx)) with ⟨r, rpos, hr⟩ diff --git a/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean b/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean index cf9189f17055a..fe2e0cf08bec2 100644 --- a/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean +++ b/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean @@ -211,7 +211,7 @@ theorem TendstoInMeasure.exists_seq_tendsto_ae (hfg : TendstoInMeasure μ f atTo set s := Filter.atTop.limsup S with hs have hμs : μ s = 0 := by refine' measure_limsup_eq_zero (ne_of_lt <| lt_of_le_of_lt (ENNReal.tsum_le_tsum hμS_le) _) - simp only [ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, inv_inv] + simp only [ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, ENNReal.two_lt_top, inv_inv] have h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x)) := by refine' fun x hx => Metric.tendsto_atTop.mpr fun ε hε => _ rw [hs, limsup_eq_iInf_iSup_of_nat] at hx diff --git a/Mathlib/MeasureTheory/Function/L1Space.lean b/Mathlib/MeasureTheory/Function/L1Space.lean index e8c37b1b68b8a..69cb75949f123 100644 --- a/Mathlib/MeasureTheory/Function/L1Space.lean +++ b/Mathlib/MeasureTheory/Function/L1Space.lean @@ -229,7 +229,7 @@ theorem HasFiniteIntegral.smul_measure {f : α → β} (h : HasFiniteIntegral f @[simp] theorem hasFiniteIntegral_zero_measure {m : MeasurableSpace α} (f : α → β) : HasFiniteIntegral f (0 : Measure α) := by - simp only [HasFiniteIntegral, lintegral_zero_measure, WithTop.zero_lt_top] + simp only [HasFiniteIntegral, lintegral_zero_measure, zero_lt_top] #align measure_theory.has_finite_integral_zero_measure MeasureTheory.hasFiniteIntegral_zero_measure variable (α β μ) diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm.lean b/Mathlib/MeasureTheory/Function/LpSeminorm.lean index d598845f2bd33..e6b3d6bc3d584 100644 --- a/Mathlib/MeasureTheory/Function/LpSeminorm.lean +++ b/Mathlib/MeasureTheory/Function/LpSeminorm.lean @@ -326,10 +326,10 @@ theorem snorm_const_lt_top_iff {p : ℝ≥0∞} {c : F} (hp_ne_zero : p ≠ 0) ( snorm (fun _ : α => c) p μ < ∞ ↔ c = 0 ∨ μ Set.univ < ∞ := by have hp : 0 < p.toReal := ENNReal.toReal_pos hp_ne_zero hp_ne_top by_cases hμ : μ = 0 - · simp only [hμ, Measure.coe_zero, Pi.zero_apply, or_true_iff, WithTop.zero_lt_top, + · simp only [hμ, Measure.coe_zero, Pi.zero_apply, or_true_iff, zero_lt_top, snorm_measure_zero] by_cases hc : c = 0 - · simp only [hc, true_or_iff, eq_self_iff_true, WithTop.zero_lt_top, snorm_zero'] + · simp only [hc, true_or_iff, eq_self_iff_true, zero_lt_top, snorm_zero'] rw [snorm_const' c hp_ne_zero hp_ne_top] by_cases hμ_top : μ Set.univ = ∞ · simp [hc, hμ_top, hp] @@ -356,7 +356,7 @@ theorem memℒp_const (c : E) [IsFiniteMeasure μ] : Memℒp (fun _ : α => c) p theorem memℒp_top_const (c : E) : Memℒp (fun _ : α => c) ∞ μ := by refine' ⟨aestronglyMeasurable_const, _⟩ by_cases h : μ = 0 - · simp only [h, snorm_measure_zero, WithTop.zero_lt_top] + · simp only [h, snorm_measure_zero, zero_lt_top] · rw [snorm_const _ ENNReal.top_ne_zero h] simp only [ENNReal.top_toReal, _root_.div_zero, ENNReal.rpow_zero, mul_one, ENNReal.coe_lt_top] #align measure_theory.mem_ℒp_top_const MeasureTheory.memℒp_top_const diff --git a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean index a6a68b4cc15bf..3b1595ea6cbaf 100644 --- a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean +++ b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean @@ -986,7 +986,7 @@ theorem Memℒp.induction_dense (hp_ne_top : p ≠ ∞) (P : (α → E) → Prop (h1P : ∀ f g, P f → P g → P (f + g)) (h2P : ∀ f, P f → AEStronglyMeasurable f μ) {f : α → E} (hf : Memℒp f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) : ∃ g : α → E, snorm (f - g) p μ ≤ ε ∧ P g := by rcases eq_or_ne p 0 with (rfl | hp_pos) - · rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, WithTop.zero_lt_top]) + · rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, zero_lt_top]) hε with ⟨g, _, Pg⟩ exact ⟨g, by simp only [snorm_exponent_zero, zero_le'], Pg⟩ suffices H : @@ -1001,7 +1001,7 @@ theorem Memℒp.induction_dense (hp_ne_top : p ≠ ∞) (P : (α → E) → Prop apply SimpleFunc.induction · intro c s hs ε εpos Hs rcases eq_or_ne c 0 with (rfl | hc) - · rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, WithTop.zero_lt_top]) + · rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, zero_lt_top]) εpos with ⟨g, hg, Pg⟩ rw [← snorm_neg, neg_sub] at hg refine' ⟨g, _, Pg⟩ diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean index 3073a23a47afb..fd654b405b9d1 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean +++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean @@ -982,7 +982,7 @@ theorem finStronglyMeasurable_zero {α β} {m : MeasurableSpace α} {μ : Measur [TopologicalSpace β] : FinStronglyMeasurable (0 : α → β) μ := ⟨0, by simp only [Pi.zero_apply, SimpleFunc.coe_zero, support_zero', measure_empty, - WithTop.zero_lt_top, forall_const], + zero_lt_top, forall_const], fun _ => tendsto_const_nhds⟩ #align measure_theory.fin_strongly_measurable_zero MeasureTheory.finStronglyMeasurable_zero diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean index df6c71a061f5e..e1678df86b8cf 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner.lean @@ -1265,7 +1265,7 @@ theorem integral_nonpos {f : α → ℝ} (hf : f ≤ 0) : ∫ a, f a ∂μ ≤ 0 theorem integral_eq_zero_iff_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfi : Integrable f μ) : ∫ x, f x ∂μ = 0 ↔ f =ᵐ[μ] 0 := by simp_rw [integral_eq_lintegral_of_nonneg_ae hf hfi.1, ENNReal.toReal_eq_zero_iff, - ← ENNReal.not_lt_top, ← hasFiniteIntegral_iff_ofReal hf, hfi.2, or_false_iff] + ← ENNReal.not_lt_top, ← hasFiniteIntegral_iff_ofReal hf, hfi.2, not_true_eq_false, or_false_iff] -- Porting note: split into parts, to make `rw` and `simp` work rw [lintegral_eq_zero_iff'] · rw [← hf.le_iff_eq, Filter.EventuallyEq, Filter.EventuallyLE] diff --git a/Mathlib/MeasureTheory/Integral/SetIntegral.lean b/Mathlib/MeasureTheory/Integral/SetIntegral.lean index 3967342254245..1343285c8ca35 100644 --- a/Mathlib/MeasureTheory/Integral/SetIntegral.lean +++ b/Mathlib/MeasureTheory/Integral/SetIntegral.lean @@ -1260,10 +1260,10 @@ theorem integral_smul_const {𝕜 : Type*} [IsROrC 𝕜] [NormedSpace 𝕜 E] [C by_cases hf : Integrable f μ · exact ((1 : 𝕜 →L[𝕜] 𝕜).smulRight c).integral_comp_comm hf · by_cases hc : c = 0 - · simp only [hc, integral_zero, smul_zero] + · simp [hc, integral_zero, smul_zero] rw [integral_undef hf, integral_undef, zero_smul] rw [integrable_smul_const hc] - simp_rw [hf] + simp_rw [hf, not_false_eq_true] #align integral_smul_const integral_smul_const theorem integral_withDensity_eq_integral_smul {f : α → ℝ≥0} (f_meas : Measurable f) (g : α → E) : diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean index 49ee1df879122..6858344d54368 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean @@ -665,7 +665,7 @@ instance isHaarMeasure_haarMeasure (K₀ : PositiveCompacts G) : IsHaarMeasure ( isHaarMeasure_of_isCompact_nonempty_interior (haarMeasure K₀) K₀ K₀.isCompact K₀.interior_nonempty · simp only [haarMeasure_self]; exact one_ne_zero - · simp only [haarMeasure_self] + · simp only [haarMeasure_self, ne_eq, ENNReal.one_ne_top, not_false_eq_true] #align measure_theory.measure.is_haar_measure_haar_measure MeasureTheory.Measure.isHaarMeasure_haarMeasure #align measure_theory.measure.is_add_haar_measure_add_haar_measure MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean index 8f33396a8948a..82c7cf8d226fa 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean +++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean @@ -3261,7 +3261,7 @@ theorem FiniteAtFilter.exists_mem_basis {f : Filter α} (hμ : FiniteAtFilter μ #align measure_theory.measure.finite_at_filter.exists_mem_basis MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis theorem finiteAtBot {m0 : MeasurableSpace α} (μ : Measure α) : μ.FiniteAtFilter ⊥ := - ⟨∅, mem_bot, by simp only [measure_empty, WithTop.zero_lt_top]⟩ + ⟨∅, mem_bot, by simp only [measure_empty, zero_lt_top]⟩ #align measure_theory.measure.finite_at_bot MeasureTheory.Measure.finiteAtBot /-- `μ` has finite spanning sets in `C` if there is a countable sequence of sets in `C` that have diff --git a/Mathlib/NumberTheory/Bernoulli.lean b/Mathlib/NumberTheory/Bernoulli.lean index 4184598955f54..8de2a7d4d5ae6 100644 --- a/Mathlib/NumberTheory/Bernoulli.lean +++ b/Mathlib/NumberTheory/Bernoulli.lean @@ -125,7 +125,7 @@ theorem bernoulli'_three : bernoulli' 3 = 0 := by @[simp] theorem bernoulli'_four : bernoulli' 4 = -1 / 30 := by - have : Nat.choose 4 2 = 6 := by norm_num -- shrug + have : Nat.choose 4 2 = 6 := by decide -- shrug rw [bernoulli'_def] norm_num [sum_range_succ, sum_range_succ, sum_range_zero, this] #align bernoulli'_four bernoulli'_four @@ -185,7 +185,7 @@ theorem bernoulli'_odd_eq_zero {n : ℕ} (h_odd : Odd n) (hlt : 1 < n) : bernoul · apply eq_zero_of_neg_eq specialize h n split_ifs at h <;> simp_all [h_odd.neg_one_pow, factorial_ne_zero] - · simpa [Nat.factorial] using h 1 + · simpa (config := {decide := true}) [Nat.factorial] using h 1 have h : B * (exp ℚ - 1) = X * exp ℚ := by simpa [bernoulli'PowerSeries] using bernoulli'PowerSeries_mul_exp_sub_one ℚ rw [sub_mul, h, mul_sub X, sub_right_inj, ← neg_sub, mul_neg, neg_eq_iff_eq_neg] @@ -349,7 +349,7 @@ theorem sum_range_pow (n p : ℕ) : have hexp : exp ℚ - 1 ≠ 0 := by simp only [exp, PowerSeries.ext_iff, Ne, not_forall] use 1 - simp + simp [factorial_ne_zero] have h_r : exp ℚ ^ n - 1 = X * mk fun p => coeff ℚ (p + 1) (exp ℚ ^ n) := by have h_const : C ℚ (constantCoeff ℚ (exp ℚ ^ n)) = 1 := by simp rw [← h_const, sub_const_eq_X_mul_shift] diff --git a/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean b/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean index 83c3817c8cbaf..17d08ac9eb5f7 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean @@ -176,7 +176,7 @@ theorem discr_prime_pow [hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact ( simp only [discr, traceMatrix_apply, Matrix.det_unique, Fin.default_eq_zero, Fin.val_zero, _root_.pow_zero, traceForm_apply, mul_one] rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr, hp, hk]; norm_num - simp [← coe_two] + simp [← coe_two, Even.neg_pow (by decide : Even (1 / 2))] · exact discr_prime_pow_ne_two hζ hirr hk #align is_cyclotomic_extension.discr_prime_pow IsCyclotomicExtension.discr_prime_pow diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean index d520899da0a0d..5b2b78cc50727 100644 --- a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean +++ b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean @@ -469,7 +469,7 @@ theorem pow_sub_one_norm_prime_pow_of_ne_zero {k s : ℕ} (hζ : IsPrimitiveRoot rw [← PNat.coe_inj, PNat.pow_coe, ← pow_one 2] at htwo replace htwo := eq_of_prime_pow_eq (prime_iff.1 hpri.out) (prime_iff.1 Nat.prime_two) (succ_pos _) htwo - rwa [show 2 = ((2 : ℕ+) : ℕ) by simp, PNat.coe_inj] at htwo + rwa [show 2 = ((2 : ℕ+) : ℕ) by decide, PNat.coe_inj] at htwo replace hs : s = k · rw [hp, ← PNat.coe_inj, PNat.pow_coe] at htwo nth_rw 2 [← pow_one 2] at htwo diff --git a/Mathlib/NumberTheory/Divisors.lean b/Mathlib/NumberTheory/Divisors.lean index 6ab57f89f54c3..7a90aaed0a596 100644 --- a/Mathlib/NumberTheory/Divisors.lean +++ b/Mathlib/NumberTheory/Divisors.lean @@ -404,7 +404,8 @@ theorem properDivisors_eq_singleton_one_iff_prime : n.properDivisors = {1} ↔ n · simp [hdvd, this] exact (le_iff_eq_or_lt.mp this).symm · by_contra' - simp [nonpos_iff_eq_zero.mp this, this] at h + simp only [nonpos_iff_eq_zero.mp this, this] at h + contradiction · exact fun h => Prime.properDivisors h #align nat.proper_divisors_eq_singleton_one_iff_prime Nat.properDivisors_eq_singleton_one_iff_prime diff --git a/Mathlib/NumberTheory/FLT/Four.lean b/Mathlib/NumberTheory/FLT/Four.lean index ab76f84eefc1b..d72959e080fbc 100644 --- a/Mathlib/NumberTheory/FLT/Four.lean +++ b/Mathlib/NumberTheory/FLT/Four.lean @@ -131,7 +131,7 @@ theorem exists_odd_minimal {a b c : ℤ} (h : Fermat42 a b c) : Int.dvd_gcd (Int.dvd_of_emod_eq_zero hap) (Int.dvd_of_emod_eq_zero hbp) rw [Int.gcd_eq_one_iff_coprime.mpr (coprime_of_minimal hf)] at h1 revert h1 - norm_num + decide · exact ⟨b0, ⟨a0, ⟨c0, minimal_comm hf, hbp⟩⟩⟩ exact ⟨a0, ⟨b0, ⟨c0, hf, hap⟩⟩⟩ #align fermat_42.exists_odd_minimal Fermat42.exists_odd_minimal @@ -179,7 +179,7 @@ theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0 -- it helps if we know the parity of a ^ 2 (and the sign of c): have ha22 : a ^ 2 % 2 = 1 := by rw [sq, Int.mul_emod, ha2] - norm_num + decide obtain ⟨m, n, ht1, ht2, ht3, ht4, ht5, ht6⟩ := ht.coprime_classification' h2 ha22 hc -- Now a, n, m form a pythagorean triple and so we can obtain r and s such that -- a = r ^ 2 - s ^ 2, n = 2 * r * s and m = r ^ 2 + s ^ 2 diff --git a/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean b/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean index 29e832b2e7e19..7b15dceee2531 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean @@ -468,7 +468,7 @@ theorem quadratic_reciprocity_three_mod_four {a b : ℕ} (ha : a % 4 = 3) (hb : theorem mod_right' (a : ℕ) {b : ℕ} (hb : Odd b) : J(a | b) = J(a | b % (4 * a)) := by rcases eq_or_ne a 0 with (rfl | ha₀) · rw [mul_zero, mod_zero] - have hb' : Odd (b % (4 * a)) := hb.mod_even (Even.mul_right (by norm_num) _) + have hb' : Odd (b % (4 * a)) := hb.mod_even (Even.mul_right (by decide) _) rcases exists_eq_pow_mul_and_not_dvd ha₀ 2 (by norm_num) with ⟨e, a', ha₁', ha₂⟩ have ha₁ := odd_iff.mpr (two_dvd_ne_zero.mp ha₁') nth_rw 2 [ha₂]; nth_rw 1 [ha₂] @@ -493,7 +493,7 @@ theorem mod_right' (a : ℕ) {b : ℕ} (hb : Odd b) : J(a | b) = J(a | b % (4 * theorem mod_right (a : ℤ) {b : ℕ} (hb : Odd b) : J(a | b) = J(a | b % (4 * a.natAbs)) := by cases' Int.natAbs_eq a with ha ha <;> nth_rw 2 [ha] <;> nth_rw 1 [ha] · exact mod_right' a.natAbs hb - · have hb' : Odd (b % (4 * a.natAbs)) := hb.mod_even (Even.mul_right (by norm_num) _) + · have hb' : Odd (b % (4 * a.natAbs)) := hb.mod_even (Even.mul_right (by decide) _) rw [jacobiSym.neg _ hb, jacobiSym.neg _ hb', mod_right' _ hb, χ₄_nat_mod_four, χ₄_nat_mod_four (b % (4 * _)), mod_mod_of_dvd b (dvd_mul_right 4 _)] #align jacobi_sym.mod_right jacobiSym.mod_right diff --git a/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean b/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean index 4a608d0f1874e..aa50a12f53dbb 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean @@ -85,7 +85,7 @@ theorem quadraticCharFun_one : quadraticCharFun F 1 = 1 := by theorem quadraticCharFun_eq_one_of_char_two (hF : ringChar F = 2) {a : F} (ha : a ≠ 0) : quadraticCharFun F a = 1 := by simp only [quadraticCharFun, ha, if_false, ite_eq_left_iff] - exact fun h => h (FiniteField.isSquare_of_char_two hF a) + exact fun h => (h (FiniteField.isSquare_of_char_two hF a)).elim #align quadratic_char_fun_eq_one_of_char_two quadraticCharFun_eq_one_of_char_two /-- If `ringChar F` is odd, then `quadraticCharFun F a` can be computed in diff --git a/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean b/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean index f7d3bddc79562..3fe7b1f41e066 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean @@ -54,7 +54,7 @@ theorem FiniteField.isSquare_two_iff : simp only [h, Nat.one_ne_zero, if_false, ite_eq_left_iff, Ne.def, (by decide : (-1 : ℤ) ≠ 1), imp_false, Classical.not_not] all_goals - rw [← Nat.mod_mod_of_dvd _ (by norm_num : 2 ∣ 8)] at h + rw [← Nat.mod_mod_of_dvd _ (by decide : 2 ∣ 8)] at h have h₁ := Nat.mod_lt (Fintype.card F) (by decide : 0 < 8) revert h₁ h generalize Fintype.card F % 8 = n @@ -65,7 +65,7 @@ theorem FiniteField.isSquare_two_iff : theorem quadraticChar_neg_two [DecidableEq F] (hF : ringChar F ≠ 2) : quadraticChar F (-2) = χ₈' (Fintype.card F) := by rw [(by norm_num : (-2 : F) = -1 * 2), map_mul, χ₈'_eq_χ₄_mul_χ₈, quadraticChar_neg_one hF, - quadraticChar_two hF, @cast_nat_cast _ (ZMod 4) _ _ _ (by norm_num : 4 ∣ 8)] + quadraticChar_two hF, @cast_nat_cast _ (ZMod 4) _ _ _ (by decide : 4 ∣ 8)] #align quadratic_char_neg_two quadraticChar_neg_two /-- `-2` is a square in `F` iff `#F` is not congruent to `5` or `7` mod `8`. -/ @@ -84,7 +84,7 @@ theorem FiniteField.isSquare_neg_two_iff : simp only [h, Nat.one_ne_zero, if_false, ite_eq_left_iff, Ne.def, (by decide : (-1 : ℤ) ≠ 1), imp_false, Classical.not_not] all_goals - rw [← Nat.mod_mod_of_dvd _ (by norm_num : 2 ∣ 8)] at h + rw [← Nat.mod_mod_of_dvd _ (by decide : 2 ∣ 8)] at h have h₁ := Nat.mod_lt (Fintype.card F) (by decide : 0 < 8) revert h₁ h generalize Fintype.card F % 8 = n diff --git a/Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean b/Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean index 52d412108318c..36b611aecfb82 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean @@ -78,7 +78,7 @@ variable (hp : p ≠ 2) theorem exists_sq_eq_two_iff : IsSquare (2 : ZMod p) ↔ p % 8 = 1 ∨ p % 8 = 7 := by rw [FiniteField.isSquare_two_iff, card p] have h₁ := Prime.mod_two_eq_one_iff_ne_two.mpr hp - rw [← mod_mod_of_dvd p (by norm_num : 2 ∣ 8)] at h₁ + rw [← mod_mod_of_dvd p (by decide : 2 ∣ 8)] at h₁ have h₂ := mod_lt p (by norm_num : 0 < 8) revert h₂ h₁ generalize p % 8 = m; clear! p @@ -89,7 +89,7 @@ theorem exists_sq_eq_two_iff : IsSquare (2 : ZMod p) ↔ p % 8 = 1 ∨ p % 8 = 7 theorem exists_sq_eq_neg_two_iff : IsSquare (-2 : ZMod p) ↔ p % 8 = 1 ∨ p % 8 = 3 := by rw [FiniteField.isSquare_neg_two_iff, card p] have h₁ := Prime.mod_two_eq_one_iff_ne_two.mpr hp - rw [← mod_mod_of_dvd p (by norm_num : 2 ∣ 8)] at h₁ + rw [← mod_mod_of_dvd p (by decide : 2 ∣ 8)] at h₁ have h₂ := mod_lt p (by norm_num : 0 < 8) revert h₂ h₁ generalize p % 8 = m; clear! p diff --git a/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean b/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean index 7b7731b54bbf6..61dc2f08096cd 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean @@ -67,7 +67,7 @@ theorem χ₄_int_eq_if_mod_four (n : ℤ) : χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 := by have help : ∀ m : ℤ, 0 ≤ m → m < 4 → χ₄ m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1 := by decide - rw [← Int.emod_emod_of_dvd n (by norm_num : (2 : ℤ) ∣ 4), ← ZMod.int_cast_mod n 4] + rw [← Int.emod_emod_of_dvd n (by decide : (2 : ℤ) ∣ 4), ← ZMod.int_cast_mod n 4] exact help (n % 4) (Int.emod_nonneg n (by norm_num)) (Int.emod_lt n (by norm_num)) #align zmod.χ₄_int_eq_if_mod_four ZMod.χ₄_int_eq_if_mod_four @@ -88,7 +88,7 @@ theorem χ₄_eq_neg_one_pow {n : ℕ} (hn : n % 2 = 1) : χ₄ n = (-1) ^ (n / have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → ite (m = 1) (1 : ℤ) (-1) = (-1) ^ (m / 2) := by decide exact help (n % 4) (Nat.mod_lt n (by norm_num)) - ((Nat.mod_mod_of_dvd n (by norm_num : 2 ∣ 4)).trans hn) + ((Nat.mod_mod_of_dvd n (by decide : 2 ∣ 4)).trans hn) #align zmod.χ₄_eq_neg_one_pow ZMod.χ₄_eq_neg_one_pow /-- If `n % 4 = 1`, then `χ₄ n = 1`. -/ @@ -162,7 +162,7 @@ theorem χ₈_int_eq_if_mod_eight (n : ℤ) : have help : ∀ m : ℤ, 0 ≤ m → m < 8 → χ₈ m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 := by decide - rw [← Int.emod_emod_of_dvd n (by norm_num : (2 : ℤ) ∣ 8), ← ZMod.int_cast_mod n 8] + rw [← Int.emod_emod_of_dvd n (by decide : (2 : ℤ) ∣ 8), ← ZMod.int_cast_mod n 8] exact help (n % 8) (Int.emod_nonneg n (by norm_num)) (Int.emod_lt n (by norm_num)) #align zmod.χ₈_int_eq_if_mod_eight ZMod.χ₈_int_eq_if_mod_eight @@ -195,7 +195,7 @@ theorem χ₈'_int_eq_if_mod_eight (n : ℤ) : have help : ∀ m : ℤ, 0 ≤ m → m < 8 → χ₈' m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 := by decide - rw [← Int.emod_emod_of_dvd n (by norm_num : (2 : ℤ) ∣ 8), ← ZMod.int_cast_mod n 8] + rw [← Int.emod_emod_of_dvd n (by decide : (2 : ℤ) ∣ 8), ← ZMod.int_cast_mod n 8] exact help (n % 8) (Int.emod_nonneg n (by norm_num)) (Int.emod_lt n (by norm_num)) #align zmod.χ₈'_int_eq_if_mod_eight ZMod.χ₈'_int_eq_if_mod_eight @@ -212,7 +212,7 @@ theorem χ₈'_eq_χ₄_mul_χ₈ (a : ZMod 8) : χ₈' a = χ₄ a * χ₈ a := #align zmod.χ₈'_eq_χ₄_mul_χ₈ ZMod.χ₈'_eq_χ₄_mul_χ₈ theorem χ₈'_int_eq_χ₄_mul_χ₈ (a : ℤ) : χ₈' a = χ₄ a * χ₈ a := by - rw [← @cast_int_cast 8 (ZMod 4) _ 4 _ (by norm_num) a] + rw [← @cast_int_cast 8 (ZMod 4) _ 4 _ (by decide) a] exact χ₈'_eq_χ₄_mul_χ₈ a #align zmod.χ₈'_int_eq_χ₄_mul_χ₈ ZMod.χ₈'_int_eq_χ₄_mul_χ₈ diff --git a/Mathlib/NumberTheory/Multiplicity.lean b/Mathlib/NumberTheory/Multiplicity.lean index e157f1c4438e8..004804dfabbc7 100644 --- a/Mathlib/NumberTheory/Multiplicity.lean +++ b/Mathlib/NumberTheory/Multiplicity.lean @@ -269,13 +269,13 @@ theorem Int.sq_mod_four_eq_one_of_odd {x : ℤ} : Odd x → x ^ 2 % 4 = 1 := by rcases hx with ⟨_, rfl⟩ ring_nf rw [add_assoc, ← add_mul, Int.add_mul_emod_self] - norm_num + decide #align int.sq_mod_four_eq_one_of_odd Int.sq_mod_four_eq_one_of_odd theorem Int.two_pow_two_pow_add_two_pow_two_pow {x y : ℤ} (hx : ¬2 ∣ x) (hxy : 4 ∣ x - y) (i : ℕ) : multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑(1 : ℕ) := by have hx_odd : Odd x := by rwa [Int.odd_iff_not_even, even_iff_two_dvd] - have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by norm_num) hxy) + have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by decide) hxy) have hy_odd : Odd y := by simpa using hx_odd.sub_even hxy_even refine' multiplicity.eq_coe_iff.mpr ⟨_, _⟩ · rw [pow_one, ← even_iff_two_dvd] @@ -292,7 +292,7 @@ theorem Int.two_pow_two_pow_add_two_pow_two_pow {x y : ℤ} (hx : ¬2 ∣ x) (hx suffices ∀ x : ℤ, Odd x → x ^ 2 ^ (i + 1) % 4 = 1 by rw [show (2 ^ (1 + 1) : ℤ) = 4 by norm_num, Int.dvd_iff_emod_eq_zero, Int.add_emod, this _ hx_odd, this _ hy_odd] - norm_num + decide intro x hx rw [pow_succ, mul_comm, pow_mul, Int.sq_mod_four_eq_one_of_odd hx.pow] #align int.two_pow_two_pow_add_two_pow_two_pow Int.two_pow_two_pow_add_two_pow_two_pow @@ -307,7 +307,7 @@ theorem Int.two_pow_two_pow_sub_pow_two_pow {x y : ℤ} (n : ℕ) (hxy : 4 ∣ x theorem Int.two_pow_sub_pow' {x y : ℤ} (n : ℕ) (hxy : 4 ∣ x - y) (hx : ¬2 ∣ x) : multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity (2 : ℤ) n := by have hx_odd : Odd x := by rwa [Int.odd_iff_not_even, even_iff_two_dvd] - have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by norm_num) hxy) + have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by decide) hxy) have hy_odd : Odd y := by simpa using hx_odd.sub_even hxy_even cases' n with n · simp only [pow_zero, sub_self, multiplicity.zero, Int.ofNat_zero, Nat.zero_eq, add_top] diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean index 83380bf8ef22d..7eff44a07ffdf 100644 --- a/Mathlib/NumberTheory/NumberField/Embeddings.lean +++ b/Mathlib/NumberTheory/NumberField/Embeddings.lean @@ -476,7 +476,7 @@ theorem card_complex_embeddings : · rwa [Subtype.mk_eq_mk, ← Subtype.ext_iff, ← Subtype.ext_iff] at h · refine ⟨⟨⟨φ, not_isReal_of_mk_isComplex (hφ.symm ▸ hw)⟩, ?_⟩, rfl⟩ rwa [Subtype.ext_iff, mkComplex_coe] - · simp_rw [mult, not_isReal_iff_isComplex.mpr hw] + · simp_rw [mult, not_isReal_iff_isComplex.mpr hw, ite_false] #align number_field.infinite_place.card_complex_embeddings NumberField.InfinitePlace.card_complex_embeddings theorem card_add_two_mul_card_eq_rank : diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index f0869351c7076..63ea9a81746f3 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -226,7 +226,7 @@ theorem mult_log_place_eq_zero {x : (𝓞 K)ˣ} {w : InfinitePlace K} : mult w * Real.log (w x) = 0 ↔ w x = 1 := by rw [mul_eq_zero, or_iff_right, Real.log_eq_zero, or_iff_right, or_iff_left] · linarith [(map_nonneg _ _ : 0 ≤ w x)] - · simp only [ne_eq, map_eq_zero, coe_ne_zero x] + · simp only [ne_eq, map_eq_zero, coe_ne_zero x, not_false_eq_true] · refine (ne_of_gt ?_) rw [mult]; split_ifs <;> norm_num @@ -347,7 +347,7 @@ theorem seq_next {x : 𝓞 K} (hx : x ≠ 0) : simp_rw [← NNReal.coe_pow, ← NNReal.coe_prod] exact le_of_eq (congr_arg toReal h_gprod) · refine div_lt_self ?_ (by norm_num) - simp only [pos_iff, ne_eq, ZeroMemClass.coe_eq_zero, hx] + simp only [pos_iff, ne_eq, ZeroMemClass.coe_eq_zero, hx, not_false_eq_true] intro _ _ rw [ne_eq, Nonneg.mk_eq_zero, div_eq_zero_iff, map_eq_zero, not_or, ZeroMemClass.coe_eq_zero] exact ⟨hx, by norm_num⟩ @@ -413,7 +413,7 @@ theorem exists_unit (w₁ : InfinitePlace K) : (Ideal.span ({ (seq K w₁ hB n : 𝓞 K) }) = Ideal.span ({ (seq K w₁ hB m : 𝓞 K) })) · have hu := Ideal.span_singleton_eq_span_singleton.mp h refine ⟨hu.choose, fun w hw => Real.log_neg ?_ ?_⟩ - · simp only [pos_iff, ne_eq, ZeroMemClass.coe_eq_zero, ne_zero] + · simp only [pos_iff, ne_eq, ZeroMemClass.coe_eq_zero, ne_zero, not_false_eq_true] · calc _ = w ((seq K w₁ hB m : K) * (seq K w₁ hB n : K)⁻¹) := by rw [← congr_arg ((↑) : (𝓞 K) → K) hu.choose_spec, mul_comm, Submonoid.coe_mul, diff --git a/Mathlib/NumberTheory/Pell.lean b/Mathlib/NumberTheory/Pell.lean index a68df8142d5d3..bba6c74e643fb 100644 --- a/Mathlib/NumberTheory/Pell.lean +++ b/Mathlib/NumberTheory/Pell.lean @@ -551,7 +551,7 @@ theorem y_strictMono {a : Solution₁ d} (h : IsFundamental a) : add_pos_of_pos_of_nonneg (mul_pos (x_zpow_pos h.x_pos _) h.2.1) (mul_nonneg _ (by rw [sub_nonneg]; exact h.1.le)) rcases hn.eq_or_lt with (rfl | hn) - · simp only [zpow_zero, y_one] + · simp only [zpow_zero, y_one, le_refl] · exact (y_zpow_pos h.x_pos h.2.1 hn).le refine' strictMono_int_of_lt_succ fun n => _ cases' le_or_lt 0 n with hn hn diff --git a/Mathlib/NumberTheory/PellMatiyasevic.lean b/Mathlib/NumberTheory/PellMatiyasevic.lean index 78a8edff6b0cd..f108fc103fc1c 100644 --- a/Mathlib/NumberTheory/PellMatiyasevic.lean +++ b/Mathlib/NumberTheory/PellMatiyasevic.lean @@ -551,8 +551,8 @@ theorem yn_modEq_a_sub_one : ∀ n, yn a1 n ≡ n [MOD a - 1] #align pell.yn_modeq_a_sub_one Pell.yn_modEq_a_sub_one theorem yn_modEq_two : ∀ n, yn a1 n ≡ n [MOD 2] - | 0 => by simp - | 1 => by simp + | 0 => by rfl + | 1 => by simp; rfl | n + 2 => (yn_modEq_two n).add_right_cancel <| by rw [yn_succ_succ, mul_assoc, (by ring : n + 2 + n = 2 * (n + 1))] diff --git a/Mathlib/NumberTheory/PythagoreanTriples.lean b/Mathlib/NumberTheory/PythagoreanTriples.lean index 33b39e9744483..e909fe28d2c6a 100644 --- a/Mathlib/NumberTheory/PythagoreanTriples.lean +++ b/Mathlib/NumberTheory/PythagoreanTriples.lean @@ -29,7 +29,7 @@ the bulk of the proof below. theorem sq_ne_two_fin_zmod_four (z : ZMod 4) : z * z ≠ 2 := by change Fin 4 at z - fin_cases z <;> norm_num [Fin.ext_iff] + fin_cases z <;> decide #align sq_ne_two_fin_zmod_four sq_ne_two_fin_zmod_four theorem Int.sq_ne_two_mod_four (z : ℤ) : z * z % 4 ≠ 2 := by @@ -155,7 +155,8 @@ theorem even_odd_of_coprime (hc : Int.gcd x y = 1) : rw [show z * z = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2 by rw [← h.eq] ring] - norm_num [Int.add_emod] + simp only [Int.add_emod, Int.mul_emod_right, zero_add] + decide #align pythagorean_triple.even_odd_of_coprime PythagoreanTriple.even_odd_of_coprime theorem gcd_dvd : (Int.gcd x y : ℤ) ∣ z := by @@ -243,10 +244,10 @@ theorem isPrimitiveClassified_of_coprime_of_zero_left (hc : Int.gcd x y = 1) (hx cases' Int.natAbs_eq y with hy hy · use 1, 0 rw [hy, hc, Int.gcd_zero_right] - norm_num + decide · use 0, 1 rw [hy, hc, Int.gcd_zero_left] - norm_num + decide #align pythagorean_triple.is_primitive_classified_of_coprime_of_zero_left PythagoreanTriple.isPrimitiveClassified_of_coprime_of_zero_left theorem coprime_of_coprime (hc : Int.gcd x y = 1) : Int.gcd y z = 1 := by @@ -339,7 +340,9 @@ private theorem coprime_sq_sub_sq_add_of_even_odd {m n : ℤ} (h : Int.gcd m n = have hnc : p = 2 ∨ p ∣ Int.natAbs n := prime_two_or_dvd_of_dvd_two_mul_pow_self_two hp h2n by_cases h2 : p = 2 -- Porting note: norm_num is not enough to close h3 - · have h3 : (m ^ 2 + n ^ 2) % 2 = 1 := by field_simp [sq, Int.add_emod, Int.mul_emod, hm, hn] + · have h3 : (m ^ 2 + n ^ 2) % 2 = 1 := by + simp only [sq, Int.add_emod, Int.mul_emod, hm, hn, dvd_refl, Int.emod_emod_of_dvd] + decide have h4 : (m ^ 2 + n ^ 2) % 2 = 0 := by apply Int.emod_eq_zero_of_dvd rwa [h2] at hp2 @@ -372,7 +375,9 @@ private theorem coprime_sq_sub_mul_of_even_odd {m n : ℤ} (h : Int.gcd m n = 1) rw [hp2'] apply mt Int.emod_eq_zero_of_dvd -- Porting note: norm_num is not enough to close this - field_simp [sq, Int.sub_emod, Int.mul_emod, hm, hn] + simp only [sq, Nat.cast_ofNat, Int.sub_emod, Int.mul_emod, hm, hn, + mul_zero, EuclideanDomain.zero_mod, mul_one, zero_sub] + decide apply mt (Int.dvd_gcd (Int.coe_nat_dvd_left.mpr hpm)) hnp apply or_self_iff.mp apply Int.Prime.dvd_mul' hp @@ -528,7 +533,7 @@ theorem isPrimitiveClassified_of_coprime_of_odd_of_pos (hc : Int.gcd x y = 1) (h Int.dvd_gcd (Int.dvd_of_emod_eq_zero hn2) (Int.dvd_of_emod_eq_zero hm2) rw [hnmcp] at h1 revert h1 - norm_num + decide · -- m even, n odd apply h.isPrimitiveClassified_aux hc hzpos hm2n2 hv2 hw2 _ hmncp · apply Or.intro_left diff --git a/Mathlib/NumberTheory/Rayleigh.lean b/Mathlib/NumberTheory/Rayleigh.lean index 9b511a02cc709..6730de57895ac 100644 --- a/Mathlib/NumberTheory/Rayleigh.lean +++ b/Mathlib/NumberTheory/Rayleigh.lean @@ -117,8 +117,8 @@ theorem compl_beattySeq {r s : ℝ} (hrs : r.IsConjugateExponent s) : ext j by_cases h₁ : j ∈ {beattySeq r k | k} <;> by_cases h₂ : j ∈ {beattySeq' s k | k} · exact (Set.not_disjoint_iff.2 ⟨j, h₁, h₂⟩ (Beatty.no_collision hrs)).elim - · simp only [Set.mem_compl_iff, h₁, h₂] - · simp only [Set.mem_compl_iff, h₁, h₂] + · simp only [Set.mem_compl_iff, h₁, h₂, not_true_eq_false] + · simp only [Set.mem_compl_iff, h₁, h₂, not_false_eq_true] · have ⟨k, h₁₁, h₁₂⟩ := (Beatty.hit_or_miss hrs.pos).resolve_left h₁ have ⟨m, h₂₁, h₂₂⟩ := (Beatty.hit_or_miss' hrs.symm.pos).resolve_left h₂ exact (Beatty.no_anticollision hrs ⟨j, k, m, h₁₁, h₁₂, h₂₁, h₂₂⟩).elim diff --git a/Mathlib/NumberTheory/SumFourSquares.lean b/Mathlib/NumberTheory/SumFourSquares.lean index 05e44b1be541c..dae91282da785 100644 --- a/Mathlib/NumberTheory/SumFourSquares.lean +++ b/Mathlib/NumberTheory/SumFourSquares.lean @@ -187,7 +187,7 @@ protected theorem Prime.sum_four_squares {p : ℕ} (hp : p.Prime) : rcases (zero_le r).eq_or_gt with rfl | hr₀ · replace hr : f a = 0 ∧ f b = 0 ∧ f c = 0 ∧ f d = 0; · simpa [and_assoc] using hr obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩, ⟨c, rfl⟩, ⟨d, rfl⟩⟩ : m ∣ a ∧ m ∣ b ∧ m ∣ c ∧ m ∣ d - · simp only [← ZMod.nat_cast_zmod_eq_zero_iff_dvd, ← hf_mod, hr, Int.cast_zero] + · simp only [← ZMod.nat_cast_zmod_eq_zero_iff_dvd, ← hf_mod, hr, Int.cast_zero, and_self] have : m * m ∣ m * p := habcd ▸ ⟨a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2, by ring⟩ rw [mul_dvd_mul_iff_left hm₀.ne'] at this exact (hp.eq_one_or_self_of_dvd _ this).elim hm₁.ne' hmp.ne diff --git a/Mathlib/NumberTheory/SumTwoSquares.lean b/Mathlib/NumberTheory/SumTwoSquares.lean index 4936e6c381629..4829dcc69b667 100644 --- a/Mathlib/NumberTheory/SumTwoSquares.lean +++ b/Mathlib/NumberTheory/SumTwoSquares.lean @@ -109,7 +109,7 @@ theorem ZMod.isSquare_neg_one_iff {n : ℕ} (hn : Squarefree n) : refine' ⟨fun H q hqp hqd => hqp.mod_four_ne_three_of_dvd_isSquare_neg_one hqd H, fun H => _⟩ induction' n using induction_on_primes with p n hpp ih · exact False.elim (hn.ne_zero rfl) - · exact ⟨0, by simp only [Fin.zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]⟩ + · exact ⟨0, by simp only [mul_zero, eq_iff_true_of_subsingleton]⟩ · haveI : Fact p.Prime := ⟨hpp⟩ have hcp : p.Coprime n := by by_contra hc diff --git a/Mathlib/Order/Filter/AtTopBot.lean b/Mathlib/Order/Filter/AtTopBot.lean index 68510ec097ce0..f7d105a86cd15 100644 --- a/Mathlib/Order/Filter/AtTopBot.lean +++ b/Mathlib/Order/Filter/AtTopBot.lean @@ -2053,7 +2053,8 @@ theorem Monotone.piecewise_eventually_eq_iUnion {β : α → Type*} [Preorder ι · refine (eventually_ge_atTop i).mono fun j hij ↦ ?_ simp only [Set.piecewise_eq_of_mem, hs hij hi, subset_iUnion _ _ hi] · refine eventually_of_forall fun i ↦ ?_ - simp only [Set.piecewise_eq_of_not_mem, not_exists.1 ha i, mt mem_iUnion.1 ha] + simp only [Set.piecewise_eq_of_not_mem, not_exists.1 ha i, mt mem_iUnion.1 ha, + not_false_eq_true, exists_false] theorem Antitone.piecewise_eventually_eq_iInter {β : α → Type*} [Preorder ι] {s : ι → Set α} [∀ i, DecidablePred (· ∈ s i)] [DecidablePred (· ∈ ⋂ i, s i)] diff --git a/Mathlib/Order/Filter/ENNReal.lean b/Mathlib/Order/Filter/ENNReal.lean index 82cf5da48a02f..b43fbd981c410 100644 --- a/Mathlib/Order/Filter/ENNReal.lean +++ b/Mathlib/Order/Filter/ENNReal.lean @@ -65,7 +65,7 @@ theorem limsup_const_mul [CountableInterFilter f] {u : α → ℝ≥0∞} {a : have h_top_le : (f.limsup fun x : α => ite (u x = 0) (0 : ℝ≥0∞) ⊤) = ⊤ := eq_top_iff.mpr (le_limsup_of_frequently_le hu_mul) have hfu : f.limsup u ≠ 0 := mt limsup_eq_zero_iff.1 hu - simp only [ha_top, top_mul', hfu, h_top_le] + simp only [ha_top, top_mul', h_top_le, hfu, ite_false] #align ennreal.limsup_const_mul ENNReal.limsup_const_mul theorem limsup_mul_le [CountableInterFilter f] (u v : α → ℝ≥0∞) : diff --git a/Mathlib/Order/Filter/IndicatorFunction.lean b/Mathlib/Order/Filter/IndicatorFunction.lean index 5e405dfff62a7..e3b129df67696 100644 --- a/Mathlib/Order/Filter/IndicatorFunction.lean +++ b/Mathlib/Order/Filter/IndicatorFunction.lean @@ -31,7 +31,7 @@ theorem mulIndicator_eventuallyEq (hf : f =ᶠ[l ⊓ 𝓟 s] g) (hs : s =ᶠ[l] (eventually_inf_principal.1 hf).mp <| hs.mem_iff.mono fun x hst hfg => by_cases (fun hxs : x ∈ s => by simp only [*, hst.1 hxs, mulIndicator_of_mem]) - (fun hxs => by simp only [mulIndicator_of_not_mem, hxs, mt hst.2 hxs]) + (fun hxs => by simp only [mulIndicator_of_not_mem, hxs, mt hst.2 hxs, not_false_eq_true]) #align indicator_eventually_eq indicator_eventuallyEq end One diff --git a/Mathlib/Order/LocallyFinite.lean b/Mathlib/Order/LocallyFinite.lean index 6912e8eeb1b6e..8156f0d79f8f5 100644 --- a/Mathlib/Order/LocallyFinite.lean +++ b/Mathlib/Order/LocallyFinite.lean @@ -1081,8 +1081,8 @@ instance locallyFiniteOrder : LocallyFiniteOrder (WithTop α) where rw [some_mem_insertNone] simp | (a : α), (b : α), ⊤ => by - simp only [some, le_eq_subset, mem_map, mem_Icc, le_top, top_le_iff, and_false, iff_false, - not_exists, not_and, and_imp, Embedding.some, forall_const] + simp only [Embedding.some, mem_map, mem_Icc, and_false, exists_const, some, le_top, + top_le_iff] | (a : α), (b : α), (x : α) => by simp only [some, le_eq_subset, Embedding.some, mem_map, mem_Icc, Embedding.coeFn_mk, some_le_some] diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean index 82fa9a5474459..ff463656637fe 100644 --- a/Mathlib/Probability/Distributions/Gaussian.lean +++ b/Mathlib/Probability/Distributions/Gaussian.lean @@ -286,7 +286,7 @@ lemma gaussianReal_map_const_mul (c : ℝ) : rw [Measure.map_const] simp only [ne_eq, measure_univ, one_smul, mul_eq_zero] convert (gaussianReal_zero_var 0).symm - simp only [ne_eq, zero_pow', mul_eq_zero, hv, or_false] + simp only [ne_eq, zero_pow', mul_eq_zero, hv, or_false, not_false_eq_true] rfl let e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv have he' : ∀ x, HasDerivAt e ((fun _ ↦ c⁻¹) x) x := by diff --git a/Mathlib/Probability/Integration.lean b/Mathlib/Probability/Integration.lean index 10faa875ee53e..164def57b5de1 100644 --- a/Mathlib/Probability/Integration.lean +++ b/Mathlib/Probability/Integration.lean @@ -172,7 +172,7 @@ theorem IndepFun.integrable_left_of_integrable_mul {β : Type*} [MeasurableSpace have A : (∫⁻ ω, ‖X ω * Y ω‖₊ ∂μ) < ∞ := h'XY.2 simp only [nnnorm_mul, ENNReal.coe_mul] at A rw [lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.ennnorm hY.ennnorm J, H] at A - simp only [ENNReal.top_mul I] at A + simp only [ENNReal.top_mul I, lt_self_iff_false] at A #align probability_theory.indep_fun.integrable_left_of_integrable_mul ProbabilityTheory.IndepFun.integrable_left_of_integrable_mul /-- If the product of two independent real-valued random variables is integrable and the @@ -194,7 +194,7 @@ theorem IndepFun.integrable_right_of_integrable_mul {β : Type*} [MeasurableSpac have A : (∫⁻ ω, ‖X ω * Y ω‖₊ ∂μ) < ∞ := h'XY.2 simp only [nnnorm_mul, ENNReal.coe_mul] at A rw [lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.ennnorm hY.ennnorm J, H] at A - simp only [ENNReal.mul_top I] at A + simp only [ENNReal.mul_top I, lt_self_iff_false] at A #align probability_theory.indep_fun.integrable_right_of_integrable_mul ProbabilityTheory.IndepFun.integrable_right_of_integrable_mul /-- The (Bochner) integral of the product of two independent, nonnegative random diff --git a/Mathlib/Probability/Martingale/Convergence.lean b/Mathlib/Probability/Martingale/Convergence.lean index 63ea1272dbcee..d4383382f162c 100644 --- a/Mathlib/Probability/Martingale/Convergence.lean +++ b/Mathlib/Probability/Martingale/Convergence.lean @@ -399,7 +399,7 @@ theorem Integrable.tendsto_ae_condexp (hg : Integrable g μ) by_cases hnm : n ≤ m · exact ⟨m, (ℱ.mono hnm _ hs).inter ht⟩ · exact ⟨n, hs.inter (ℱ.mono (not_le.1 hnm).le _ ht)⟩ - · simp only [measure_empty, WithTop.zero_lt_top, Measure.restrict_empty, integral_zero_measure, + · simp only [measure_empty, ENNReal.zero_lt_top, Measure.restrict_empty, integral_zero_measure, forall_true_left] · rintro t ⟨n, ht⟩ - exact this n _ ht diff --git a/Mathlib/Probability/Martingale/Upcrossing.lean b/Mathlib/Probability/Martingale/Upcrossing.lean index 9b3b3b33a3e46..a1b10094646c1 100644 --- a/Mathlib/Probability/Martingale/Upcrossing.lean +++ b/Mathlib/Probability/Martingale/Upcrossing.lean @@ -699,7 +699,7 @@ theorem crossing_pos_eq (hab : a < b) : split_ifs with h₁ h₂ h₂ · simp_rw [← sub_le_iff_le_add, hf ω] · refine' False.elim (h₂ _) - simp_all only [Set.mem_Ici] + simp_all only [Set.mem_Ici, not_true_eq_false] · refine' False.elim (h₁ _) simp_all only [Set.mem_Ici] · rfl @@ -709,7 +709,7 @@ theorem crossing_pos_eq (hab : a < b) : split_ifs with h₁ h₂ h₂ · simp_rw [hf' ω] · refine' False.elim (h₂ _) - simp_all only [Set.mem_Iic] + simp_all only [Set.mem_Iic, not_true_eq_false] · refine' False.elim (h₁ _) simp_all only [Set.mem_Iic] · rfl diff --git a/Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean b/Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean index 6b1840e725a4c..4f954fbfa1e4c 100644 --- a/Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean +++ b/Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean @@ -93,6 +93,7 @@ private theorem pairMap_mem_pairs {k : ℕ} (t : Finset σ × σ) (h : t ∈ pai simp only [card_erase_of_mem h1, tsub_le_iff_right, mem_erase, ne_eq, h1] refine ⟨le_step h, ?_⟩ by_contra h2 + simp only [not_true_eq_false, and_true, not_forall, not_false_eq_true, exists_prop] at h2 rw [← h2] at h exact not_le_of_lt (sub_lt (card_pos.mpr ⟨t.snd, h1⟩) zero_lt_one) h · rw [pairMap_of_snd_nmem_fst σ h1] @@ -184,8 +185,9 @@ private theorem sum_filter_pairs_eq_sum_filter_antidiagonal_powersetCard_sum (k have hnk' : n.fst ≤ k := by apply le_of_lt; aesop aesop · simp_all only [mem_antidiagonal, mem_filter, mem_pairs, disjiUnion_eq_biUnion, - add_tsub_cancel_of_le] - · simp_all only [mem_antidiagonal, mem_filter, mem_pairs, disjiUnion_eq_biUnion, implies_true] + add_tsub_cancel_of_le, and_true] + · simp_all only [mem_antidiagonal, mem_filter, mem_pairs, disjiUnion_eq_biUnion, + implies_true, and_true] simp only [← hdisj, disj_equiv] private theorem disjoint_filter_pairs_lt_filter_pairs_eq (k : ℕ) : diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean index c2528bfbaa470..53eaf0060c3c2 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean @@ -339,7 +339,7 @@ theorem degree_cyclotomic (n : ℕ) (R : Type*) [Ring R] [Nontrivial R] : rw [← map_cyclotomic_int] rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom R) _] · cases' n with k - · simp only [cyclotomic, degree_one, dif_pos, Nat.totient_zero, WithTop.coe_zero] + · simp only [cyclotomic, degree_one, dif_pos, Nat.totient_zero, CharP.cast_eq_zero] rw [← degree_cyclotomic' (Complex.isPrimitiveRoot_exp k.succ (Nat.succ_ne_zero k))] exact (int_cyclotomic_spec k.succ).2.1 simp only [(int_cyclotomic_spec n).right.right, eq_intCast, Monic.leadingCoeff, Int.cast_one, diff --git a/Mathlib/RingTheory/WittVector/IsPoly.lean b/Mathlib/RingTheory/WittVector/IsPoly.lean index 0d70990e0a39a..b106c5583e7ac 100644 --- a/Mathlib/RingTheory/WittVector/IsPoly.lean +++ b/Mathlib/RingTheory/WittVector/IsPoly.lean @@ -328,8 +328,8 @@ theorem bind₁_onePoly_wittPolynomial [hp : Fact p.Prime] (n : ℕ) : AlgHom.map_pow, bind₁_X_right, AlgHom.map_mul] · rw [Finset.mem_range] -- porting note: was `decide` - simp only [add_pos_iff, or_true, not_true, pow_zero, map_one, ge_iff_le, nonpos_iff_eq_zero, - tsub_zero, one_mul, gt_iff_lt, IsEmpty.forall_iff] + intro h + simp only [add_pos_iff, zero_lt_one, or_true, not_true_eq_false] at h #align witt_vector.bind₁_one_poly_witt_polynomial WittVector.bind₁_onePoly_wittPolynomial /-- The function that is constantly one on Witt vectors is a polynomial function. -/ diff --git a/Mathlib/RingTheory/WittVector/MulCoeff.lean b/Mathlib/RingTheory/WittVector/MulCoeff.lean index ab6e5b6171a79..48f1d191b3a68 100644 --- a/Mathlib/RingTheory/WittVector/MulCoeff.lean +++ b/Mathlib/RingTheory/WittVector/MulCoeff.lean @@ -243,7 +243,8 @@ theorem peval_polyOfInterest' (n : ℕ) (x y : 𝕎 k) : x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) := by rw [peval_polyOfInterest] have : (p : k) = 0 := CharP.cast_eq_zero k p - simp only [this, Nat.cast_pow, ne_eq, add_eq_zero, and_false, zero_pow', zero_mul, add_zero] + simp only [this, Nat.cast_pow, ne_eq, add_eq_zero, and_false, zero_pow', zero_mul, add_zero, + not_false_eq_true] have sum_zero_pow_mul_pow_p : ∀ y : 𝕎 k, ∑ x : ℕ in range (n + 1 + 1), (0 : k) ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1) := by intro y diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index acf217ffe7bdc..bda7d41c768df 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -1883,13 +1883,13 @@ def toPartENat : Cardinal →+ PartENat where rw [← Nat.cast_add, toNat_cast, Nat.cast_add] · simp_rw [if_neg hy, PartENat.add_top] contrapose! hy - simp only [ne_eq, ite_eq_right_iff, - PartENat.natCast_ne_top, not_forall, exists_prop, and_true] at hy + simp only [ne_eq, ite_eq_right_iff, PartENat.natCast_ne_top, not_forall, exists_prop, + and_true, not_false_eq_true] at hy exact le_add_self.trans_lt hy · simp_rw [if_neg hx, PartENat.top_add] contrapose! hx - simp only [ne_eq, ite_eq_right_iff, - PartENat.natCast_ne_top, not_forall, exists_prop, and_true] at hx + simp only [ne_eq, ite_eq_right_iff, PartENat.natCast_ne_top, not_forall, exists_prop, + and_true, not_false_eq_true] at hx exact le_self_add.trans_lt hx #align cardinal.to_part_enat Cardinal.toPartENat diff --git a/Mathlib/SetTheory/Cardinal/Finite.lean b/Mathlib/SetTheory/Cardinal/Finite.lean index af658391b6c64..4ae92568aecc7 100644 --- a/Mathlib/SetTheory/Cardinal/Finite.lean +++ b/Mathlib/SetTheory/Cardinal/Finite.lean @@ -69,7 +69,7 @@ an equivalence between `α` and `Fin (Nat.card α)`. See also `Finite.equivFin`. def equivFinOfCardPos {α : Type*} (h : Nat.card α ≠ 0) : α ≃ Fin (Nat.card α) := by cases fintypeOrInfinite α · simpa only [card_eq_fintype_card] using Fintype.equivFin α - · simp only [card_eq_zero_of_infinite, ne_eq] at h + · simp only [card_eq_zero_of_infinite, ne_eq, not_true_eq_false] at h #align nat.equiv_fin_of_card_pos Nat.equivFinOfCardPos theorem card_of_subsingleton (a : α) [Subsingleton α] : Nat.card α = 1 := by diff --git a/Mathlib/SetTheory/Lists.lean b/Mathlib/SetTheory/Lists.lean index 9306d7ecadcd2..3b811c7d62078 100644 --- a/Mathlib/SetTheory/Lists.lean +++ b/Mathlib/SetTheory/Lists.lean @@ -369,7 +369,7 @@ def Equiv.decidableMeas : theorem sizeof_pos {b} (l : Lists' α b) : 0 < SizeOf.sizeOf l := by cases l <;> simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec, - true_or, add_pos_iff] + true_or, add_pos_iff, zero_lt_one] #align lists.sizeof_pos Lists.sizeof_pos theorem lt_sizeof_cons' {b} (a : Lists' α b) (l) : diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean index 70e2b88d5aeaa..f0f5617372a3d 100644 --- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean +++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean @@ -1003,7 +1003,8 @@ theorem le_of_dvd : ∀ {a b : Ordinal}, b ≠ 0 → a ∣ b → a ≤ b -- Porting note: `Ne` is required. simpa only [mul_one] using mul_le_mul_left' - (one_le_iff_ne_zero.2 fun h : b = 0 => by simp only [h, mul_zero, Ne] at b0) a + (one_le_iff_ne_zero.2 fun h : b = 0 => by + simp only [h, mul_zero, Ne, not_true_eq_false] at b0) a #align ordinal.le_of_dvd Ordinal.le_of_dvd theorem dvd_antisymm {a b : Ordinal} (h₁ : a ∣ b) (h₂ : b ∣ a) : a = b := diff --git a/Mathlib/SetTheory/Ordinal/CantorNormalForm.lean b/Mathlib/SetTheory/Ordinal/CantorNormalForm.lean index 0ce02e0b9ead4..bed9105c56c5b 100644 --- a/Mathlib/SetTheory/Ordinal/CantorNormalForm.lean +++ b/Mathlib/SetTheory/Ordinal/CantorNormalForm.lean @@ -162,11 +162,11 @@ set_option linter.uppercaseLean3 false in /-- The exponents of the Cantor normal form are decreasing. -/ theorem CNF_sorted (b o : Ordinal) : ((CNF b o).map Prod.fst).Sorted (· > ·) := by refine' CNFRec b _ (fun o ho IH ↦ _) o - · simp only [CNF_zero] + · simp only [gt_iff_lt, CNF_zero, map_nil, sorted_nil] · cases' le_or_lt b 1 with hb hb - · simp only [CNF_of_le_one hb ho, map] + · simp only [CNF_of_le_one hb ho, gt_iff_lt, map_cons, map, sorted_singleton] · cases' lt_or_le o b with hob hbo - · simp only [CNF_of_lt ho hob, map] + · simp only [CNF_of_lt ho hob, gt_iff_lt, map_cons, map, sorted_singleton] · rw [CNF_ne_zero ho, map_cons, sorted_cons] refine' ⟨fun a H ↦ _, IH⟩ rw [mem_map] at H diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean index 0ce5aceecc77e..a1600f206cc20 100644 --- a/Mathlib/SetTheory/Ordinal/Notation.lean +++ b/Mathlib/SetTheory/Ordinal/Notation.lean @@ -189,7 +189,8 @@ theorem eq_of_cmp_eq : ∀ {o₁ o₂}, cmp o₁ o₂ = Ordering.eq → o₁ = o #align onote.eq_of_cmp_eq ONote.eq_of_cmp_eq protected theorem zero_lt_one : (0 : ONote) < 1 := by - simp only [lt_def, repr, repr_one, opow_zero, one_mul, add_zero, nat_cast_pos] + simp only [lt_def, repr, opow_zero, Nat.succPNat_coe, Nat.cast_one, mul_one, add_zero, + zero_lt_one] #align onote.zero_lt_one ONote.zero_lt_one /-- `NFBelow o b` says that `o` is a normal form ordinal notation @@ -830,9 +831,10 @@ instance nf_opow (o₁ o₂) [NF o₁] [NF o₂] : NF (o₁ ^ o₂) := by haveI := (nf_repr_split' e₂).1 cases' a with a0 n a' · cases' m with m - · by_cases o₂ = 0 <;> simp [(· ^ ·), Pow.pow, pow, opow, opowAux2, *] + · by_cases o₂ = 0 <;> simp only [(· ^ ·), Pow.pow, pow, opow, opowAux2, *] <;> decide · by_cases m = 0 · simp only [(· ^ ·), Pow.pow, pow, opow, opowAux2, *, zero_def] + decide · simp only [(· ^ ·), Pow.pow, pow, opow, opowAux2, mulNat_eq_mul, ofNat, *] infer_instance · simp [(· ^ ·),Pow.pow,pow, opow, opowAux2, e₁, e₂, split_eq_scale_split' e₂] @@ -1098,6 +1100,7 @@ theorem fundamentalSequence_has_prop (o) : FundamentalSequenceProp o (fundamenta eq_self_iff_true, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero, Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe, succ_zero, true_and_iff, _root_.zero_add, zero_def] + · decide · exact ⟨rfl, inferInstance⟩ · have := opow_pos (repr a') omega_pos refine' diff --git a/Mathlib/Tactic/ComputeDegree.lean b/Mathlib/Tactic/ComputeDegree.lean index d523afc63969e..5ab9de971c149 100644 --- a/Mathlib/Tactic/ComputeDegree.lean +++ b/Mathlib/Tactic/ComputeDegree.lean @@ -448,12 +448,14 @@ elab_rules : tactic | `(tactic| compute_degree $[!%$bang]?) => focus <| withMain -- simplify the left-hand sides, since this is where the degree computations leave -- expressions such as `max (0 * 1) (max (1 + 0 + 3 * 4) (7 * 0))` evalTactic - (← `(tactic| try any_goals conv_lhs => (simp only [Nat.cast_withBot]; norm_num))) + (← `(tactic| try any_goals conv_lhs => + (simp (config := {decide := true}) only [Nat.cast_withBot]; norm_num))) if bang.isSome then let mut false_goals : Array MVarId := #[] let mut new_goals : Array MVarId := #[] for g in ← getGoals do - let gs' ← run g do evalTactic (← `(tactic| try (any_goals norm_num <;> try assumption))) + let gs' ← run g do evalTactic (← + `(tactic| try (any_goals norm_num <;> norm_cast <;> try assumption))) new_goals := new_goals ++ gs'.toArray if ← gs'.anyM fun g' => g'.withContext do return (← g'.getType'').isConstOf ``False then false_goals := false_goals.push g diff --git a/Mathlib/Tactic/NormNum/LegendreSymbol.lean b/Mathlib/Tactic/NormNum/LegendreSymbol.lean index db5269773b3c2..8417a02e44a34 100644 --- a/Mathlib/Tactic/NormNum/LegendreSymbol.lean +++ b/Mathlib/Tactic/NormNum/LegendreSymbol.lean @@ -124,6 +124,7 @@ theorem jacobiSymNat.odd_even (a b c : ℕ) (r : ℤ) (ha : a % 2 = 1) (hb : b % jacobiSymNat a b = r := by have ha' : legendreSym 2 a = 1 := by simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha] + decide rcases eq_or_ne c 0 with (rfl | hc') · rw [← hr, Nat.eq_zero_of_dvd_of_div_eq_zero (Nat.dvd_of_mod_eq_zero hb) hc] · haveI : NeZero c := ⟨hc'⟩ diff --git a/Mathlib/Topology/Category/Profinite/Nobeling.lean b/Mathlib/Topology/Category/Profinite/Nobeling.lean index 2a1e3bd757692..812d2351b1a05 100644 --- a/Mathlib/Topology/Category/Profinite/Nobeling.lean +++ b/Mathlib/Topology/Category/Profinite/Nobeling.lean @@ -386,7 +386,7 @@ theorem eval_eq (l : Products I) (x : C) : push_neg at h convert h with i dsimp [LocallyConstant.evalMonoidHom, e] - simp only [ite_eq_right_iff] + simp only [ite_eq_right_iff, one_ne_zero] theorem evalFacProp {l : Products I} (J : I → Prop) (h : ∀ a, a ∈ l.val → J a) [∀ j, Decidable (J j)] : diff --git a/Mathlib/Topology/EMetricSpace/Paracompact.lean b/Mathlib/Topology/EMetricSpace/Paracompact.lean index 1dfa424744a91..b4494c9f093de 100644 --- a/Mathlib/Topology/EMetricSpace/Paracompact.lean +++ b/Mathlib/Topology/EMetricSpace/Paracompact.lean @@ -45,7 +45,7 @@ instance (priority := 100) instParacompactSpace [PseudoEMetricSpace α] : Paraco have hpow_le : ∀ {m n : ℕ}, m ≤ n → (2⁻¹ : ℝ≥0∞) ^ n ≤ 2⁻¹ ^ m := @fun m n h => pow_le_pow_of_le_one' (ENNReal.inv_le_one.2 ENNReal.one_lt_two.le) h have h2pow : ∀ n : ℕ, 2 * (2⁻¹ : ℝ≥0∞) ^ (n + 1) = 2⁻¹ ^ n := fun n => by - simp [pow_succ, ← mul_assoc, ENNReal.mul_inv_cancel] + simp [pow_succ, ← mul_assoc, ENNReal.mul_inv_cancel two_ne_zero two_ne_top] -- Consider an open covering `S : Set (Set α)` refine' ⟨fun ι s ho hcov => _⟩ simp only [iUnion_eq_univ_iff] at hcov diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean index 688949454900e..ec1da50389cc0 100644 --- a/Mathlib/Topology/Instances/ENNReal.lean +++ b/Mathlib/Topology/Instances/ENNReal.lean @@ -306,7 +306,7 @@ protected theorem tendsto_atTop_zero [Nonempty β] [SemilatticeSup β] {f : β theorem tendsto_sub : ∀ {a b : ℝ≥0∞}, (a ≠ ∞ ∨ b ≠ ∞) → Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 - p.2) (𝓝 (a, b)) (𝓝 (a - b)) - | ⊤, ⊤, h => by simp only at h + | ⊤, ⊤, h => by simp only [ne_eq, not_true_eq_false, or_self] at h | ⊤, (b : ℝ≥0), _ => by rw [top_sub_coe, tendsto_nhds_top_iff_nnreal] refine fun x => ((lt_mem_nhds <| @coe_lt_top (b + 1 + x)).prod_nhds @@ -343,11 +343,11 @@ protected theorem tendsto_mul (ha : a ≠ 0 ∨ b ≠ ⊤) (hb : b ≠ 0 ∨ a refine' this.mono fun c hc => _ exact (ENNReal.div_mul_cancel hε.ne' coe_ne_top).symm.trans_lt (mul_lt_mul hc.1 hc.2) induction a using recTopCoe with - | top => simp only [ne_eq, or_false] at hb; simp [ht b hb, top_mul hb] + | top => simp only [ne_eq, or_false, not_true_eq_false] at hb; simp [ht b hb, top_mul hb] | coe a => induction b using recTopCoe with | top => - simp only [ne_eq, or_false] at ha + simp only [ne_eq, or_false, not_true_eq_false] at ha simpa [(· ∘ ·), mul_comm, mul_top ha] using (ht a ha).comp (continuous_swap.tendsto (some a, ⊤)) | coe b => @@ -1456,7 +1456,7 @@ theorem continuous_of_le_add_edist {f : α → ℝ≥0∞} (C : ℝ≥0∞) (hC #align continuous_of_le_add_edist continuous_of_le_add_edist theorem continuous_edist : Continuous fun p : α × α => edist p.1 p.2 := by - apply continuous_of_le_add_edist 2 (by norm_num) + apply continuous_of_le_add_edist 2 (by decide) rintro ⟨x, y⟩ ⟨x', y'⟩ calc edist x y ≤ edist x x' + edist x' y' + edist y' y := edist_triangle4 _ _ _ _ diff --git a/Mathlib/Topology/Sequences.lean b/Mathlib/Topology/Sequences.lean index 264d2361babff..c91386ce66cea 100644 --- a/Mathlib/Topology/Sequences.lean +++ b/Mathlib/Topology/Sequences.lean @@ -163,7 +163,8 @@ theorem FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto · exact subset_seqClosure hx · obtain ⟨u, hux, hus⟩ : ∃ u : ℕ → X, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s · simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop, - ← mem_closure_iff_frequently, hcx, imp_false, not_forall, not_not] using h (· ∉ s) x + ← mem_closure_iff_frequently, hcx, imp_false, not_forall, not_not, not_false_eq_true, + not_true_eq_false] using h (· ∉ s) x rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩ exact ⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩ #align frechet_urysohn_space.of_seq_tendsto_imp_tendsto FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto diff --git a/Mathlib/Topology/Sheaves/Presheaf.lean b/Mathlib/Topology/Sheaves/Presheaf.lean index 37d1f9c6b500f..ede11350b74cb 100644 --- a/Mathlib/Topology/Sheaves/Presheaf.lean +++ b/Mathlib/Topology/Sheaves/Presheaf.lean @@ -335,7 +335,7 @@ def pullbackObjObjOfImageOpen {X Y : TopCat.{v}} (f : X ⟶ Y) (ℱ : Y.Presheaf · refine' (homOfLE _).op apply (Set.image_subset f s.pt.hom.unop.le).trans exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop) - · simp + · simp [autoParam] -- porting note : add `fac`, `uniq` manually fac := fun _ _ => by ext; simp uniq := fun _ _ _ => by ext; simp } diff --git a/test/RewriteSearch/Basic.lean b/test/RewriteSearch/Basic.lean index 7ca2eacd390d4..d06ecc1d270af 100644 --- a/test/RewriteSearch/Basic.lean +++ b/test/RewriteSearch/Basic.lean @@ -50,6 +50,6 @@ def makeSingleton : Nat → List Nat #guard_msgs in example (n : Nat) : makeSingleton n = [0] := by induction' n with n' ih - · simp + · simp only [makeSingleton] · -- At one point, this failed with: unknown free variable '_uniq.62770' rw_search diff --git a/test/linear_combination.lean b/test/linear_combination.lean index 55e5adab860ed..05d7b32149fd0 100644 --- a/test/linear_combination.lean +++ b/test/linear_combination.lean @@ -140,7 +140,7 @@ example (a b : ℝ) (ha : 2 * a = 4) (hab : 2 * b = a - b) : b = 2 / 3 := by example (x y : ℤ) (h1 : x = -3) (_h2 : y = 10) : 2 * x = -6 := by linear_combination (norm := skip) 2 * h1 - simp + simp (config := {decide := true}) /-! ### Cases without any arguments provided -/ diff --git a/test/matrix.lean b/test/matrix.lean index e13ff85cceab2..deac900999aea 100644 --- a/test/matrix.lean +++ b/test/matrix.lean @@ -139,9 +139,10 @@ example {α : Type _} [CommRing α] {a b c d : α} : Matrix.det !![a, b; c, d] = a * d - b * c := by simp? [Matrix.det_succ_row_zero, Fin.sum_univ_succ] says simp only [det_succ_row_zero, Nat.odd_iff_not_even, of_apply, cons_val', empty_val', - cons_val_fin_one, cons_val_zero, det_unique, Fin.default_eq_zero, submatrix_apply, Fin.succ_zero_eq_one, ne_eq, - cons_val_one, head_fin_const, Fin.sum_univ_succ, Fin.val_zero, pow_zero, one_mul, Fin.zero_succAbove, head_cons, - Finset.univ_unique, Fin.val_succ, Fin.coe_fin_one, zero_add, pow_one, cons_val_succ, neg_mul, + cons_val_fin_one, cons_val_zero, det_unique, Fin.default_eq_zero, submatrix_apply, + Fin.succ_zero_eq_one, ne_eq, cons_val_one, head_fin_const, Fin.sum_univ_succ, Fin.val_zero, + pow_zero, one_mul, not_true_eq_false, Fin.zero_succAbove, head_cons, Finset.univ_unique, + Fin.val_succ, Fin.coe_fin_one, zero_add, pow_one, cons_val_succ, neg_mul, Fin.succ_succAbove_zero, Finset.sum_const, Finset.card_singleton, smul_neg, one_smul] ring @@ -150,10 +151,10 @@ example {α : Type _} [CommRing α] {a b c d e f g h i : α} : a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g := by simp? [Matrix.det_succ_row_zero, Fin.sum_univ_succ] says simp only [det_succ_row_zero, Nat.odd_iff_not_even, of_apply, cons_val', empty_val', - cons_val_fin_one, cons_val_zero, submatrix_apply, Fin.succ_zero_eq_one, cons_val_one, - head_cons, submatrix_submatrix, det_unique, Fin.default_eq_zero, Function.comp_apply, - Fin.succ_one_eq_two, ne_eq, cons_val_two, tail_cons, head_fin_const, Fin.sum_univ_succ, - Fin.val_zero, pow_zero, one_mul, Fin.zero_succAbove, Finset.univ_unique, Fin.val_succ, + cons_val_fin_one, cons_val_zero, submatrix_apply, Fin.succ_zero_eq_one, cons_val_one, head_cons, + submatrix_submatrix, det_unique, Fin.default_eq_zero, Function.comp_apply, Fin.succ_one_eq_two, + ne_eq, cons_val_two, tail_cons, head_fin_const, Fin.sum_univ_succ, Fin.val_zero, pow_zero, + one_mul, not_true_eq_false, Fin.zero_succAbove, Finset.univ_unique, Fin.val_succ, Fin.coe_fin_one, zero_add, pow_one, neg_mul, Fin.succ_succAbove_zero, Finset.sum_neg_distrib, Finset.sum_singleton, cons_val_succ, Fin.succ_succAbove_one, even_add_self, Even.neg_pow, one_pow, Finset.sum_const, Finset.card_singleton, one_smul] diff --git a/test/norm_num_ext.lean b/test/norm_num_ext.lean index e1cccc8619ce4..d06b0a36a5e4d 100644 --- a/test/norm_num_ext.lean +++ b/test/norm_num_ext.lean @@ -335,18 +335,24 @@ variable {α : Type _} [CommRing α] open BigOperators -- Lists: +-- `by decide` closes the three goals below. +/- example : ([1, 2, 1, 3]).sum = 7 := by norm_num only --- example : (([1, 2, 1, 3] : List ℚ).map (fun i => i^2)).sum = 15 := by norm_num [-List.map] --TODO example : (List.range 10).sum = 45 := by norm_num only example : (List.finRange 10).sum = 45 := by norm_num only +-/ +-- example : (([1, 2, 1, 3] : List ℚ).map (fun i => i^2)).sum = 15 := by norm_num [-List.map] --TODO -- Multisets: +-- `by decide` closes the three goals below. +/- example : (1 ::ₘ 2 ::ₘ 1 ::ₘ 3 ::ₘ {}).sum = 7 := by norm_num only example : ((1 ::ₘ 2 ::ₘ 1 ::ₘ 3 ::ₘ {}).map (fun i => i^2)).sum = 15 := by norm_num only --- example : (({1, 2, 1, 3} : Multiset ℚ).map (fun i => i^2)).sum = 15 := by -- TODO --- norm_num [-Multiset.map_cons] example : (Multiset.range 10).sum = 45 := by norm_num only example : (↑[1, 2, 1, 3] : Multiset ℕ).sum = 7 := by norm_num only +-/ +-- example : (({1, 2, 1, 3} : Multiset ℚ).map (fun i => i^2)).sum = 15 := by -- TODO +-- norm_num [-Multiset.map_cons] -- Finsets: example : Finset.prod (Finset.cons 2 ∅ (Finset.not_mem_empty _)) (λ x => x) = 2 := by norm_num1