[Merged by Bors] - chore: tidy various files

Mathlib/Algebra/BigOperators/Group/List.lean

@@ -432,9 +432,9 @@ lemma prod_rotate_eq_one_of_prod_eq_one :
   | [], _, _ => by simp
   | a :: l, hl, n => by
     have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
-    rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl;
-    rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq, ←
-      one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_self, mul_one]
+    rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl
+    rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
+      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_self, mul_one]
 
 end Group
 

Mathlib/Algebra/Homology/Embedding/Boundary.lean

@@ -9,11 +9,11 @@ import Mathlib.Algebra.Homology.HomologicalComplex
 /-!
 # Boundary of an embedding of complex shapes
 
-In the file `Algebra.Homology.Embedding.Basic`, given `p : ℤ`, we have defined
+In the file `Mathlib.Algebra.Homology.Embedding.Basic`, given `p : ℤ`, we have defined
 an embedding `embeddingUpIntGE p` of `ComplexShape.up ℕ` in `ComplexShape.up ℤ`
 which sends `n : ℕ` to `p + n`. The (canonical) truncation (`≥ p`) of
 `K : CochainComplex C ℤ` shall be defined as the extension to `ℤ`
-(see `Algebra.Homology.Embedding.Extend`) of
+(see `Mathlib.Algebra.Homology.Embedding.Extend`) of
 a certain cochain complex indexed by `ℕ`:
 
 `Q ⟶ K.X (p + 1) ⟶ K.X (p + 2) ⟶ K.X (p + 3) ⟶ ...`

Mathlib/Algebra/Module/Opposites.lean

@@ -10,7 +10,7 @@ import Mathlib.Algebra.Module.Equiv.Defs
 # Module operations on `Mᵐᵒᵖ`
 
 This file contains definitions that build on top of the group action definitions in
-`Algebra.GroupWithZero.Action.Opposite`.
+`Mathlib.Algebra.GroupWithZero.Action.Opposite`.
 -/
 
 

Mathlib/Algebra/Order/Ring/Basic.lean

@@ -41,22 +41,20 @@ theorem zero_pow_le_one : ∀ n : ℕ, (0 : R) ^ n ≤ 1
   | n + 1 => by rw [zero_pow n.succ_ne_zero]; exact zero_le_one
 
 theorem pow_add_pow_le (hx : 0 ≤ x) (hy : 0 ≤ y) (hn : n ≠ 0) : x ^ n + y ^ n ≤ (x + y) ^ n := by
-  rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩
+  rcases Nat.exists_eq_add_one_of_ne_zero hn with ⟨k, rfl⟩
   induction' k with k ih
-  · have eqn : Nat.succ Nat.zero = 1 := rfl
-    rw [eqn]
-    simp only [pow_one, le_refl]
+  · simp only [zero_add, pow_one, le_refl]
   · let n := k.succ
     have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
     have h2 := add_nonneg hx hy
     calc
-      x ^ n.succ + y ^ n.succ ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
+      x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
         rw [pow_succ' _ n, pow_succ' _ n]
         exact le_add_of_nonneg_right h1
       _ = (x + y) * (x ^ n + y ^ n) := by
         rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
           add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
