chore: update lean4/std4 (#1096)

Mathlib/Algebra/Group/Basic.lean

@@ -719,7 +719,6 @@ theorem div_div_div_cancel_left (a b c : G) : c / a / (c / b) = b / a := by
 theorem div_eq_div_iff_mul_eq_mul : a / b = c / d ↔ a * d = c * b := by
   rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul']
   simp only [mul_comm, eq_comm]
-  rfl
 
 @[to_additive]
 theorem div_eq_div_iff_div_eq_div : a / b = c / d ↔ a / c = b / d := by

Mathlib/Algebra/Group/Opposite.lean

@@ -178,7 +178,7 @@ theorem op_div [DivInvMonoid α] (x y : α) : op (x / y) = (op y)⁻¹ * op x :=
 
 @[simp, to_additive]
 theorem semiconjBy_op [Mul α] {a x y : α} : SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y :=
-  by simp only [SemiconjBy, ← op_mul, op_inj, eq_comm] ; rfl
+  by simp only [SemiconjBy, ← op_mul, op_inj, eq_comm]
 #align mul_opposite.semiconj_by_op MulOpposite.semiconjBy_op
 
 @[simp, to_additive]

Mathlib/Algebra/GroupPower/Order.lean

@@ -601,7 +601,6 @@ theorem abs_le_of_sq_le_sq' (h : x ^ 2 ≤ y ^ 2) (hy : 0 ≤ y) : -y ≤ x ∧
 
 theorem sq_eq_sq_iff_abs_eq_abs (x y : R) : x ^ 2 = y ^ 2 ↔ |x| = |y| := by
   simp only [le_antisymm_iff, sq_le_sq]
-  apply Iff.refl
 #align sq_eq_sq_iff_abs_eq_abs sq_eq_sq_iff_abs_eq_abs
 
 @[simp]

Mathlib/Algebra/GroupPower/Ring.lean

@@ -275,7 +275,7 @@ theorem eq_or_eq_neg_of_sq_eq_sq (a b : R) : a ^ 2 = b ^ 2 → a = b ∨ a = -b
 namespace Units
 
 protected theorem sq_eq_sq_iff_eq_or_eq_neg {a b : Rˣ} : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b := by
-  simp_rw [ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg, iff_self]
+  simp_rw [ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]
 
 protected theorem eq_or_eq_neg_of_sq_eq_sq (a b : Rˣ) (h : a ^ 2 = b ^ 2) : a = b ∨ a = -b :=
   Units.sq_eq_sq_iff_eq_or_eq_neg.1 h

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

@@ -232,7 +232,7 @@ theorem exists0 {p : G₀ˣ → Prop} : (∃ g : G₀ˣ, p g) ↔ ∃ (g : G₀)
 figure out `p` when using `Units.exists0` from right to left. -/
 theorem exists0' {p : ∀ g : G₀, g ≠ 0 → Prop} :
     (∃ (g : G₀)(hg : g ≠ 0), p g hg) ↔ ∃ g : G₀ˣ, p g g.ne_zero :=
-  Iff.trans (by simp_rw [val_mk0]; rfl) exists0.symm
+  Iff.trans (by simp_rw [val_mk0]) exists0.symm
   -- porting note: had to add the `rfl`
 #align units.exists0' Units.exists0'
 

Mathlib/Algebra/Order/Invertible.lean

@@ -24,7 +24,7 @@ theorem invOf_pos [Invertible a] : 0 < ⅟ a ↔ 0 < a :=
 #align inv_of_pos invOf_pos
 
 @[simp]
-theorem invOf_nonpos [Invertible a] : ⅟ a ≤ 0 ↔ a ≤ 0 := by simp only [← not_lt, invOf_pos]; rfl
+theorem invOf_nonpos [Invertible a] : ⅟ a ≤ 0 ↔ a ≤ 0 := by simp only [← not_lt, invOf_pos]
 #align inv_of_nonpos invOf_nonpos
 
 @[simp]
@@ -34,7 +34,7 @@ theorem invOf_nonneg [Invertible a] : 0 ≤ ⅟ a ↔ 0 ≤ a :=
 #align inv_of_nonneg invOf_nonneg
 
 @[simp]
-theorem invOf_lt_zero [Invertible a] : ⅟ a < 0 ↔ a < 0 := by simp only [← not_le, invOf_nonneg]; rfl
+theorem invOf_lt_zero [Invertible a] : ⅟ a < 0 ↔ a < 0 := by simp only [← not_le, invOf_nonneg]
 #align inv_of_lt_zero invOf_lt_zero
 
 @[simp]

Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

@@ -189,7 +189,6 @@ theorem le_iff_exists_mul : a ≤ b ↔ ∃ c, b = a * c :=
 @[to_additive]
 theorem le_iff_exists_mul' : a ≤ b ↔ ∃ c, b = c * a := by
   simp only [mul_comm _ a, le_iff_exists_mul]
-  rfl
 #align le_iff_exists_mul' le_iff_exists_mul'
 
 @[simp, to_additive zero_le]
@@ -225,7 +224,6 @@ theorem eq_one_or_one_lt : a = 1 ∨ 1 < a :=
 @[simp, to_additive add_pos_iff]
 theorem one_lt_mul_iff : 1 < a * b ↔ 1 < a ∨ 1 < b := by
   simp only [one_lt_iff_ne_one, Ne.def, mul_eq_one_iff, not_and_or]
-  rfl -- Porting note: Should this be needed? It wasn't needed in lean3
 #align one_lt_mul_iff one_lt_mul_iff
 
 @[to_additive]

Mathlib/Algebra/Order/Monoid/WithTop.lean

@@ -131,7 +131,6 @@ theorem add_ne_top : a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤ :=
 
 theorem add_lt_top [PartialOrder α] {a b : WithTop α} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ := by
   simp_rw [lt_top_iff_ne_top, add_ne_top]
-  rfl
 #align with_top.add_lt_top WithTop.add_lt_top
 
 theorem add_eq_coe :

Mathlib/Algebra/Order/Sub/Canonical.lean

@@ -48,7 +48,7 @@ theorem tsub_le_tsub_iff_right (h : c ≤ b) : a - c ≤ b - c ↔ a ≤ b := by
 #align tsub_le_tsub_iff_right tsub_le_tsub_iff_right
 
 theorem tsub_left_inj (h1 : c ≤ a) (h2 : c ≤ b) : a - c = b - c ↔ a = b := by
-  simp_rw [le_antisymm_iff, tsub_le_tsub_iff_right h1, tsub_le_tsub_iff_right h2]; rfl
+  simp_rw [le_antisymm_iff, tsub_le_tsub_iff_right h1, tsub_le_tsub_iff_right h2]
 #align tsub_left_inj tsub_left_inj
 
 theorem tsub_inj_left (h₁ : a ≤ b) (h₂ : a ≤ c) : b - a = c - a → b = c :=
@@ -376,7 +376,7 @@ protected theorem tsub_le_tsub_iff_left (ha : AddLECancellable a) (hc : AddLECan
 protected theorem tsub_right_inj (ha : AddLECancellable a) (hb : AddLECancellable b)
     (hc : AddLECancellable c) (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c := by
   simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca,
-    and_comm]; rfl
+    and_comm]
 #align add_le_cancellable.tsub_right_inj AddLECancellable.tsub_right_inj
 
 end AddLECancellable

Mathlib/CategoryTheory/Iso.lean

@@ -511,28 +511,24 @@ Presumably we could write `X ↪ Y` and `X ↠ Y`.
 theorem cancel_iso_hom_left {X Y Z : C} (f : X ≅ Y) (g g' : Y ⟶ Z) :
     f.hom ≫ g = f.hom ≫ g' ↔ g = g' := by
   simp only [cancel_epi]
-  rfl
 #align category_theory.iso.cancel_iso_hom_left CategoryTheory.Iso.cancel_iso_hom_left
 
 @[simp]
 theorem cancel_iso_inv_left {X Y Z : C} (f : Y ≅ X) (g g' : Y ⟶ Z) :
     f.inv ≫ g = f.inv ≫ g' ↔ g = g' := by
   simp only [cancel_epi]
-  rfl
 #align category_theory.iso.cancel_iso_inv_left CategoryTheory.Iso.cancel_iso_inv_left
 
 @[simp]
 theorem cancel_iso_hom_right {X Y Z : C} (f f' : X ⟶ Y) (g : Y ≅ Z) :
     f ≫ g.hom = f' ≫ g.hom ↔ f = f' := by
   simp only [cancel_mono]
-  rfl
 #align category_theory.iso.cancel_iso_hom_right CategoryTheory.Iso.cancel_iso_hom_right
 
 @[simp]
 theorem cancel_iso_inv_right {X Y Z : C} (f f' : X ⟶ Y) (g : Z ≅ Y) :
     f ≫ g.inv = f' ≫ g.inv ↔ f = f' := by
   simp only [cancel_mono]
-  rfl
 #align category_theory.iso.cancel_iso_inv_right CategoryTheory.Iso.cancel_iso_inv_right
 
 /-
@@ -545,13 +541,13 @@ but then stop.
 @[simp]
 theorem cancel_iso_hom_right_assoc {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
     (g' : X' ⟶ Y) (h : Y ≅ Z) : f ≫ g ≫ h.hom = f' ≫ g' ≫ h.hom ↔ f ≫ g = f' ≫ g' := by
-  simp only [← Category.assoc, cancel_mono]; rfl
+  simp only [← Category.assoc, cancel_mono]
 #align category_theory.iso.cancel_iso_hom_right_assoc CategoryTheory.Iso.cancel_iso_hom_right_assoc
 
 @[simp]
 theorem cancel_iso_inv_right_assoc {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
     (g' : X' ⟶ Y) (h : Z ≅ Y) : f ≫ g ≫ h.inv = f' ≫ g' ≫ h.inv ↔ f ≫ g = f' ≫ g' := by
-  simp only [← Category.assoc, cancel_mono]; rfl
+  simp only [← Category.assoc, cancel_mono]
 #align category_theory.iso.cancel_iso_inv_right_assoc CategoryTheory.Iso.cancel_iso_inv_right_assoc
 
 end Iso

Mathlib/Data/List/Basic.lean

@@ -266,4 +266,3 @@ theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach
 theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} :
     b ∈ pmap f l H ↔ ∃ (a : _)(h : a ∈ l), f a (H a h) = b := by
   simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]
-  rfl

Mathlib/Data/List/Pairwise.lean

@@ -24,7 +24,6 @@ theorem pairwise_middle (s : Symmetric R) {a : α} {l₁ l₂ : List α} :
   show Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂) by
     rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]
     simp only [mem_append, or_comm]
-    rfl
 
 theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by
   simp [Pairwise.nil]

Mathlib/Data/List/Range.lean

@@ -46,7 +46,6 @@ theorem range_eq_range' (n : ℕ) : range n = range' 0 n :=
 @[simp]
 theorem mem_range {m n : ℕ} : m ∈ range n ↔ m < n := by
   simp only [range_eq_range', mem_range', Nat.zero_le, true_and, Nat.zero_add]
-  rfl
 
 theorem chain_succ_range' : ∀ s n : ℕ, Chain (fun a b ↦ b = succ a) s (range' (s + 1) n)
   | _, 0 => Chain.nil

Mathlib/Data/Nat/Basic.lean

@@ -227,7 +227,7 @@ theorem lt_add_one_iff {a b : ℕ} : a < b + 1 ↔ a ≤ b :=
 #align nat.lt_add_one_iff Nat.lt_add_one_iff
 
 -- A flipped version of `lt_add_one_iff`.
-theorem lt_one_add_iff {a b : ℕ} : a < 1 + b ↔ a ≤ b := by simp only [add_comm, lt_succ_iff]; rfl
+theorem lt_one_add_iff {a b : ℕ} : a < 1 + b ↔ a ≤ b := by simp only [add_comm, lt_succ_iff]
 #align nat.lt_one_add_iff Nat.lt_one_add_iff
 
 -- This is true reflexively, by the definition of `≤` on ℕ,
@@ -236,7 +236,7 @@ theorem add_one_le_iff {a b : ℕ} : a + 1 ≤ b ↔ a < b :=
   Iff.refl _
 #align nat.add_one_le_iff Nat.add_one_le_iff
 
-theorem one_add_le_iff {a b : ℕ} : 1 + a ≤ b ↔ a < b := by simp only [add_comm, add_one_le_iff]; rfl
+theorem one_add_le_iff {a b : ℕ} : 1 + a ≤ b ↔ a < b := by simp only [add_comm, add_one_le_iff]
 #align nat.one_add_le_iff Nat.one_add_le_iff
 
 theorem of_le_succ {n m : ℕ} (H : n ≤ m.succ) : n ≤ m ∨ n = m.succ :=
@@ -264,7 +264,7 @@ theorem two_lt_of_ne : ∀ {n}, n ≠ 0 → n ≠ 1 → n ≠ 2 → 2 < n
 #align nat.two_lt_of_ne Nat.two_lt_of_ne
 
 theorem forall_lt_succ {P : ℕ → Prop} {n : ℕ} : (∀ m < n + 1, P m) ↔ (∀ m < n, P m) ∧ P n := by
-  simp only [lt_succ_iff, Decidable.le_iff_eq_or_lt, forall_eq_or_imp, and_comm]; rfl
+  simp only [lt_succ_iff, Decidable.le_iff_eq_or_lt, forall_eq_or_imp, and_comm]
 #align nat.forall_lt_succ Nat.forall_lt_succ
 
 theorem exists_lt_succ {P : ℕ → Prop} {n : ℕ} : (∃ m < n + 1, P m) ↔ (∃ m < n, P m) ∨ P n := by
@@ -681,14 +681,7 @@ protected theorem mul_div_cancel_left' {a b : ℕ} (Hd : a ∣ b) : a * (b / a)
   rw [mul_comm, Nat.div_mul_cancel Hd]
 #align nat.mul_div_cancel_left' Nat.mul_div_cancel_left'
 
---TODO: Update `nat.mul_div_mul` in the core?
-/-- Alias of `nat.mul_div_mul` -/
-protected theorem mul_div_mul_left (a b : ℕ) {c : ℕ} (hc : 0 < c) : c * a / (c * b) = a / b :=
-  Nat.mul_div_mul a b hc
 #align nat.mul_div_mul_left Nat.mul_div_mul_left
-
-protected theorem mul_div_mul_right (a b : ℕ) {c : ℕ} (hc : 0 < c) : a * c / (b * c) = a / b := by
-  rw [mul_comm, mul_comm b, a.mul_div_mul_left b hc]
 #align nat.mul_div_mul_right Nat.mul_div_mul_right
 
 theorem lt_div_mul_add {a b : ℕ} (hb : 0 < b) : a < a / b * b + b := by
@@ -848,17 +841,17 @@ theorem find_lt_iff (h : ∃ n : ℕ, p n) (n : ℕ) : Nat.find h < n ↔ ∃ m
 
 @[simp]
 theorem find_le_iff (h : ∃ n : ℕ, p n) (n : ℕ) : Nat.find h ≤ n ↔ ∃ m ≤ n, p m := by
-  simp only [exists_prop, ← lt_succ_iff, find_lt_iff]; rfl
+  simp only [exists_prop, ← lt_succ_iff, find_lt_iff]
 #align nat.find_le_iff Nat.find_le_iff
 
 @[simp]
 theorem le_find_iff (h : ∃ n : ℕ, p n) (n : ℕ) : n ≤ Nat.find h ↔ ∀ m < n, ¬p m := by
-  simp_rw [← not_lt, find_lt_iff, not_exists, not_and]; rfl
+  simp_rw [← not_lt, find_lt_iff, not_exists, not_and]
 #align nat.le_find_iff Nat.le_find_iff
 
 @[simp]
 theorem lt_find_iff (h : ∃ n : ℕ, p n) (n : ℕ) : n < Nat.find h ↔ ∀ m ≤ n, ¬p m := by
-  simp only [← succ_le_iff, le_find_iff, succ_le_succ_iff]; rfl
+  simp only [← succ_le_iff, le_find_iff, succ_le_succ_iff]
 #align nat.lt_find_iff Nat.lt_find_iff
 
 @[simp]

Mathlib/Data/Nat/Order/Basic.lean

@@ -91,8 +91,6 @@ theorem one_lt_iff_ne_zero_and_ne_one : ∀ {n : ℕ}, 1 < n ↔ n ≠ 0 ∧ n 
   | n + 2 => by simp
 #align nat.one_lt_iff_ne_zero_and_ne_one Nat.one_lt_iff_ne_zero_and_ne_one
 
-protected theorem mul_ne_zero (n0 : n ≠ 0) (m0 : m ≠ 0) : n * m ≠ 0
-  | nm => (eq_zero_of_mul_eq_zero nm).elim n0 m0
 #align nat.mul_ne_zero Nat.mul_ne_zero
 
 -- Porting note: already in Std
@@ -446,7 +444,7 @@ theorem div_mul_div_le_div (m n k : ℕ) : m / k * n / m ≤ n / k :=
         Nat.div_le_div_right (by rw [mul_comm] ; exact mul_div_le_mul_div_assoc _ _ _)
       _ = n / k := by
         { rw [Nat.div_div_eq_div_mul, mul_comm n, mul_comm k,
-            Nat.mul_div_mul _ _ (Nat.pos_of_ne_zero hm0)] }
+            Nat.mul_div_mul_left _ _ (Nat.pos_of_ne_zero hm0)] }
 
 
 #align nat.div_mul_div_le_div Nat.div_mul_div_le_div

