[Merged by Bors] - chore: remove unused simps

Archive/Imo/Imo1988Q6.lean

@@ -207,7 +207,7 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
       hk (fun x => k * x) (fun x => x * x - k) fun _ _ => False <;>
     clear hk a b
   · -- We will now show that the fibers of the solution set are described by a quadratic equation.
-    intro x y; dsimp only
+    intro x y
     rw [← Int.coe_nat_inj', ← sub_eq_zero]
     apply eq_iff_eq_cancel_right.2
     simp; ring
@@ -265,7 +265,7 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^
       hk (fun x => k * x) (fun x => x * x + 1) fun x _ => x ≤ 1 <;>
     clear hk a b
   · -- We will now show that the fibers of the solution set are described by a quadratic equation.
-    intro x y; dsimp only
+    intro x y
     rw [← Int.coe_nat_inj', ← sub_eq_zero]
     apply eq_iff_eq_cancel_right.2
     simp; ring

Archive/Sensitivity.lean

@@ -399,7 +399,6 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
   let W := Span (e '' H)
   let img := range (g m)
   suffices 0 < dim (W ⊓ img) by
-    simp only [exists_prop]
     exact_mod_cast exists_mem_ne_zero_of_rank_pos this
   have dim_le : dim (W ⊔ img) ≤ 2 ^ (m + 1) := by
     convert ← rank_submodule_le (W ⊔ img)

Mathlib/Algebra/Associated.lean

@@ -145,9 +145,7 @@ theorem prime_pow_succ_dvd_mul {α : Type*} [CancelCommMonoidWithZero α] {p x y
   rw [or_iff_not_imp_right]
   intro hy
   induction' i with i ih generalizing x
-  · simp only [zero_add, pow_one] at *
-    rw [pow_one]
-    rw [pow_one] at hxy
+  · rw [pow_one] at hxy ⊢
     exact (h.dvd_or_dvd hxy).resolve_right hy
   rw [pow_succ] at hxy ⊢
   obtain ⟨x', rfl⟩ := (h.dvd_or_dvd (dvd_of_mul_right_dvd hxy)).resolve_right hy

Mathlib/Algebra/BigOperators/Basic.lean

@@ -1003,7 +1003,7 @@ theorem prod_ite_of_false {p : α → Prop} {hp : DecidablePred p} (f g : α →
     ∏ x in s, (if p x then f x else g x) = ∏ x in s, g x := by
   rw [prod_ite, filter_false_of_mem, filter_true_of_mem]
   · simp only [prod_empty, one_mul]
-  all_goals intros; simp; apply h; assumption
+  all_goals intros; apply h; assumption
 #align finset.prod_ite_of_false Finset.prod_ite_of_false
 #align finset.sum_ite_of_false Finset.sum_ite_of_false
 

Mathlib/Algebra/BigOperators/Ring.lean

@@ -151,8 +151,7 @@ theorem prod_add [DecidableEq α] (f g : α → β) (s : Finset α) :
             (by simp) (by simp))
         (fun t _ a _ => a ∈ t)
         (by simp [Classical.em])
-        (by simp_rw [mem_filter, Function.funext_iff, eq_iff_iff, mem_singleton, mem_pi,
-          mem_insert, iff_true, iff_false]; tauto)
+        (by simp_rw [mem_filter, Function.funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
         (by simp_rw [ext_iff, @mem_filter _ _ (id _), mem_powerset]; tauto)
 #align finset.prod_add Finset.prod_add
 

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -124,7 +124,7 @@ theorem left_unitality (X : Type u) :
   change q x' = Finsupp.mapDomain (λ_ X).hom (finsuppTensorFinsupp' R (𝟙_ (Type u)) X
     (Finsupp.single PUnit.unit 1 ⊗ₜ[R] Finsupp.single x 1)) x'
   simp_rw [finsuppTensorFinsupp'_single_tmul_single,
-    ModuleCat.MonoidalCategory.leftUnitor_hom_apply, Finsupp.smul_single', mul_one,
+    ModuleCat.MonoidalCategory.leftUnitor_hom_apply, mul_one,
     Finsupp.mapDomain_single, CategoryTheory.leftUnitor_hom_apply, one_smul]
 #align Module.free.left_unitality ModuleCat.Free.left_unitality
 
@@ -145,7 +145,7 @@ theorem right_unitality (X : Type u) :
   change q x' = Finsupp.mapDomain (ρ_ X).hom (finsuppTensorFinsupp' R X (𝟙_ (Type u))
     (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single PUnit.unit 1)) x'
   simp_rw [finsuppTensorFinsupp'_single_tmul_single,
-    ModuleCat.MonoidalCategory.rightUnitor_hom_apply, Finsupp.smul_single', mul_one,
+    ModuleCat.MonoidalCategory.rightUnitor_hom_apply, mul_one,
     Finsupp.mapDomain_single, CategoryTheory.rightUnitor_hom_apply, one_smul]
 #align Module.free.right_unitality ModuleCat.Free.right_unitality
 

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -544,7 +544,6 @@ def HomEquiv.fromExtendScalars {X Y} (g : X ⟶ (restrictScalars f).obj Y) :
       map_smul' := fun (r : R) (s : S) => ?_}
     · ext
       dsimp
-      simp only [LinearMap.coe_mk, LinearMap.add_apply]
       rw [← add_smul]
     · ext x
       apply mul_smul (f r) s (g x)

Mathlib/Algebra/CharP/MixedCharZero.lean

@@ -230,15 +230,15 @@ noncomputable def algebraRat (h : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸
       intro a b
       field_simp
       trans (↑((a * b).num * a.den * b.den) : R)
-      · simp_rw [Int.cast_mul, Int.cast_ofNat, Rat.coe_pnatDen]
+      · simp_rw [Int.cast_mul, Int.cast_ofNat]
         ring
       rw [Rat.mul_num_den' a b]
       simp
     map_add' := by
       intro a b
       field_simp
       trans (↑((a + b).num * a.den * b.den) : R)
-      · simp_rw [Int.cast_mul, Int.cast_ofNat, Rat.coe_pnatDen]
+      · simp_rw [Int.cast_mul, Int.cast_ofNat]
         ring
       rw [Rat.add_num_den' a b]
       simp }

Mathlib/Algebra/GeomSum.lean

@@ -86,7 +86,6 @@ theorem op_geom_sum (x : α) (n : ℕ) : op (∑ i in range n, x ^ i) = ∑ i in
 @[simp]
 theorem op_geom_sum₂ (x y : α) (n : ℕ) : ∑ i in range n, op y ^ (n - 1 - i) * op x ^ i =
     ∑ i in range n, op y ^ i * op x ^ (n - 1 - i):= by
-  simp only [op_sum, op_mul, op_pow]
   rw [← sum_range_reflect]
   refine' sum_congr rfl fun j j_in => _
   rw [mem_range, Nat.lt_iff_add_one_le] at j_in
@@ -319,7 +318,6 @@ protected theorem Commute.geom_sum₂_Ico_mul [Ring α] {x y : α} (h : Commute
   have : (∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k) =
       ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) := by
     refine' sum_congr rfl fun k _ => _
-    simp only [ge_iff_le, tsub_le_iff_right]
     have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
     simpa [Commute, SemiconjBy] using hp
   simp only [this]

Mathlib/Algebra/GroupPower/Basic.lean

@@ -176,7 +176,6 @@ theorem pow_eq_pow_mod {M : Type*} [Monoid M] {x : M} (m : ℕ) {n : ℕ} (h : x
     x ^ m = x ^ (m % n) := by
   have t : x ^ m = x ^ (n * (m / n) + m % n) :=
     congr_arg (fun a => x ^ a) ((Nat.add_comm _ _).trans (Nat.mod_add_div _ _)).symm
-  dsimp at t
   rw [t, pow_add, pow_mul, h, one_pow, one_mul]
 #align pow_eq_pow_mod pow_eq_pow_mod
 #align nsmul_eq_mod_nsmul nsmul_eq_mod_nsmul

Mathlib/Algebra/Homology/Homotopy.lean

@@ -349,7 +349,6 @@ def nullHomotopy (hom : ∀ i j, C.X i ⟶ D.X j) (zero : ∀ i j, ¬c.Rel j i 
 def nullHomotopy' (h : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) : Homotopy (nullHomotopicMap' h) 0 := by
   apply nullHomotopy fun i j => dite (c.Rel j i) (h i j) fun _ => 0
   intro i j hij
-  dsimp
   rw [dite_eq_right_iff]
   intro hij'
   exfalso
@@ -375,7 +374,6 @@ theorem nullHomotopicMap'_f {k₂ k₁ k₀ : ι} (r₂₁ : c.Rel k₂ k₁) (r
     (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁ := by
   simp only [nullHomotopicMap']
   rw [nullHomotopicMap_f r₂₁ r₁₀]
-  dsimp
   split_ifs
   rfl
 #align homotopy.null_homotopic_map'_f Homotopy.nullHomotopicMap'_f
@@ -395,7 +393,6 @@ theorem nullHomotopicMap'_f_of_not_rel_left {k₁ k₀ : ι} (r₁₀ : c.Rel k
     (nullHomotopicMap' h).f k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀ := by
   simp only [nullHomotopicMap']
   rw [nullHomotopicMap_f_of_not_rel_left r₁₀ hk₀]
-  dsimp
   split_ifs
   rfl
 #align homotopy.null_homotopic_map'_f_of_not_rel_left Homotopy.nullHomotopicMap'_f_of_not_rel_left
@@ -415,7 +412,6 @@ theorem nullHomotopicMap'_f_of_not_rel_right {k₁ k₀ : ι} (r₁₀ : c.Rel k
     (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ := by
   simp only [nullHomotopicMap']
   rw [nullHomotopicMap_f_of_not_rel_right r₁₀ hk₁]
-  dsimp
   split_ifs
   rfl
 #align homotopy.null_homotopic_map'_f_of_not_rel_right Homotopy.nullHomotopicMap'_f_of_not_rel_right

Mathlib/Algebra/Module/Injective.lean

@@ -419,7 +419,6 @@ def extensionOfMaxAdjoin (h : Module.Baer R Q) (y : N) : ExtensionOf i f where
         congr }
   is_extension m := by
     dsimp
-    simp only [LinearPMap.mk_apply, LinearMap.coe_mk]
     rw [(extensionOfMax i f).is_extension,
       ExtensionOfMaxAdjoin.extensionToFun_wd i f h _ ⟨i m, _⟩ 0 _, map_zero, add_zero]
     simp

Mathlib/Algebra/Module/Torsion.lean

@@ -426,8 +426,7 @@ theorem iSup_torsionBySet_ideal_eq_torsionBySet_iInf [DecidableEq ι] :
       · have := coe_mem (μ i)
         simp only [mem_iInf] at this
         exact Ideal.mul_mem_left _ _ (this j hj ij)
-    · simp_rw [coe_mk]
-      rw [← Finset.sum_smul, hμ, one_smul]
+    · rw [← Finset.sum_smul, hμ, one_smul]
 #align submodule.supr_torsion_by_ideal_eq_torsion_by_infi Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf
 
 -- Porting note: iSup_torsionBySet_ideal_eq_torsionBySet_iInf now requires DecidableEq ι

Mathlib/Algebra/Order/CompleteField.lean

@@ -261,7 +261,6 @@ theorem le_inducedMap_mul_self_of_mem_cutMap (ha : 0 < a) (b : β) (hb : b ∈ c
   trans (q' : β) ^ 2
   exact_mod_cast hqq'.le
   rw [pow_two] at hqa ⊢
-  push_cast at hqa
   exact mul_self_le_mul_self (by exact_mod_cast hq'.le)
     (le_csSup (cutMap_bddAbove β a) <|
       coe_mem_cutMap_iff.2 <| lt_of_mul_self_lt_mul_self ha.le hqa)

Mathlib/Algebra/QuaternionBasis.lean

@@ -125,9 +125,7 @@ theorem lift_add (x y : ℍ[R,c₁,c₂]) : q.lift (x + y) = q.lift x + q.lift y
 
 theorem lift_mul (x y : ℍ[R,c₁,c₂]) : q.lift (x * y) = q.lift x * q.lift y := by
   simp only [lift, Algebra.algebraMap_eq_smul_one]
-  simp only [add_mul]
-  simp_rw [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, ← Algebra.smul_def,
-    smul_add, smul_smul]
+  simp_rw [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, smul_smul]
   simp only [i_mul_i, j_mul_j, i_mul_j, j_mul_i, i_mul_k, k_mul_i, k_mul_j, j_mul_k, k_mul_k]
   simp only [smul_smul, smul_neg, sub_eq_add_neg, add_smul, ← add_assoc, mul_neg, neg_smul]
   simp only [mul_right_comm _ _ (c₁ * c₂), mul_comm _ (c₁ * c₂)]

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -220,7 +220,7 @@ def IsAffineOpen.fromSpec {X : Scheme} {U : Opens X} (hU : IsAffineOpen U) :
 
 instance IsAffineOpen.isOpenImmersion_fromSpec {X : Scheme} {U : Opens X}
     (hU : IsAffineOpen U) : IsOpenImmersion hU.fromSpec := by
-  delta IsAffineOpen.fromSpec; dsimp; simp only [Scheme.comp_val]
+  delta IsAffineOpen.fromSpec; dsimp
   -- Porting note : this was automatic
   repeat apply (config := { allowSynthFailures := true }) PresheafedSpace.IsOpenImmersion.comp
 #align algebraic_geometry.is_affine_open.is_open_immersion_from_Spec AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec

Mathlib/AlgebraicGeometry/Gluing.lean

@@ -378,7 +378,6 @@ theorem fromGlued_injective : Function.Injective 𝒰.fromGlued.1.base := by
   rw [𝒰.gluedCover.ι_eq_iff]
   right
   use e.hom ⟨⟨x, y⟩, h⟩
-  simp_rw [← comp_apply]
   constructor
   -- Porting note: in the two subproofs below, added the `change` lines
   · change (e.hom ≫ _) ⟨(x, y), h⟩ = x

Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean

@@ -236,7 +236,6 @@ def restrict {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : O
     LocallyRingedSpace where
   localRing := by
     intro x
-    dsimp at *
     -- We show that the stalk of the restriction is isomorphic to the original stalk,
     apply @RingEquiv.localRing _ _ _ (X.localRing (f x))
     exact (X.restrictStalkIso h x).symm.commRingCatIsoToRingEquiv

Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean

@@ -156,7 +156,6 @@ def pushforwardDiagramToColimit (F : J ⥤ PresheafedSpace.{_, _, v} C) :
       Opens.map_comp_obj, Pushforward.comp_inv_app, pushforwardEq_hom_app, eqToHom_op, id_eq,
       eqToHom_map, id_comp, assoc, eqToHom_trans]
     dsimp
-    simp only [eqToHom_trans, id_comp]
     congr 1
     -- The key fact is `(F.map f).c.congr`,
     -- which allows us in rewrite in the argument of `(F.map f).c.app`.

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -471,7 +471,7 @@ theorem carrier.smul_mem (c x : A) (hx : x ∈ carrier f_deg q) : c • x ∈ ca
   refine' DirectSum.Decomposition.inductionOn 𝒜 _ _ _
   · rw [zero_smul]; exact carrier.zero_mem f_deg hm _
   · rintro n ⟨a, ha⟩ i
-    simp_rw [Subtype.coe_mk, proj_apply, smul_eq_mul, coe_decompose_mul_of_left_mem 𝒜 i ha]
+    simp_rw [proj_apply, smul_eq_mul, coe_decompose_mul_of_left_mem 𝒜 i ha]
     -- Porting note: having trouble with Mul instance
     let product : A⁰_ f :=
       Mul.mul (Quotient.mk'' ⟨_, ⟨a ^ m, pow_mem_graded m ha⟩, ⟨_, ?_⟩, ⟨n, rfl⟩⟩ : A⁰_ f)
@@ -481,8 +481,8 @@ theorem carrier.smul_mem (c x : A) (hx : x ∈ carrier f_deg q) : c • x ∈ ca
       · dsimp
         erw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk'',
           HomogeneousLocalization.mul_val, HomogeneousLocalization.val_mk'',
-          HomogeneousLocalization.val_mk'', Subtype.coe_mk]
-        simp_rw [mul_pow, Subtype.coe_mk]; rw [Localization.mk_mul]
+          HomogeneousLocalization.val_mk'']
+        simp_rw [mul_pow]; rw [Localization.mk_mul]
         congr; erw [← pow_add, Nat.add_sub_of_le h]
         · rw [(_ : m • n = _)]; mem_tac; simp only [smul_eq_mul, mul_comm]
         · rw [(_ : m • (i - n) = _)]; mem_tac; simp only [smul_eq_mul, mul_comm]
@@ -543,7 +543,7 @@ theorem carrier.asIdeal.prime : (carrier.asIdeal f_deg hm q).IsPrime :=
       rw [← and_forall_ne nx, and_iff_left, ← and_forall_ne ny, and_iff_left]
       · apply q.2.mem_or_mem; convert hxy (nx + ny) using 1
         dsimp
-        simp_rw [proj_apply, decompose_of_mem_same 𝒜 hnx, decompose_of_mem_same 𝒜 hny,
+        simp_rw [decompose_of_mem_same 𝒜 hnx, decompose_of_mem_same 𝒜 hny,
           decompose_of_mem_same 𝒜 (SetLike.GradedMonoid.toGradedMul.mul_mem hnx hny),
           mul_pow, pow_add]
         simp only [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk'',
@@ -552,7 +552,7 @@ theorem carrier.asIdeal.prime : (carrier.asIdeal f_deg hm q).IsPrime :=
       all_goals
         intro n hn; convert q.1.zero_mem using 1
         rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk'',
-          HomogeneousLocalization.zero_val]; simp_rw [proj_apply, Subtype.coe_mk]
+          HomogeneousLocalization.zero_val]; simp_rw [proj_apply]
         convert mk_zero (S := Submonoid.powers f) _
         rw [decompose_of_mem_ne 𝒜 _ hn.symm, zero_pow hm]
         · first | exact hnx | exact hny

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean

@@ -371,7 +371,6 @@ theorem zeroLocus_vanishingIdeal_eq_closure (t : Set (ProjectiveSpectrum 𝒜))
 theorem vanishingIdeal_closure (t : Set (ProjectiveSpectrum 𝒜)) :
     vanishingIdeal (closure t) = vanishingIdeal t := by
   have := (gc_ideal 𝒜).u_l_u_eq_u t
-  dsimp only at this
   ext1
   erw [zeroLocus_vanishingIdeal_eq_closure 𝒜 t] at this
   exact this

Mathlib/AlgebraicTopology/CechNerve.lean

@@ -151,7 +151,6 @@ def cechNerveEquiv (X : SimplicialObject.Augmented C) (F : Arrow C) :
   invFun := equivalenceRightToLeft _ _
   left_inv := by
     intro A
-    dsimp
     ext
     · dsimp
       erw [WidePullback.lift_π]
@@ -167,7 +166,6 @@ def cechNerveEquiv (X : SimplicialObject.Augmented C) (F : Arrow C) :
     · rfl
   right_inv := by
     intro A
-    dsimp
     ext x : 2
     · refine' WidePullback.hom_ext _ _ _ (fun j => _) _
       · dsimp
@@ -309,7 +307,6 @@ def cechConerveEquiv (F : Arrow C) (X : CosimplicialObject.Augmented C) :
   invFun := equivalenceRightToLeft _ _
   left_inv := by
     intro A
-    dsimp
     ext x : 2
     · rfl
     · refine' WidePushout.hom_ext _ _ _ (fun j => _) _

Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

@@ -335,7 +335,6 @@ noncomputable def extraDegeneracy : SimplicialObject.Augmented.ExtraDegeneracy f
         subst hk
         erw [Fin.succ_succAbove_succ, ExtraDegeneracy.s_comp_π_succ,
           ExtraDegeneracy.s_comp_π_succ]
-        dsimp
         simp only [WidePullback.lift_π]
     · simp only [assoc, WidePullback.lift_base]
       erw [ExtraDegeneracy.s_comp_base, ExtraDegeneracy.s_comp_base]
@@ -354,7 +353,6 @@ noncomputable def extraDegeneracy : SimplicialObject.Augmented.ExtraDegeneracy f
         subst hk
         erw [Fin.succ_predAbove_succ, ExtraDegeneracy.s_comp_π_succ,
           ExtraDegeneracy.s_comp_π_succ]
-        dsimp
         simp only [WidePullback.lift_π]
     · simp only [assoc, WidePullback.lift_base]
       erw [ExtraDegeneracy.s_comp_base, ExtraDegeneracy.s_comp_base]

Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

@@ -264,8 +264,7 @@ theorem trans_assoc_reparam {x₀ x₁ x₂ x₃ : X} (p : Path x₀ x₁) (q :
     linarith
   · exfalso
     linarith
-  · simp only [h₁, if_false, dif_neg (show ¬False from id)]
-    congr
+  · congr
     ring
 #align path.homotopy.trans_assoc_reparam Path.Homotopy.trans_assoc_reparam
 

Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean

@@ -173,7 +173,6 @@ def prodToProdTop : πₓ A × πₓ B ⥤ πₓ (TopCat.of (A × B)) where
   map_id := by
     rintro ⟨x₀, x₁⟩
     simp only [CategoryTheory.prod_id, FundamentalGroupoid.id_eq_path_refl]
-    dsimp
     rfl
   map_comp {x y z} f g :=
     match x, y, z, f, g with

Mathlib/AlgebraicTopology/SplitSimplicialObject.lean

@@ -97,7 +97,6 @@ instance : Fintype (IndexSet Δ) :=
       simp only [unop_op, Sigma.mk.inj_iff, Fin.mk.injEq] at h₁
       have h₂ : Δ₁ = Δ₂ := by
         ext1
-        simp at h₁
         simpa only [Fin.mk_eq_mk] using h₁.1
       subst h₂
       refine' ext _ _ rfl _

Mathlib/Analysis/Analytic/Composition.lean

@@ -972,7 +972,6 @@ theorem sigma_pi_composition_eq_iff
         ofFn fun i : Fin (Composition.length a') => (b' i).blocks.sum at this
     simpa [Composition.blocks_sum, Composition.ofFn_blocksFun] using this
   induction h
-  simp only [true_and_iff, eq_self_iff_true, heq_iff_eq]
   ext1
   · rfl
   · simp only [heq_eq_eq, ofFn_inj] at H ⊢
@@ -1170,8 +1169,7 @@ def sigmaEquivSigmaPi (n : ℕ) :
       rw [get_of_eq (splitWrtComposition_join _ _ _)]
       · simp only [get_ofFn]
         rfl
-      · simp only [map_ofFn]
-        congr
+      · congr
       · simp only [map_ofFn]
         rfl
 #align composition.sigma_equiv_sigma_pi Composition.sigmaEquivSigmaPi

Mathlib/Analysis/Analytic/Inverse.lean

@@ -434,7 +434,6 @@ theorem radius_right_inv_pos_of_radius_pos_aux1 (n : ℕ) (p : ℕ → ℝ) (hp
         MultilinearMap.map_sum_finset (MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ) fun _ (m : ℕ) =>
           r * (a ^ m * p m)]
       simp only [MultilinearMap.mkPiAlgebra_apply]
-      dsimp
       simp [prod_const, ← mul_sum, mul_pow]
 #align formal_multilinear_series.radius_right_inv_pos_of_radius_pos_aux1 FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1
 

Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

@@ -237,7 +237,6 @@ theorem u_exists :
     · have I1 : x ∉ support f := by rwa [f_support]
       have I2 : -x ∉ support f := by
         rw [f_support]
-        simp only at hx
         simpa using hx
       simp only [mem_support, Classical.not_not] at I1 I2
       simp only [I1, I2, add_zero, zero_div]
@@ -459,7 +458,6 @@ theorem y_pos_of_mem_ball {D : ℝ} {x : E} (Dpos : 0 < D) (D_lt_one : D < 1)
         apply closedBall_subset_closedBall' _ (ball_subset_closedBall hy)
         rw [← one_smul ℝ x, dist_eq_norm, hz, ← sub_smul, one_smul, norm_smul, ID]
         simp only [B.ne', div_le_iff B, field_simps]
-        simp only [mem_ball_zero_iff] at hx
         nlinarith only [hx, D_lt_one]
     apply lt_of_lt_of_le _ (measure_mono C)
     apply measure_ball_pos

Mathlib/Analysis/Calculus/LHopital.lean

@@ -80,7 +80,6 @@ theorem lhopital_zero_right_on_Ioo (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x
   have cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x := fun x hx => (hc x hx).1
   rw [← nhdsWithin_Ioo_eq_nhdsWithin_Ioi hab]
   apply tendsto_nhdsWithin_congr this
-  simp only
   apply hdiv.comp
   refine' tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
     (tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds