feat: implement simp_rw fails if unchanged

Mathlib/Algebra/Algebra/Operations.lean

@@ -175,9 +175,7 @@ theorem mul_le : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P :=
 theorem mul_toAddSubmonoid (M N : Submodule R A) :
     (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid := by
   dsimp [HMul.hMul, Mul.mul]  --porting note: added `hMul`
-  simp_rw [← LinearMap.mulLeft_toAddMonoidHom R, LinearMap.mulLeft, ← map_toAddSubmonoid _ N,
-    map₂]
-  rw [supᵢ_toAddSubmonoid]
+  rw [map₂, supᵢ_toAddSubmonoid]
   rfl
 #align submodule.mul_to_add_submonoid Submodule.mul_toAddSubmonoid
 
@@ -387,13 +385,13 @@ variable {M N P}
 
 theorem mem_span_singleton_mul {x y : A} : x ∈ span R {y} * P ↔ ∃ z ∈ P, y * z = x := by
   --porting note: need both `*` and `Mul.mul`
-  simp_rw [(· * ·), Mul.mul, map₂_span_singleton_eq_map, exists_prop]
+  simp_rw [(· * ·), Mul.mul, map₂_span_singleton_eq_map]
   rfl
 #align submodule.mem_span_singleton_mul Submodule.mem_span_singleton_mul
 
 theorem mem_mul_span_singleton {x y : A} : x ∈ P * span R {y} ↔ ∃ z ∈ P, z * y = x := by
   --porting note: need both `*` and `Mul.mul`
-  simp_rw [(· * ·), Mul.mul, map₂_span_singleton_eq_map_flip, exists_prop]
+  simp_rw [(· * ·), Mul.mul, map₂_span_singleton_eq_map_flip]
   rfl
 #align submodule.mem_mul_span_singleton Submodule.mem_mul_span_singleton
 
@@ -641,13 +639,13 @@ instance moduleSet : Module (SetSemiring A) (Submodule R A) where
   smul s P := span R (SetSemiring.down s) * P
   smul_add _ _ _ := mul_add _ _ _
   add_smul s t P := by
-    simp_rw [HSMul.hSMul, SMul.smul, SetSemiring.down_add, span_union, sup_mul, add_eq_sup]
+    simp_rw [HSMul.hSMul, SetSemiring.down_add, span_union, sup_mul, add_eq_sup]
   mul_smul s t P := by
-    simp_rw [HSMul.hSMul, SMul.smul, SetSemiring.down_mul, ← mul_assoc, span_mul_span]
+    simp_rw [HSMul.hSMul, SetSemiring.down_mul, ← mul_assoc, span_mul_span]
   one_smul P := by
-    simp_rw [HSMul.hSMul, SMul.smul, SetSemiring.down_one, ←one_eq_span_one_set, one_mul]
+    simp_rw [HSMul.hSMul, SetSemiring.down_one, ←one_eq_span_one_set, one_mul]
   zero_smul P := by
-    simp_rw [HSMul.hSMul, SMul.smul, SetSemiring.down_zero, span_empty, bot_mul, bot_eq_zero]
+    simp_rw [HSMul.hSMul, SetSemiring.down_zero, span_empty, bot_mul, bot_eq_zero]
   smul_zero _ := mul_bot _
 #align submodule.module_set Submodule.moduleSet
 

Mathlib/Algebra/BigOperators/Basic.lean

@@ -2069,7 +2069,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, eq_self_iff_true, not_true, IsEmpty.forall_iff, true_and_iff,
+      forall_eq_or_imp, Ne.def, 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]

Mathlib/Algebra/BigOperators/Fin.lean

@@ -330,9 +330,9 @@ def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
       induction' n with n ih
       · haveI : Subsingleton (Fin (m ^ 0)) := (Fin.cast <| pow_zero _).toEquiv.subsingleton
         exact Subsingleton.elim _ _
-      simp_rw [Fin.forall_iff, Fin.ext_iff, Fin.val_mk] at ih
+      simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
       ext