Mathlib/Data/Set/Basic.lean

@@ -526,11 +526,11 @@ theorem inter_nonempty : (s ∩ t).Nonempty ↔ ∃ x, x ∈ s ∧ x ∈ t :=
 #align set.inter_nonempty Set.inter_nonempty
 
 theorem inter_nonempty_iff_exists_left : (s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t := by
-  simp_rw [inter_nonempty, exists_prop]; rfl
+  simp_rw [inter_nonempty]
 #align set.inter_nonempty_iff_exists_left Set.inter_nonempty_iff_exists_left
 
 theorem inter_nonempty_iff_exists_right : (s ∩ t).Nonempty ↔ ∃ x ∈ t, x ∈ s := by
-  simp_rw [inter_nonempty, exists_prop, and_comm]; rfl
+  simp_rw [inter_nonempty, exists_prop, and_comm]
 #align set.inter_nonempty_iff_exists_right Set.inter_nonempty_iff_exists_right
 
 theorem nonempty_iff_univ_nonempty : Nonempty α ↔ (univ : Set α).Nonempty :=
@@ -1162,7 +1162,6 @@ theorem insert_subset_insert_iff (ha : a ∉ s) : insert a s ⊆ insert a t ↔
 theorem ssubset_iff_insert {s t : Set α} : s ⊂ t ↔ ∃ (a : α) (_ : a ∉ s), insert a s ⊆ t := by
   simp only [insert_subset, exists_and_right, ssubset_def, not_subset]
   simp only [exists_prop, and_comm]
-  rfl
 #align set.ssubset_iff_insert Set.ssubset_iff_insert
 
 theorem ssubset_insert {s : Set α} {a : α} (h : a ∉ s) : s ⊂ insert a s :=
@@ -1406,7 +1405,7 @@ theorem mem_sep_iff : x ∈ { x ∈ s | p x } ↔ x ∈ s ∧ p x :=
 #align set.mem_sep_iff Set.mem_sep_iff
 
 theorem sep_ext_iff : { x ∈ s | p x } = { x ∈ s | q x } ↔ ∀ x ∈ s, p x ↔ q x := by
-  simp_rw [ext_iff, mem_sep_iff, and_congr_right_iff]; rfl
+  simp_rw [ext_iff, mem_sep_iff, and_congr_right_iff]
 #align set.sep_ext_iff Set.sep_ext_iff
 
 theorem sep_eq_of_subset (h : s ⊆ t) : { x ∈ t | x ∈ s } = s :=
@@ -1419,12 +1418,12 @@ theorem sep_subset (s : Set α) (p : α → Prop) : { x ∈ s | p x } ⊆ s := f
 
 @[simp]
 theorem sep_eq_self_iff_mem_true : { x ∈ s | p x } = s ↔ ∀ x ∈ s, p x := by
-  simp_rw [ext_iff, mem_sep_iff, and_iff_left_iff_imp]; rfl
+  simp_rw [ext_iff, mem_sep_iff, and_iff_left_iff_imp]
 #align set.sep_eq_self_iff_mem_true Set.sep_eq_self_iff_mem_true
 
 @[simp]
 theorem sep_eq_empty_iff_mem_false : { x ∈ s | p x } = ∅ ↔ ∀ x ∈ s, ¬p x := by
-  simp_rw [ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false_iff, not_and]; rfl
+  simp_rw [ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false_iff, not_and]
 #align set.sep_eq_empty_iff_mem_false Set.sep_eq_empty_iff_mem_false
 
 --Porting note: removed `simp` attribute because `simp` can prove it
@@ -2512,7 +2511,7 @@ theorem nontrivial_mono {α : Type _} {s t : Set α} (hst : s ⊆ t) (hs : Nontr
 
 @[simp]
 theorem not_subsingleton_iff : ¬s.Subsingleton ↔ s.Nontrivial := by
-  simp_rw [Set.Subsingleton, Set.Nontrivial, not_forall]; rfl
+  simp_rw [Set.Subsingleton, Set.Nontrivial, not_forall]
 #align set.not_subsingleton_iff Set.not_subsingleton_iff
 
 @[simp]

Mathlib/Data/Set/Function.lean

@@ -1156,7 +1156,7 @@ theorem preimage_invFun_of_mem [n : Nonempty α] {f : α → β} (hf : Injective
   ext x
   rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
   · simp only [mem_preimage, mem_union, mem_compl_iff, mem_range_self, not_true, or_false,
-      leftInverse_invFun hf _, hf.mem_set_image]; rfl
+      leftInverse_invFun hf _, hf.mem_set_image]
   · simp only [mem_preimage, invFun_neg hx, h, hx, mem_union, mem_compl_iff, not_false_iff, or_true]
 #align set.preimage_inv_fun_of_mem Set.preimage_invFun_of_mem
 

Mathlib/Data/Set/Prod.lean

@@ -174,7 +174,7 @@ theorem prod_inter_prod : s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×
 
 theorem disjoint_prod : Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂ := by
   simp_rw [disjoint_left, mem_prod, not_and_or, Prod.forall, and_imp, ← @forall_or_right α, ←
-    @forall_or_left β, ← @forall_or_right (_ ∈ s₁), ← @forall_or_left (_ ∈ t₁), iff_self]
+    @forall_or_left β, ← @forall_or_right (_ ∈ s₁), ← @forall_or_left (_ ∈ t₁)]
 #align set.disjoint_prod Set.disjoint_prod
 
 theorem insert_prod : insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t := by
@@ -416,7 +416,6 @@ theorem prod_eq_prod_iff :
   rw [prod_eq_prod_iff_of_nonempty h]
   rw [nonempty_iff_ne_empty, Ne.def, prod_eq_empty_iff] at h
   simp_rw [h, false_and_iff, or_false_iff]
-  rfl
 #align set.prod_eq_prod_iff Set.prod_eq_prod_iff
 
 @[simp]
@@ -497,7 +496,7 @@ theorem range_diag : (range fun x => (x, x)) = diagonal α := by
 theorem prod_subset_compl_diagonal_iff_disjoint : s ×ˢ t ⊆ diagonal αᶜ ↔ Disjoint s t :=
   subset_compl_comm.trans <| by
     simp_rw [← range_diag, range_subset_iff, disjoint_left, mem_compl_iff, prod_mk_mem_set_prod_eq,
-      not_and, iff_self]
+      not_and]
 #align set.prod_subset_compl_diagonal_iff_disjoint Set.prod_subset_compl_diagonal_iff_disjoint
 
 @[simp]

Mathlib/Data/Set/Sigma.lean

@@ -222,7 +222,7 @@ theorem sigma_nonempty_iff : (s.Sigma t : Set _).Nonempty ↔ ∃ i ∈ s, (t i)
 theorem sigma_eq_empty_iff : s.Sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅ :=
   not_nonempty_iff_eq_empty.symm.trans <|
     sigma_nonempty_iff.not.trans <| by
-      simp only [not_nonempty_iff_eq_empty, not_and, not_exists] ; rfl
+      simp only [not_nonempty_iff_eq_empty, not_and, not_exists]
 #align set.sigma_eq_empty_iff Set.sigma_eq_empty_iff
 
 theorem image_sigmaMk_subset_sigma_left {a : ∀ i, α i} (ha : ∀ i, a i ∈ t i) :

Mathlib/Init/Data/Int/Basic.lean

@@ -33,9 +33,7 @@ namespace Int
 #align int.of_nat_add Int.ofNat_add
 #align int.of_nat_mul Int.ofNat_mul
 #align int.of_nat_succ Int.ofNat_succ
-#align int.neg_of_nat_of_succ Int.neg_ofNat_of_succ
-
-theorem neg_negSucc (n : ℕ) : - -[n+1] = ofNat (succ n) := rfl
+#align int.neg_of_nat_of_succ Int.neg_ofNat_succ
 #align int.neg_neg_of_nat_succ Int.neg_negSucc
 
 #align int.of_nat_eq_coe Int.ofNat_eq_coe

