chore: tidy various files (#14968)

Author: Ruben-VandeVelde

Mathlib/Algebra/Category/Ring/Colimits.lean

@@ -38,8 +38,11 @@ variable {J : Type v} [SmallCategory J] (F : J ⥤ RingCat.{v})
 /-- An inductive type representing all ring expressions (without Relations)
 on a collection of types indexed by the objects of `J`.
 -/
-inductive Prequotient -- There's always `of`
-  | of : ∀ (j : J) (_ : F.obj j), Prequotient -- Then one generator for each operation
+inductive Prequotient
+  -- There's always `of`
+  | of : ∀ (j : J) (_ : F.obj j), Prequotient
+
+  -- Then one generator for each operation
   | zero : Prequotient
   | one : Prequotient
   | neg : Prequotient → Prequotient

Mathlib/Algebra/GeomSum.lean

@@ -92,16 +92,14 @@ theorem geom_sum₂_with_one (x : α) (n : ℕ) :
 protected theorem Commute.geom_sum₂_mul_add {x y : α} (h : Commute x y) (n : ℕ) :
     (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n := by
   let f :  ℕ → ℕ → α := fun m i : ℕ => (x + y) ^ i * y ^ (m - 1 - i)
-  -- Porting note: adding `hf` here, because below in two places `dsimp [f]` didn't work
-  have hf : ∀ m i : ℕ, f m i = (x + y) ^ i * y ^ (m - 1 - i) := by
-    simp only [tsub_le_iff_right, forall_const]
   change (∑ i ∈ range n, (f n) i) * x + y ^ n = (x + y) ^ n
   induction' n with n ih
   · rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
   · have f_last : f (n + 1) n = (x + y) ^ n := by
-      rw [hf, ← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
+      dsimp only [f]
+      rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
     have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := fun i hi => by
-      rw [hf]
+      dsimp only [f]
       have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
       rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ' y (n - 1 - i)]
       congr 2

Mathlib/Algebra/Group/Action/Basic.lean

@@ -11,7 +11,7 @@ import Mathlib.GroupTheory.Perm.Basic
 # More lemmas about group actions
 
 This file contains lemmas about group actions that require more imports than
-`Algebra.Group.Action.Defs` offers.
+`Mathlib.Algebra.Group.Action.Defs` offers.
 -/
 
 assert_not_exists MonoidWithZero

Mathlib/Algebra/Lie/Weights/Cartan.lean

@@ -283,9 +283,9 @@ lemma mem_corootSpace' {x : H} :
   suffices H.subtype '' s = {⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))} by
     obtain ⟨x, hx⟩ := x
     erw [← (H : Submodule R L).injective_subtype.mem_set_image (s := Submodule.span R s)]
-    change _ ↔ x ∈ (Submodule.span R s).map H.subtype
-    rw [Submodule.map_span, mem_corootSpace, ← this]
-    rfl
+    rw [mem_image]
+    simp_rw [SetLike.mem_coe]
+    rw [← Submodule.mem_map, Submodule.coeSubtype, Submodule.map_span, mem_corootSpace, ← this]
   ext u
   simp only [Submodule.coeSubtype, mem_image, Subtype.exists, LieSubalgebra.mem_coe_submodule,
     exists_and_right, exists_eq_right, mem_setOf_eq, s]

Mathlib/Algebra/Module/Submodule/Localization.lean

@@ -144,8 +144,8 @@ lemma LinearMap.localized'_ker_eq_ker_localizedMap (g : M →ₗ[R] P) :
 lemma LinearMap.ker_localizedMap_eq_localized'_ker (g : M →ₗ[R] P) :
     LinearMap.ker (IsLocalizedModule.map p f f' g) =
       ((LinearMap.ker g).localized' S p f).restrictScalars _ := by
-  rw [localized'_ker_eq_ker_localizedMap S p f f']
-  rfl
+  ext
+  simp [localized'_ker_eq_ker_localizedMap S p f f']
 
 /--
 The canonical map from the kernel of `g` to the kernel of `g` localized at a submonoid.

Mathlib/Algebra/Star/NonUnitalSubsemiring.lean

@@ -68,7 +68,7 @@ Useful to fix definitional equalities. -/
 protected def copy (S : NonUnitalStarSubsemiring R) (s : Set R) (hs : s = ↑S) :
     NonUnitalStarSubsemiring R :=
   { S.toNonUnitalSubsemiring.copy s hs with
-    star_mem' := @fun x (hx : x ∈ s) => by
+    star_mem' := fun {x} (hx : x ∈ s) => by
       show star x ∈ s
       rw [hs] at hx ⊢
       exact S.star_mem' hx }

Mathlib/Algebra/Tropical/BigOperators.lean

@@ -99,14 +99,12 @@ theorem Multiset.untrop_sum [LinearOrder R] [OrderTop R] (s : Multiset (Tropical
     untrop s.sum = Multiset.inf (s.map untrop) := by
   induction' s using Multiset.induction with s x IH
   · simp
-  · simp only [sum_cons, untrop_add, untrop_le_iff, map_cons, inf_cons, ← IH]
-    rfl
+  · simp only [sum_cons, untrop_add, untrop_le_iff, map_cons, inf_cons, ← IH, inf_eq_min]
 
 theorem Finset.untrop_sum' [LinearOrder R] [OrderTop R] (s : Finset S) (f : S → Tropical R) :
     untrop (∑ i ∈ s, f i) = s.inf (untrop ∘ f) := by
   convert Multiset.untrop_sum (s.val.map f)
-  simp only [Multiset.map_map, Function.comp_apply]
-  rfl
+  simp only [Multiset.map_map, Function.comp_apply, inf_def]
 
 theorem untrop_sum_eq_sInf_image [ConditionallyCompleteLinearOrder R] (s : Finset S)
     (f : S → Tropical (WithTop R)) : untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' s) := by
@@ -116,8 +114,7 @@ theorem untrop_sum_eq_sInf_image [ConditionallyCompleteLinearOrder R] (s : Finse
 
 theorem untrop_sum [ConditionallyCompleteLinearOrder R] [Fintype S] (f : S → Tropical (WithTop R)) :
     untrop (∑ i : S, f i) = ⨅ i : S, untrop (f i) := by
-  rw [iInf,← Set.image_univ,← coe_univ, untrop_sum_eq_sInf_image]
-  rfl
+  rw [iInf, ← Set.image_univ, ← coe_univ, untrop_sum_eq_sInf_image, Function.comp_def]
 
 /-- Note we cannot use `i ∈ s` instead of `i : s` here
 as it is simply not true on conditionally complete lattices! -/

Mathlib/Algebra/Vertex/HVertexOperator.lean

@@ -59,8 +59,7 @@ def coeff (A : HVertexOperator Γ R V W) (n : Γ) : V →ₗ[R] W where
   toFun v := ((of R).symm (A v)).coeff n
   map_add' _ _ := by simp
   map_smul' _ _ := by
-    simp only [map_smul, RingHom.id_apply]
-    exact rfl
+    simp only [map_smul, RingHom.id_apply, of_symm_smul, HahnSeries.smul_coeff]
 
 @[deprecated (since := "2024-06-18")] alias _root_.VertexAlg.coeff := coeff
 
@@ -85,12 +84,8 @@ condition, we produce a heterogeneous vertex operator. -/
 def of_coeff (f : Γ → V →ₗ[R] W)
     (hf : ∀(x : V), (Function.support (f · x)).IsPWO) : HVertexOperator Γ R V W where
   toFun x := (of R) { coeff := fun g => f g x, isPWO_support' := hf x }
-  map_add' _ _ := by
-    ext
-    simp
-  map_smul' _ _ := by
-    simp only [map_smul, RingHom.id_apply]
-    exact rfl
+  map_add' _ _ := by ext; simp
+  map_smul' _ _ := by ext; simp
 
 @[deprecated (since := "2024-06-18")] alias _root_.VertexAlg.HetVertexOperator.of_coeff := of_coeff
 
@@ -122,14 +117,14 @@ theorem compHahnSeries_add (u v : U) :
     compHahnSeries A B (u + v) = compHahnSeries A B u + compHahnSeries A B v := by
   ext
   simp only [compHahnSeries_coeff, map_add, coeff_apply, HahnSeries.add_coeff', Pi.add_apply]
-  rw [← @HahnSeries.add_coeff]
+  rw [← HahnSeries.add_coeff]
 
 @[simp]
 theorem compHahnSeries_smul (r : R) (u : U) :
     compHahnSeries A B (r • u) = r • compHahnSeries A B u := by
   ext
   simp only [compHahnSeries_coeff, LinearMapClass.map_smul, coeff_apply, HahnSeries.smul_coeff]
-  exact rfl
+  rw [← HahnSeries.smul_coeff]
 
 /-- The composite of two heterogeneous vertex operators, as a heterogeneous vertex operator. -/
 @[simps]
@@ -143,9 +138,8 @@ def comp : HVertexOperator (Γ' ×ₗ Γ) R U W where
   map_smul' := by
     intro r x
     ext g
-    simp only [HahnSeries.ofIterate, compHahnSeries_smul, Equiv.symm_apply_apply, RingHom.id_apply,
-      HahnSeries.smul_coeff, compHahnSeries_coeff, coeff_apply]
-    exact rfl
+    simp only [HahnSeries.ofIterate, compHahnSeries_smul, HahnSeries.smul_coeff,
+      compHahnSeries_coeff, coeff_apply, Equiv.symm_apply_apply, RingHom.id_apply, of_symm_smul]
 
 @[simp]
 theorem comp_coeff (g : Γ' ×ₗ Γ) :

Mathlib/CategoryTheory/Bicategory/Coherence.lean

@@ -77,7 +77,7 @@ See `inclusion`.
 def preinclusion (B : Type u) [Quiver.{v + 1} B] :
     PrelaxFunctor (LocallyDiscrete (Paths B)) (FreeBicategory B) where
   obj a := a.as
-  map := @fun a b f => (@inclusionPath B _ a.as b.as).obj f
+  map {a b} f := (@inclusionPath B _ a.as b.as).obj f
   map₂ η := (inclusionPath _ _).map η
 
 @[simp]

Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

@@ -59,8 +59,8 @@ instance [Inhabited C] : Inhabited (LocallyDiscrete C) :=
   ⟨⟨default⟩⟩
 
 instance categoryStruct [CategoryStruct.{v} C] : CategoryStruct (LocallyDiscrete C) where
-  Hom := fun a b => Discrete (a.as ⟶ b.as)
-  id := fun a => ⟨𝟙 a.as⟩
+  Hom a b := Discrete (a.as ⟶ b.as)
+  id a := ⟨𝟙 a.as⟩
   comp f g := ⟨f.as ≫ g.as⟩
 
 variable [CategoryStruct.{v} C]