-      simp_rw [Fin.val_mk, Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one,
+      simp_rw [Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one,
         mul_one, pow_succ, ← Nat.div_div_eq_div_mul, mul_left_comm _ m, ← mul_sum]
       rw [ih _ (Nat.div_lt_of_lt_mul ?_), Nat.mod_add_div]
       -- porting note: replaces `a.is_lt` in the wildcard above. Caused by a refactor of the `npow`
@@ -366,7 +366,7 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
         replace := this (Fin.init n) (n (Fin.last _)) (Fin.init f) (f (Fin.last _))
         rw [← Fin.snoc_init_self f]
         simp (config := { singlePass := true }) only [← Fin.snoc_init_self n]
-        simp_rw [Fin.snoc_cast_succ, Fin.init_snoc, Fin.snoc_last, Fin.snoc_init_self n]
+        simp_rw [Fin.snoc_cast_succ, Fin.snoc_last, Fin.snoc_init_self n]
         exact this
       intro n nn f fn
       cases nn
@@ -391,9 +391,9 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
           (Fin.cast <| prod_empty).toEquiv.subsingleton
         exact Subsingleton.elim _ _
       · intro n x xs ih a
-        simp_rw [Fin.forall_iff, Fin.ext_iff, Fin.val_mk] at ih
+        simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
         ext
-        simp_rw [Fin.val_mk, Fin.sum_univ_succ, Fin.cons_succ]
+        simp_rw [Fin.sum_univ_succ, Fin.cons_succ]
         have := fun i : Fin n =>
           Fintype.prod_equiv (Fin.cast <| Fin.val_succ i).toEquiv
             (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Fin.is_lt _).le j))

Mathlib/Algebra/BigOperators/Finsupp.lean

@@ -477,7 +477,7 @@ theorem sum_univ_single [AddCommMonoid M] [Fintype α] (i : α) (m : M) :
 theorem sum_univ_single' [AddCommMonoid M] [Fintype α] (i : α) (m : M) :
     (∑ j : α, (single j m) i) = m := by
 -- Porting note: rewrite due to leaky classical in lean3
-  simp_rw [single, coe_mk, Finset.sum_pi_single]
+  simp_rw [single, coe_mk]
   classical rw [Finset.sum_pi_single]
   simp
 #align finsupp.sum_univ_single' Finsupp.sum_univ_single'

Mathlib/Algebra/CharZero/Quotient.lean

@@ -63,7 +63,7 @@ theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {
   let Zp := AddSubgroup.zmultiples p
   have : (Quotient.mk'' : R → R ⧸ Zp) = ((↑) : R → R ⧸ Zp) := rfl
   simp only [this]
-  simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_nsmul, ← QuotientAddGroup.mk_add,
+  simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add,
     QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]
   exact AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div hz
 #align quotient_add_group.zmultiples_zsmul_eq_zsmul_iff quotientAddGroup.zmultiples_zsmul_eq_zsmul_iff

Mathlib/Algebra/GroupPower/Order.lean

@@ -767,9 +767,8 @@ section LinearOrderedCommMonoidWithZero
 variable [LinearOrderedCommMonoidWithZero M] [NoZeroDivisors M] {a : M} {n : ℕ}
 
 theorem pow_pos_iff (hn : 0 < n) : 0 < a ^ n ↔ 0 < a := by
-  simp_rw [zero_lt_iff, pow_ne_zero_iff hn]
-  rw [pow_ne_zero_iff]
-  assumption
+  simp_rw [zero_lt_iff]
+  rw [pow_ne_zero_iff hn] -- Porting note: simp used to find unify the instances here
 #align pow_pos_iff pow_pos_iff
 
 end LinearOrderedCommMonoidWithZero

Mathlib/Algebra/Homology/Flip.lean

