chore: adapt to new simp default (decide := false) (#7834)

Mostly smooth so far, but I think `norm_num` is less powerful for modulo and divisibility operations on integers. `(config := {decide := true})`  was added only as a last resort.



Co-authored-by: Mauricio Collares <[email protected]>
Co-authored-by: Scott Morrison <[email protected]>

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
 

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

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

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

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

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

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₂
 

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

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
 

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

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** -/

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 _)

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

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

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 -/

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

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 :

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

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

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

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