-      _ ≤ (x + y) ^ n.succ := by
+      _ ≤ (x + y) ^ (n + 1) := by
         rw [pow_succ' _ n]
         exact mul_le_mul_of_nonneg_left (ih (Nat.succ_ne_zero k)) h2
 

Mathlib/Analysis/Calculus/LocalExtr/Basic.lean

@@ -90,7 +90,7 @@ theorem mem_posTangentConeAt_of_frequently_mem (h : ∃ᶠ t : ℝ in 𝓝[>] 0,
 
 /-- If `[x -[ℝ] x + y] ⊆ s`, then `y` belongs to the positive tangnet cone of `s`.
 
-Before 2024-07-13, this lemma used to be callsed `mem_posTangentConeAt_of_segment_subset`.
+Before 2024-07-13, this lemma used to be called `mem_posTangentConeAt_of_segment_subset`.
 See also `sub_mem_posTangentConeAt_of_segment_subset`
 for the lemma that used to be called `mem_posTangentConeAt_of_segment_subset`. -/
 theorem mem_posTangentConeAt_of_segment_subset (h : [x -[ℝ] x + y] ⊆ s) :
@@ -242,7 +242,7 @@ lemma one_mem_posTangentConeAt_iff_frequently :
     1 ∈ posTangentConeAt s a ↔ ∃ᶠ x in 𝓝[>] a, x ∈ s := by
   rw [one_mem_posTangentConeAt_iff_mem_closure, mem_closure_iff_frequently,
     frequently_nhdsWithin_iff, inter_comm]
-  rfl
+  simp_rw [mem_inter_iff]
 
 /-- **Fermat's Theorem**: the derivative of a function at a local minimum equals zero. -/
 theorem IsLocalMin.hasDerivAt_eq_zero (h : IsLocalMin f a) (hf : HasDerivAt f f' a) : f' = 0 := by

Mathlib/Analysis/Complex/Schwarz.lean

@@ -122,7 +122,7 @@ theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div [CompleteSpace E] [St
     (differentiableOn_dslope (isOpen_ball.mem_nhds (mem_ball_self h_R₁))).mpr hd
   have : g z = g z₀ := eqOn_of_isPreconnected_of_isMaxOn_norm (convex_ball c R₁).isPreconnected
     isOpen_ball g_diff h_z₀ g_max hz
-  simp [g] at this
+  simp only [g] at this
   simp [g, ← this]
 
 theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div' [CompleteSpace E]

Mathlib/Analysis/Convex/Uniform.lean

@@ -95,7 +95,7 @@ theorem exists_forall_closed_ball_dist_add_le_two_sub (hε : 0 < ε) :
     _ ≤ 2 - δ + δ' + δ' :=
       (add_le_add_three (h (h₁ _ hx') (h₁ _ hy') hxy') (h₂ _ hx hx'.le) (h₂ _ hy hy'.le))
     _ ≤ 2 - δ' := by
-      dsimp [δ']
+      dsimp only [δ']
       rw [← le_sub_iff_add_le, ← le_sub_iff_add_le, sub_sub, sub_sub]
       refine sub_le_sub_left ?_ _
       ring_nf

Mathlib/Analysis/NormedSpace/MazurUlam.lean

@@ -62,7 +62,7 @@ theorem midpoint_fixed {x y : PE} :
   -- Note that `f` doubles the value of `dist (e z) z`
   have hf_dist : ∀ e, dist (f e z) z = 2 * dist (e z) z := by
     intro e
-    dsimp [f, R]
+    dsimp only [trans_apply, coe_toIsometryEquiv, f, R]
     rw [dist_pointReflection_fixed, ← e.dist_eq, e.apply_symm_apply,
       dist_pointReflection_self_real, dist_comm]
   -- Also note that `f` maps `s` to itself

Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus.lean

@@ -131,9 +131,6 @@ theorem elementalStarAlgebra.isUnit_of_isUnit_of_isStarNormal (h : IsUnit a) :
   simp only [u, Units.coe_map, Units.val_inv_eq_inv_val, RingHom.toMonoidHom_eq_coe, Units.val_mk0,
     Units.coe_map_inv, MonoidHom.coe_coe, norm_algebraMap', norm_inv, Complex.norm_eq_abs,
     Complex.abs_ofReal, abs_norm, inv_inv]
-    --RingHom.coe_monoidHom,
-    -- Complex.abs_ofReal, map_inv₀,
-  --rw [norm_algebraMap', inv_inv, Complex.norm_eq_abs, abs_norm]I-
   /- Since `a` is invertible, by `spectrum_star_mul_self_of_isStarNormal`, the spectrum (in `A`)
     of `star a * a` is contained in the half-open interval `(0, ‖star a * a‖]`. Therefore, by basic
     spectral mapping properties, the spectrum of `‖star a * a‖ • 1 - star a * a` is contained in

Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Order.lean

@@ -100,9 +100,8 @@ lemma IsSelfAdjoint.toReal_spectralRadius_eq_norm {a : A} (ha : IsSelfAdjoint a)
 lemma CstarRing.norm_or_neg_norm_mem_spectrum [Nontrivial A] {a : A}
     (ha : IsSelfAdjoint a := by cfc_tac) : ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a := by
   have ha' : SpectrumRestricts a Complex.reCLM := ha.spectrumRestricts
-  have := ha.toReal_spectralRadius_eq_norm
-  convert Real.spectralRadius_mem_spectrum_or (ha'.image ▸ (spectrum.nonempty a).image _)
-    <;> exact id (Eq.symm this)
+  rw [← ha.toReal_spectralRadius_eq_norm]
+  exact Real.spectralRadius_mem_spectrum_or (ha'.image ▸ (spectrum.nonempty a).image _)
 
 lemma CstarRing.nnnorm_mem_spectrum_of_nonneg [Nontrivial A] {a : A} (ha : 0 ≤ a := by cfc_tac) :
     ‖a‖₊ ∈ spectrum ℝ≥0 a := by

Mathlib/CategoryTheory/Abelian/Basic.lean

@@ -611,8 +611,8 @@ instance epi_pullback_of_epi_f [Epi f] : Epi (pullback.snd f g) :=
     let u := biprod.desc (0 : X ⟶ R) e
     -- The composite pullback f g ⟶ X ⊞ Y ⟶ R is zero by assumption.
     have hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0 := by simpa [u]
-    -- pullback_to_biproduct f g is a kernel of (f, -g), so (f, -g) is a
-    -- cokernel of pullback_to_biproduct f g
+    -- pullbackToBiproduct f g is a kernel of (f, -g), so (f, -g) is a
+    -- cokernel of pullbackToBiproduct f g
     have :=
       epiIsCokernelOfKernel _
         (PullbackToBiproductIsKernel.isLimitPullbackToBiproduct f g)
@@ -643,8 +643,8 @@ instance epi_pullback_of_epi_g [Epi g] : Epi (pullback.fst f g) :=
     let u := biprod.desc e (0 : Y ⟶ R)
     -- The composite pullback f g ⟶ X ⊞ Y ⟶ R is zero by assumption.
     have hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0 := by simpa [u]
-    -- pullback_to_biproduct f g is a kernel of (f, -g), so (f, -g) is a
-    -- cokernel of pullback_to_biproduct f g
+    -- pullbackToBiproduct f g is a kernel of (f, -g), so (f, -g) is a
+    -- cokernel of pullbackToBiproduct f g
     have :=
       epiIsCokernelOfKernel _
         (PullbackToBiproductIsKernel.isLimitPullbackToBiproduct f g)

Mathlib/CategoryTheory/Grothendieck.lean

@@ -237,7 +237,7 @@ def functor {E : Cat.{v,u}} : (E ⥤ Cat.{v,u}) ⥤ Over (T := Cat.{v,u}) E wher
   map {F G} α := Over.homMk (X:= E) (Grothendieck.map α) Grothendieck.functor_comp_forget
   map_id F := by
     ext
-    exact Grothendieck.map_id_eq (F:= F)
+    exact Grothendieck.map_id_eq (F := F)
   map_comp α β := by
     simp [Grothendieck.map_comp_eq α β]
     rfl
@@ -246,13 +246,13 @@ universe w
 
 variable (G : C ⥤ Type w)
 
-/-- Auxiliary definition for `grothendieck_Type_to_Cat`, to speed up elaboration. -/
+/-- Auxiliary definition for `grothendieckTypeToCat`, to speed up elaboration. -/
 @[simps!]
 def grothendieckTypeToCatFunctor : Grothendieck (G ⋙ typeToCat) ⥤ G.Elements where
   obj X := ⟨X.1, X.2.as⟩
-  map := @fun X Y f => ⟨f.1, f.2.1.1⟩
+  map f := ⟨f.1, f.2.1.1⟩
 
-/-- Auxiliary definition for `grothendieck_Type_to_Cat`, to speed up elaboration. -/
+/-- Auxiliary definition for `grothendieckTypeToCat`, to speed up elaboration. -/
 -- Porting note:
 -- `simps` is incorrectly producing Prop-valued projections here,
 -- so we manually specify which ones to produce.

Mathlib/CategoryTheory/Sites/Subsheaf.lean

@@ -210,7 +210,7 @@ theorem Subpresheaf.sheafify_isSheaf (hF : Presieve.IsSheaf J F) :
     intro s
     constructor
     · intro H V i hi
-      dsimp only [x'', show x'' = fun V i hi => F.map (i₁ V i hi).op (x _ (hi₂ V i hi)) from rfl]
+      dsimp only [x'']
       conv_lhs => rw [← h₂ _ _ hi]
       rw [← H _ (hi₂ _ _ hi)]
       exact FunctorToTypes.map_comp_apply F (i₂ _ _ hi).op (i₁ _ _ hi).op _

Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

@@ -241,7 +241,7 @@ theorem adjMatrix_pow_apply_eq_card_walk [DecidableEq V] [Semiring α] (n : ℕ)
     · rintro ⟨x, hx⟩ - ⟨y, hy⟩ - hxy
       rw [disjoint_iff_inf_le]
       intro p hp
-      simp only [inf_eq_inter, mem_inter, mem_map, Function.Embedding.coeFn_mk, exists_prop] at hp;
+      simp only [inf_eq_inter, mem_inter, mem_map, Function.Embedding.coeFn_mk, exists_prop] at hp
       obtain ⟨⟨px, _, rfl⟩, ⟨py, hpy, hp⟩⟩ := hp
       cases hp
       simp at hxy
@@ -254,10 +254,7 @@ theorem one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes [DecidableEq V] [Decida
   rw [of_apply, add_apply, adjMatrix_apply, add_apply, adjMatrix_apply, one_apply]
   by_cases h : G.Adj i j
   · aesop
-  · rw [if_neg h]
-    by_cases heq : i = j
-    · repeat rw [if_pos heq, add_zero]
-    · rw [if_neg heq, if_neg heq, zero_add, zero_add, if_pos (refl 0)]
+  · split_ifs <;> simp_all
 
 theorem dotProduct_mulVec_adjMatrix [NonAssocSemiring α] (x y : V → α) :
     x ⬝ᵥ (G.adjMatrix α).mulVec y = ∑ i : V, ∑ j : V, if G.Adj i j then x i * y j else 0 := by

Mathlib/Control/Functor/Multivariate.lean

@@ -176,8 +176,7 @@ theorem LiftP_PredLast_iff {β} (P : β → Prop) (x : F (α ::: β)) :
   · intros
     rw [MvFunctor.map_map]
     dsimp (config := { unfoldPartialApp := true }) [(· ⊚ ·)]
-    suffices (fun i => Subtype.val) = (fun i x => (MvFunctor.f P n α i x).val)
-      by rw [this]
+    suffices (fun i => Subtype.val) = (fun i x => (MvFunctor.f P n α i x).val) by rw [this]
     ext i ⟨x, _⟩
     cases i <;> rfl
 
@@ -210,14 +209,13 @@ theorem LiftR_RelLast_iff (x y : F (α ::: β)) :
   · ext i ⟨x, _⟩ : 2
     cases i <;> rfl
   · intros
-    simp (config := { unfoldPartialApp := true }) [MvFunctor.map_map, (· ⊚ ·)]
+    simp (config := { unfoldPartialApp := true }) only [map_map, TypeVec.comp]
     -- Porting note: proof was
     -- rw [MvFunctor.map_map, MvFunctor.map_map, (· ⊚ ·), (· ⊚ ·)]
     -- congr <;> ext i ⟨x, _⟩ <;> cases i <;> rfl
     suffices  (fun i t => t.val.fst) = ((fun i x => (MvFunctor.f' rr n α i x).val.fst))
-            ∧ (fun i t => t.val.snd) = ((fun i x => (MvFunctor.f' rr n α i x).val.snd))
-    by  rcases this with ⟨left, right⟩
-        rw [left, right]
+            ∧ (fun i t => t.val.snd) = ((fun i x => (MvFunctor.f' rr n α i x).val.snd)) by
+      rw [this.1, this.2]
     constructor <;> ext i ⟨x, _⟩ <;> cases i <;> rfl
 
 end LiftPLastPredIff

Mathlib/Data/Int/Order/Units.lean

@@ -50,8 +50,8 @@ theorem sq_eq_one_of_sq_le_three {x : ℤ} (h1 : x ^ 2 ≤ 3) (h2 : x ≠ 0) : x
 
 theorem units_pow_eq_pow_mod_two (u : ℤˣ) (n : ℕ) : u ^ n = u ^ (n % 2) := by
   conv =>
-      lhs
-      rw [← Nat.mod_add_div n 2]
-      rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
+    lhs
+    rw [← Nat.mod_add_div n 2]
+    rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
 
 end Int

Mathlib/Data/Nat/Choose/Sum.lean

@@ -41,12 +41,12 @@ theorem add_pow (h : Commute x y) (n : ℕ) :
   have h_last : ∀ n, t n n.succ = 0 := fun n ↦ by
     simp only [t, choose_succ_self, cast_zero, mul_zero]
   have h_middle :
-    ∀ n i : ℕ, i ∈ range n.succ → (t n.succ ∘ Nat.succ) i =
+    ∀ n i : ℕ, i ∈ range n.succ → (t n.succ (Nat.succ i)) =
       x * t n i + y * t n i.succ := by
     intro n i h_mem
     have h_le : i ≤ n := Nat.le_of_lt_succ (mem_range.mp h_mem)
     dsimp only [t]
-    rw [Function.comp_apply, choose_succ_succ, Nat.cast_add, mul_add]
+    rw [choose_succ_succ, Nat.cast_add, mul_add]
     congr 1
     · rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
     · rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
@@ -58,9 +58,8 @@ theorem add_pow (h : Commute x y) (n : ℕ) :
   · rw [_root_.pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]
     dsimp only [t]
     rw [_root_.pow_zero, _root_.pow_zero, choose_self, Nat.cast_one, mul_one, mul_one]
-  · rw [sum_range_succ', h_first]
-    erw [sum_congr rfl (h_middle n), sum_add_distrib, add_assoc]
-    rw [pow_succ' (x + y), ih, add_mul, mul_sum, mul_sum]
+  · rw [sum_range_succ', h_first, sum_congr rfl (h_middle n), sum_add_distrib, add_assoc,
+      pow_succ' (x + y), ih, add_mul, mul_sum, mul_sum]
     congr 1
     rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']
 

Mathlib/Data/Rat/Defs.lean

@@ -305,7 +305,7 @@ attribute [simp] mkRat_eq_zero
 
 protected theorem mul_inv_cancel : a ≠ 0 → a * a⁻¹ = 1 :=
   numDenCasesOn' a fun n d hd hn ↦ by
-    simp [hd] at hn
+    simp only [divInt_ofNat, ne_eq, hd, not_false_eq_true, mkRat_eq_zero] at hn
     simp [-divInt_ofNat, mkRat_eq_divInt, Int.mul_comm, Int.mul_ne_zero hn (Int.ofNat_ne_zero.2 hd)]
 
 protected theorem inv_mul_cancel (h : a ≠ 0) : a⁻¹ * a = 1 :=

Mathlib/Geometry/RingedSpace/OpenImmersion.lean

@@ -377,12 +377,10 @@ def pullbackConeOfLeftLift : s.pt ⟶ (pullbackConeOfLeft f g).pt where
 
                 have : _ = s.snd.base := limit.lift_π s' WalkingCospan.right
                 conv_lhs =>
-                  erw [← this]
+                  rw [← this]
                   dsimp [s']
-                  -- Porting note: need a bit more hand holding here about function composition
-                  rw [show ∀ f g, f ∘ g = fun x => f (g x) from fun _ _ => rfl]
-                  erw [← Set.preimage_preimage]
-                erw [Set.preimage_image_eq _
+                  rw [Function.comp_def, ← Set.preimage_preimage]
+                rw [Set.preimage_image_eq _
                     (TopCat.snd_openEmbedding_of_left_openEmbedding hf.base_open g.base).inj]
                 rfl))
       naturality := fun U V i => by

Mathlib/GroupTheory/CoprodI.lean

@@ -1012,7 +1012,7 @@ theorem _root_.FreeGroup.injective_lift_of_ping_pong : Function.Injective (FreeG
     have hnne0 : n ≠ 0 := by
       rintro rfl
       apply hne1
-      simp [H]; rfl
+      simp [H, FreeGroup.freeGroupUnitEquivInt]
     clear hne1
     simp only [X']
     -- Positive and negative powers separately

Mathlib/GroupTheory/MonoidLocalization/Order.lean

@@ -24,7 +24,7 @@ variable [OrderedCancelCommMonoid α] {s : Submonoid α} {a₁ b₁ : α} {a₂
 instance le : LE (Localization s) :=
   ⟨fun a b =>
     Localization.liftOn₂ a b (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ ≤ a₂ * b₁)
-      @fun a₁ b₁ a₂ b₂ c₁ d₁ c₂ d₂ hab hcd => propext <| by
+      fun {a₁ b₁ a₂ b₂ c₁ d₁ c₂ d₂} hab hcd => propext <| by
         obtain ⟨e, he⟩ := r_iff_exists.1 hab
         obtain ⟨f, hf⟩ := r_iff_exists.1 hcd
         simp only [mul_right_inj] at he hf
@@ -37,7 +37,7 @@ instance le : LE (Localization s) :=
 instance lt : LT (Localization s) :=
   ⟨fun a b =>
     Localization.liftOn₂ a b (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ < a₂ * b₁)
-      @fun a₁ b₁ a₂ b₂ c₁ d₁ c₂ d₂ hab hcd => propext <| by
+      fun {a₁ b₁ a₂ b₂ c₁ d₁ c₂ d₂} hab hcd => propext <| by
         obtain ⟨e, he⟩ := r_iff_exists.1 hab
         obtain ⟨f, hf⟩ := r_iff_exists.1 hcd
         simp only [mul_right_inj] at he hf

Mathlib/LinearAlgebra/Contraction.lean

@@ -228,11 +228,10 @@ theorem lTensorHomEquivHomLTensor_toLinearMap :
   have h : Function.Surjective e.toLinearMap := e.surjective
   refine (cancel_right h).1 ?_
   ext f q m
-  dsimp [e, lTensorHomEquivHomLTensor]
-  simp only [lTensorHomEquivHomLTensor, dualTensorHomEquiv, compr₂_apply, mk_apply, coe_comp,
-    LinearEquiv.coe_toLinearMap, Function.comp_apply, map_tmul, LinearEquiv.coe_coe,
-    dualTensorHomEquivOfBasis_apply, LinearEquiv.trans_apply, congr_tmul, LinearEquiv.refl_apply,
-    dualTensorHomEquivOfBasis_symm_cancel_left, leftComm_tmul, dualTensorHom_apply, tmul_smul]
+  simp only [e, lTensorHomEquivHomLTensor, dualTensorHomEquiv, LinearEquiv.comp_coe, compr₂_apply,
+    mk_apply, LinearEquiv.coe_coe, LinearEquiv.trans_apply, congr_tmul, LinearEquiv.refl_apply,
+    dualTensorHomEquivOfBasis_apply, dualTensorHomEquivOfBasis_symm_cancel_left, leftComm_tmul,
+    dualTensorHom_apply, coe_comp, Function.comp_apply, lTensorHomToHomLTensor_apply, tmul_smul]
 
 @[simp]
 theorem rTensorHomEquivHomRTensor_toLinearMap :

Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

@@ -217,7 +217,7 @@ lemma derivative_det_one_add_X_smul (M : Matrix n n R) :
   · ext; simp [e]
   · delta trace
     rw [← (Fintype.equivFin n).symm.sum_comp]
-    rfl
+    simp_rw [e, reindexLinearEquiv_apply, reindex_apply, diag_apply, submatrix_apply]
 
 lemma coeff_det_one_add_X_smul_one (M : Matrix n n R) :
     (det (1 + (X : R[X]) • M.map C)).coeff 1 = trace M := by

Mathlib/LinearAlgebra/Matrix/HermitianFunctionalCalculus.lean

@@ -157,7 +157,7 @@ lemma cfc_eq (f : ℝ → ℝ) : cfc f A = hA.cfc f := by
   have := cfcHom_eq_of_continuous_of_map_id hA' hA.cfcAux hA.closedEmbedding_cfcAux.continuous
     hA.cfcAux_id
   rw [cfc_apply f A hA' (by rw [continuousOn_iff_continuous_restrict]; fun_prop), this]
-  rfl
+  simp only [cfcAux_apply, ContinuousMap.coe_mk, Function.comp, Set.restrict_apply, IsHermitian.cfc]
 
 end IsHermitian
 end Matrix

Mathlib/MeasureTheory/Function/UnifTight.lean

@@ -49,7 +49,7 @@ variable {α β ι : Type*} {m : MeasurableSpace α} {μ : Measure α} [NormedAd
 section UnifTight
 
 /- This follows closely the `UnifIntegrable` section
-from `MeasureTheory.Functions.UniformIntegrable`.-/
+from `Mathlib.MeasureTheory.Functions.UniformIntegrable`.-/
 
 variable {f g : ι → α → β} {p : ℝ≥0∞}
 
@@ -187,13 +187,11 @@ private theorem unifTight_fin (hp_top : p ≠ ∞) {n : ℕ} {f : Fin n → α 
     · simp only [Fin.coe_eq_castSucc, Fin.castSucc_mk, g]
   · rw [(_ : i = n)]
     · rw [compl_union, inter_comm, ← indicator_indicator]
-      apply (snorm_indicator_le _).trans
-      convert hfε.le
+      exact (snorm_indicator_le _).trans hfε.le
     · have hi' := Fin.is_lt i
       rw [Nat.lt_succ_iff] at hi'
       rw [not_lt] at hi
-      -- Porting note: Original proof was `simp [← le_antisymm hi' hi]`
-      ext; symm; rw [Fin.coe_ofNat_eq_mod, le_antisymm hi' hi, Nat.mod_succ_eq_iff_lt, Nat.lt_succ]
+      simp [← le_antisymm hi' hi]
 
 /-- A finite sequence of Lp functions is uniformly tight. -/
 theorem unifTight_finite [Finite ι] (hp_top : p ≠ ∞) {f : ι → α → β}