@@ -42,7 +42,6 @@ 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_rw [C.shape j j' w]
         simp_all only [shape, zero_f]
       d_comp_d' := fun j₁ j₂ j₃ _ _ => congr_hom (C.d_comp_d j₁ j₂ j₃) i }
   d i i' :=

Mathlib/Analysis/Convex/Join.lean

@@ -212,7 +212,7 @@ theorem convexHull_insert (hs : s.Nonempty) :
 theorem convexJoin_segments (a b c d : E) :
     convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = convexHull 𝕜 {a, b, c, d} := by
   simp_rw [← convexHull_pair, convexHull_insert (insert_nonempty _ _),
-    convexHull_insert (singleton_nonempty _), convexJoin_singletons, convexJoin_assoc,
+    convexHull_insert (singleton_nonempty _), convexJoin_assoc,
     convexHull_singleton]
 #align convex_join_segments convexJoin_segments
 
@@ -229,4 +229,3 @@ theorem convexJoin_singleton_segment (a b c : E) :
 -- porting note: moved 3 lemmas up to golf
 
 end LinearOrderedField
-

Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean

@@ -82,7 +82,7 @@ theorem balancedCore_empty : balancedCore 𝕜 (∅ : Set E) = ∅ :=
 #align balanced_core_empty balancedCore_empty
 
 theorem mem_balancedCore_iff : x ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t := by
-  simp_rw [balancedCore, mem_unionₛ, mem_setOf_eq, exists_prop, and_assoc]
+  simp_rw [balancedCore, mem_unionₛ, mem_setOf_eq, and_assoc]
 #align mem_balanced_core_iff mem_balancedCore_iff
 
 theorem smul_balancedCore_subset (s : Set E) {a : 𝕜} (ha : ‖a‖ ≤ 1) :

Mathlib/Analysis/Normed/Group/Seminorm.lean

@@ -584,7 +584,7 @@ instance : Sup (NonarchAddGroupSeminorm E) :=
       add_le_max' := fun x y =>
         sup_le ((map_add_le_max p x y).trans <| max_le_max le_sup_left le_sup_left)
           ((map_add_le_max q x y).trans <| max_le_max le_sup_right le_sup_right)
-      neg' := fun x => by simp_rw [Pi.sup_apply, Pi.sup_apply, map_neg_eq_map p, map_neg_eq_map q]}⟩
+      neg' := fun x => by simp_rw [Pi.sup_apply, map_neg_eq_map p, map_neg_eq_map q]}⟩
 
 @[simp, norm_cast]
 theorem coe_sup : ⇑(p ⊔ q) = ⇑p ⊔ ⇑q :=

Mathlib/Analysis/NormedSpace/LinearIsometry.lean

@@ -448,7 +448,7 @@ end LinearIsometry
 def LinearMap.toLinearIsometry (f : E →ₛₗ[σ₁₂] E₂) (hf : Isometry f) : E →ₛₗᵢ[σ₁₂] E₂ :=
   { f with
     norm_map' := by
-      simp_rw [← dist_zero_right, ← f.map_zero]
+      simp_rw [← dist_zero_right]
       simpa using (hf.dist_eq · 0) }
 #align linear_map.to_linear_isometry LinearMap.toLinearIsometry
 

Mathlib/Analysis/Seminorm.lean

@@ -404,7 +404,6 @@ theorem smul_le_smul {p q : Seminorm 𝕜 E} {a b : ℝ≥0} (hpq : p ≤ q) (ha
     a • p ≤ b • q := by
   simp_rw [le_def]
   intro x
-  simp_rw [Pi.smul_apply, NNReal.smul_def, smul_eq_mul]
   exact mul_le_mul hab (hpq x) (map_nonneg p x) (NNReal.coe_nonneg b)
 #align seminorm.smul_le_smul Seminorm.smul_le_smul
 

Mathlib/Combinatorics/Derangements/Basic.lean

@@ -63,7 +63,7 @@ protected def subtypeEquiv (p : α → Prop) [DecidablePred p] :
         refine' (Perm.subtypeEquivSubtypePerm p).subtypeEquiv fun f => ⟨fun hf a hfa ha => _, _⟩
         · refine' hf ⟨a, ha⟩ (Subtype.ext _)
           simp_rw [mem_fixedPoints, IsFixedPt, Perm.subtypeEquivSubtypePerm,
-          Equiv.coe_fn_mk, Subtype.coe_mk, Perm.ofSubtype_apply_of_mem _ ha] at hfa
+          Equiv.coe_fn_mk, Perm.ofSubtype_apply_of_mem _ ha] at hfa
           assumption
         rintro hf ⟨a, ha⟩ hfa
         refine' hf _ _ ha

Mathlib/Combinatorics/HalesJewett.lean

@@ -219,7 +219,7 @@ theorem prod_apply {α ι ι'} (l : Line α ι) (l' : Line α ι') (x : α) :
 
 @[simp]
 theorem diagonal_apply {α ι} [Nonempty ι] (x : α) : Line.diagonal α ι x = fun _ => x := by
-  simp_rw [Line.apply, Line.diagonal, Option.getD_none]
+  simp_rw [Line.diagonal, Option.getD_none]
 #align combinatorics.line.diagonal_apply Combinatorics.Line.diagonal_apply
 
 /-- The Hales-Jewett theorem. This version has a restriction on universe levels which is necessary
@@ -373,7 +373,7 @@ theorem exists_mono_homothetic_copy {M κ : Type _} [AddCommMonoid M] (S : Finse
     intro i hi
     rw [hs, Finset.compl_filter, Finset.mem_filter] at hi
     obtain ⟨y, hy⟩ := Option.ne_none_iff_exists.mp hi.right
-    simp_rw [Line.apply, ← hy, Option.map_some', Option.getD]
+    simp_rw [← hy, Option.map_some', Option.getD]
 #align combinatorics.exists_mono_homothetic_copy Combinatorics.exists_mono_homothetic_copy
 
 end Combinatorics

Mathlib/Combinatorics/SetFamily/Compression/Down.lean

@@ -175,8 +175,7 @@ open FinsetFamily
 original, or it's not in the original but it's the compression of something in the original. -/
 theorem mem_compression : s ∈ 𝓓 a 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 :=
   by
-  simp_rw [compression, mem_disjUnion, mem_filter, mem_image,
-    decide_eq_true_eq, and_comm (a := (¬ s ∈ 𝒜))]
+  simp_rw [compression, mem_disjUnion, mem_filter, mem_image, and_comm (a := (¬ s ∈ 𝒜))]
   refine'
     or_congr_right
       (and_congr_left fun hs =>

Mathlib/Combinatorics/SetFamily/LYM.lean

@@ -132,7 +132,7 @@ def falling : Finset (Finset α) :=
 variable {𝒜 k} {s : Finset α}
 
 theorem mem_falling : s ∈ falling k 𝒜 ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ s.card = k := by
-  simp_rw [falling, mem_sup, mem_powersetLen, exists_and_right]
+  simp_rw [falling, mem_sup, mem_powersetLen]
   aesop
 #align finset.mem_falling Finset.mem_falling
 
@@ -151,7 +151,7 @@ theorem falling_zero_subset : falling 0 𝒜 ⊆ {∅} :=
 
 theorem slice_union_shadow_falling_succ : 𝒜 # k ∪ (∂ ) (falling (k + 1) 𝒜) = falling k 𝒜 := by
   ext s
-  simp_rw [mem_union, mem_slice, mem_shadow_iff, exists_prop, mem_falling]
+  simp_rw [mem_union, mem_slice, mem_shadow_iff, mem_falling]
   constructor
   · rintro (h | ⟨s, ⟨⟨t, ht, hst⟩, hs⟩, a, ha, rfl⟩)
     · exact ⟨⟨s, h.1, Subset.refl _⟩, h.2⟩
@@ -174,7 +174,7 @@ theorem IsAntichain.disjoint_slice_shadow_falling {m n : ℕ}
     (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) : Disjoint (𝒜 # m) ((∂ ) (falling n 𝒜)) :=
   disjoint_right.2 fun s h₁ h₂ =>
     by
-    simp_rw [mem_shadow_iff, exists_prop, mem_falling] at h₁
+    simp_rw [mem_shadow_iff, mem_falling] at h₁
     obtain ⟨s, ⟨⟨t, ht, hst⟩, _⟩, a, ha, rfl⟩ := h₁
     refine' h𝒜 (slice_subset h₂) ht _ ((erase_subset _ _).trans hst)
     rintro rfl

Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean

@@ -91,7 +91,7 @@ theorem equitabilise_aux (hs : a * m + b * (m + 1) = s.card) :
     · simp only [extend_parts, mem_insert, forall_eq_or_imp, and_iff_left hR₁, htn, hn]
       exact ite_eq_or_eq _ _ _
     · exact fun x hx => (card_le_of_subset <| sdiff_subset _ _).trans (lt_succ_iff.1 <| h _ hx)
-    simp_rw [extend_parts, filter_insert, htn, hn, m.succ_ne_self.symm.ite_eq_right_iff]
+    simp_rw [extend_parts, filter_insert, htn, m.succ_ne_self.symm.ite_eq_right_iff]
     split_ifs with ha
     · rw [hR₃, if_pos ha]
     rw [card_insert_of_not_mem, hR₃, if_neg ha, tsub_add_cancel_of_le]

Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean

@@ -136,8 +136,7 @@ theorem antidiagonalTuple_zero_right : ∀ k, antidiagonalTuple k 0 = [0]
 @[simp]
 theorem antidiagonalTuple_one (n : ℕ) : antidiagonalTuple 1 n = [![n]] := by
   simp_rw [antidiagonalTuple, antidiagonal, List.range_succ, List.map_append, List.map_singleton,
-    tsub_self, List.bind_append, List.bind_singleton, antidiagonalTuple_zero_zero,
-    List.map_singleton, List.map_bind]
+    tsub_self, List.bind_append, List.bind_singleton, List.map_bind]
   conv_rhs => rw [← List.nil_append [![n]]]
   congr 1
   simp_rw [List.bind_eq_nil, List.mem_range, List.map_eq_nil]

Mathlib/Data/Finset/Basic.lean

@@ -2787,9 +2787,8 @@ theorem disjoint_filter_filter' (s t : Finset α)
 
 theorem disjoint_filter_filter_neg (s t : Finset α) (p : α → Prop)
     [DecidablePred p] [∀ x, Decidable (¬p x)] :
-    Disjoint (s.filter p) (t.filter fun a => ¬p a) := by
-  simp_rw [decide_not, Bool.decide_coe, Bool.not_eq_true']
-  exact disjoint_filter_filter' s t disjoint_compl_right
+    Disjoint (s.filter p) (t.filter fun a => ¬p a) :=
+  disjoint_filter_filter' s t disjoint_compl_right
 #align finset.disjoint_filter_filter_neg Finset.disjoint_filter_filter_neg
 
 theorem filter_disj_union (s : Finset α) (t : Finset α) (h : Disjoint s t) :
@@ -2860,7 +2859,6 @@ theorem filter_and (s : Finset α) : (s.filter fun a => p a ∧ q a) = s.filter
 
 theorem filter_not (s : Finset α) : (s.filter fun a => ¬p a) = s \ s.filter p :=
   ext <| fun a => by
-    simp_rw [decide_not]
     simp only [Bool.decide_coe, Bool.not_eq_true', mem_filter, and_comm, mem_sdiff, not_and_or,
       Bool.not_eq_true, and_or_left, and_not_self, or_false]
 #align finset.filter_not Finset.filter_not
@@ -3504,7 +3502,7 @@ theorem disjUnionᵢ_filter_eq_of_maps_to [DecidableEq β] {s : Finset α} {t :
     (h : ∀ x ∈ s, f x ∈ t) :
     t.disjUnionᵢ (fun a => s.filter (fun c => f c = a))
       (fun x' hx y' hy hne => by
-        simp_rw [disjoint_left, mem_filter, Bool.coe_decide]
+        simp_rw [disjoint_left, mem_filter]
         rintro i ⟨_, rfl⟩ ⟨_, rfl⟩
         exact hne rfl) = s :=
   ext fun b => by simpa using h b

Mathlib/Data/Finset/Card.lean

@@ -586,7 +586,7 @@ theorem two_lt_card_iff : 2 < s.card ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c 
 #align finset.two_lt_card_iff Finset.two_lt_card_iff
 
 theorem two_lt_card : 2 < s.card ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c := by
-  simp_rw [two_lt_card_iff, exists_prop, exists_and_left]
+  simp_rw [two_lt_card_iff, exists_and_left]
 #align finset.two_lt_card Finset.two_lt_card
 
 theorem exists_ne_of_one_lt_card (hs : 1 < s.card) (a : α) : ∃ b, b ∈ s ∧ b ≠ a := by

Mathlib/Data/Finset/Functor.lean

@@ -104,7 +104,7 @@ instance lawfulApplicative : LawfulApplicative Finset :=
       by
       rw [seq_def, fmap_def, seqLeft_def]
       obtain rfl | ht := t.eq_empty_or_nonempty
-      · simp_rw [if_pos rfl, image_empty, if_true]
+      · simp_rw [image_empty, if_true]
         exact (sup_bot _).symm
       · ext a
         rw [if_neg ht.ne_empty, mem_sup]

Mathlib/Data/Finset/Interval.lean

@@ -77,7 +77,7 @@ variable {s t}
 
 theorem Icc_eq_image_powerset (h : s ⊆ t) : Icc s t = (t \ s).powerset.image ((· ∪ ·) s) := by
   ext u
-  simp_rw [mem_Icc, mem_image, exists_prop, mem_powerset]
+  simp_rw [mem_Icc, mem_image, mem_powerset]
   constructor
   · rintro ⟨hs, ht⟩
     exact ⟨u \ s, sdiff_le_sdiff_right ht, sup_sdiff_cancel_right hs⟩
@@ -87,7 +87,7 @@ theorem Icc_eq_image_powerset (h : s ⊆ t) : Icc s t = (t \ s).powerset.image (
 
 theorem Ico_eq_image_ssubsets (h : s ⊆ t) : Ico s t = (t \ s).ssubsets.image ((· ∪ ·) s) := by
   ext u
-  simp_rw [mem_Ico, mem_image, exists_prop, mem_ssubsets]
+  simp_rw [mem_Ico, mem_image, mem_ssubsets]
   constructor
   · rintro ⟨hs, ht⟩
     exact ⟨u \ s, sdiff_lt_sdiff_right ht hs, sup_sdiff_cancel_right hs⟩

Mathlib/Data/Finset/Sigma.lean

@@ -132,7 +132,7 @@ theorem mem_sigmaLift (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (a : Si
   obtain ⟨⟨i, a⟩, j, b⟩ := a, b
   obtain rfl | h := Decidable.eq_or_ne i j
   · constructor
-    · simp_rw [sigmaLift, dif_pos rfl, mem_map, Embedding.sigmaMk_apply]
+    · simp_rw [sigmaLift]
       simp only [dite_eq_ite, ite_true, mem_map, Embedding.sigmaMk_apply, forall_exists_index,
         and_imp]
       rintro x hx rfl
@@ -176,7 +176,7 @@ theorem sigmaLift_nonempty :
 #align finset.sigma_lift_nonempty Finset.sigmaLift_nonempty
 
 theorem sigmaLift_eq_empty : sigmaLift f a b = ∅ ↔ ∀ h : a.1 = b.1, f (h ▸ a.2) b.2 = ∅ := by
-  simp_rw [nonempty_iff_ne_empty, sigmaLift]
+  simp_rw [sigmaLift]
   split_ifs with h
   . simp [h, forall_prop_of_true h]
   . simp [h, forall_prop_of_false h]
@@ -194,7 +194,7 @@ variable (f a b)
 
 theorem card_sigmaLift :
     (sigmaLift f a b).card = dite (a.1 = b.1) (fun h => (f (h ▸ a.2) b.2).card) fun _ => 0 := by
-  simp_rw [nonempty_iff_ne_empty, sigmaLift]
+  simp_rw [sigmaLift]
   split_ifs with h <;> simp [h]
 #align finset.card_sigma_lift Finset.card_sigmaLift