Mathlib/Init/Set.lean

@@ -67,7 +67,7 @@ macro_rules
   | `({ $x:ident | $p }) => `(setOf fun $x:ident ↦ $p)
   | `({ $x:ident : $t | $p }) => `(setOf fun $x:ident : $t ↦ $p)
   | `({ $x:ident $b:binderPred | $p }) =>
-    `(setOf fun $x:ident ↦ satisfiesBinderPred% $x $b ∧ $p)
+    `(setOf fun $x:ident ↦ satisfies_binder_pred% $x $b ∧ $p)
 
 @[app_unexpander setOf]
 def setOf.unexpander : Lean.PrettyPrinter.Unexpander

Mathlib/Logic/Basic.lean

@@ -397,8 +397,8 @@ theorem and_iff_not_or_not : a ∧ b ↔ ¬(¬a ∨ ¬b) := Decidable.and_iff_no
   simp only [not_and, Xor', not_or, not_not, ← iff_iff_implies_and_implies, iff_self]
 
 theorem xor_iff_not_iff (P Q : Prop) : Xor' P Q ↔ ¬ (P ↔ Q) := (not_xor P Q).not_right
-theorem xor_iff_iff_not : Xor' a b ↔ (a ↔ ¬b) := by simp only [← @xor_not_right a, not_not]; rfl
-theorem xor_iff_not_iff' : Xor' a b ↔ (¬a ↔ b) := by simp only [← @xor_not_left _ b, not_not]; rfl
+theorem xor_iff_iff_not : Xor' a b ↔ (a ↔ ¬b) := by simp only [← @xor_not_right a, not_not]
+theorem xor_iff_not_iff' : Xor' a b ↔ (¬a ↔ b) := by simp only [← @xor_not_left _ b, not_not]
 
 end Propositional
 
@@ -846,7 +846,7 @@ theorem bex_congr (H : ∀ x h, P x h ↔ Q x h) : (∃ x h, P x h) ↔ ∃ x h,
   exists_congr fun x ↦ exists_congr (H x)
 
 theorem bex_eq_left {a : α} : (∃ (x : _) (_ : x = a), p x) ↔ p a := by
-  simp only [exists_prop, exists_eq_left]; rfl
+  simp only [exists_prop, exists_eq_left]
 
 theorem BAll.imp_right (H : ∀ x h, P x h → Q x h) (h₁ : ∀ x h, P x h) (x h) : Q x h :=
   H _ _ <| h₁ _ _
@@ -949,7 +949,7 @@ theorem dite_ne_left_iff : dite P (fun _ ↦ a) B ≠ a ↔ ∃ h, a ≠ B h :=
   exact exists_congr fun h ↦ by rw [ne_comm]
 
 theorem dite_ne_right_iff : (dite P A fun _ ↦ b) ≠ b ↔ ∃ h, A h ≠ b := by
-  simp only [Ne.def, dite_eq_right_iff, not_forall]; rfl
+  simp only [Ne.def, dite_eq_right_iff, not_forall]
 
 theorem ite_ne_left_iff : ite P a b ≠ a ↔ ¬P ∧ a ≠ b :=
   dite_ne_left_iff.trans <| by simp only; rw [exists_prop]