chore: tidy various files (#2950)

Mathlib/Algebra/Star/Basic.lean

@@ -78,7 +78,8 @@ namespace StarMemClass
 
 variable {S : Type u} [Star R] [SetLike S R] [hS : StarMemClass S R] (s : S)
 
-instance : Star s where star r := ⟨star (r : R), star_mem r.prop⟩
+nonrec instance star : Star s where
+  star r := ⟨star (r : R), star_mem r.prop⟩
 
 end StarMemClass
 

Mathlib/Algebra/Star/Subalgebra.lean

@@ -47,30 +47,30 @@ variable [Semiring B] [StarRing B] [Algebra R B] [StarModule R B]
 variable [Semiring C] [StarRing C] [Algebra R C] [StarModule R C]
 
 instance setLike : SetLike (StarSubalgebra R A) A where
-  coe := fun S ↦ S.carrier
-  coe_injective' := fun p q h => by obtain ⟨⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩, _⟩ := p; cases q; congr
+  coe S := S.carrier
+  coe_injective' p q h := by obtain ⟨⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩, _⟩ := p; cases q; congr
 
 instance starMemClass : StarMemClass (StarSubalgebra R A) A where
-  star_mem := @fun s => s.star_mem'
+  star_mem {s} := s.star_mem'
 
 
 instance subsemiringClass : SubsemiringClass (StarSubalgebra R A) A where
-  add_mem := @fun s => s.add_mem'
-  mul_mem := @fun s => s.mul_mem'
-  one_mem := @fun s => s.one_mem'
-  zero_mem := @fun s => s.zero_mem'
+  add_mem {s} := s.add_mem'
+  mul_mem {s} := s.mul_mem'
+  one_mem {s} := s.one_mem'
+  zero_mem {s} := s.zero_mem'
 
 -- porting note: work around lean4#2074
 -- the following instance works with `set_option synthInstance.etaExperiment true`
 attribute [-instance] Ring.toNonAssocRing Ring.toNonUnitalRing CommRing.toNonUnitalCommRing
 
 instance subringClass {R A} [CommRing R] [StarRing R] [Ring A] [StarRing A] [Algebra R A]
     [StarModule R A] : SubringClass (StarSubalgebra R A) A where
-  neg_mem := @fun s a ha => show -a ∈ s.toSubalgebra from neg_mem ha
+  neg_mem {s a} ha := show -a ∈ s.toSubalgebra from neg_mem ha
 
 -- this uses the `Star` instance `s` inherits from `StarMemClass (StarSubalgebra R A) A`
 instance starRing (s : StarSubalgebra R A) : StarRing s :=
-  { StarMemClass.instStarSubtypeMemInstMembership s with
+  { StarMemClass.star s with
     star_involutive := fun r => Subtype.ext (star_star (r : A))
     star_mul := fun r₁ r₂ => Subtype.ext (star_mul (r₁ : A) (r₂ : A))
     star_add := fun r₁ r₂ => Subtype.ext (star_add (r₁ : A) (r₂ : A)) }
@@ -173,8 +173,7 @@ theorem toSubalgebra_subtype : S.toSubalgebra.val = S.subtype.toAlgHom :=
 
 /-- The inclusion map between `StarSubalgebra`s given by `Subtype.map id` as a `StarAlgHom`. -/
 @[simps]
-def inclusion {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) : S₁ →⋆ₐ[R] S₂
-    where
+def inclusion {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) : S₁ →⋆ₐ[R] S₂ where
   toFun := Subtype.map id h
   map_one' := rfl
   map_mul' _ _ := rfl
@@ -340,17 +339,14 @@ variable [Semiring A] [Algebra R A] [StarRing A] [StarModule R A]
 variable [Semiring B] [Algebra R B] [StarRing B] [StarModule R B]
 
 /-- The pointwise `star` of a subalgebra is a subalgebra. -/
-instance involutiveStar : InvolutiveStar (Subalgebra R A)
-    where
+instance involutiveStar : InvolutiveStar (Subalgebra R A) where
   star S :=
     { carrier := star S.carrier
-      mul_mem' := @fun x y hx hy =>
-        by
+      mul_mem' := fun {x y} hx hy => by
         simp only [Set.mem_star, Subalgebra.mem_carrier] at *
         exact (star_mul x y).symm ▸ mul_mem hy hx
       one_mem' := Set.mem_star.mp ((star_one A).symm ▸ one_mem S : star (1 : A) ∈ S)
-      add_mem' := @fun x y hx hy =>
-        by
+      add_mem' := fun {x y} hx hy => by
         simp only [Set.mem_star, Subalgebra.mem_carrier] at *
         exact (star_add x y).symm ▸ add_mem hx hy
       zero_mem' := Set.mem_star.mp ((star_zero A).symm ▸ zero_mem S : star (0 : A) ∈ S)
@@ -395,7 +391,7 @@ containing both `S` and `star S`. -/
 @[simps!]
 def starClosure (S : Subalgebra R A) : StarSubalgebra R A :=
   { S ⊔ star S with
-    star_mem' := @fun a ha =>
+    star_mem' := fun {a} ha =>
       by
       simp only [Subalgebra.mem_carrier, ← (@Algebra.gi R A _ _ _).l_sup_u _ _] at *
       rw [← mem_star_iff _ a, star_adjoin_comm, sup_comm]
@@ -433,7 +429,7 @@ variable (R)
 @[simps!]
 def adjoin (s : Set A) : StarSubalgebra R A :=
   { Algebra.adjoin R (s ∪ star s) with
-    star_mem' := @fun x hx => by
+    star_mem' := fun hx => by
       rwa [Subalgebra.mem_carrier, ← Subalgebra.mem_star_iff, Subalgebra.star_adjoin_comm,
         Set.union_star, star_star, Set.union_comm] }
 #align star_subalgebra.adjoin StarSubalgebra.adjoin
@@ -476,8 +472,7 @@ protected theorem gc : GaloisConnection (adjoin R : Set A → StarSubalgebra R A
 #align star_subalgebra.gc StarSubalgebra.gc
 
 /-- Galois insertion between `adjoin` and `coe`. -/
-protected def gi : GaloisInsertion (adjoin R : Set A → StarSubalgebra R A) (↑)
-    where
+protected def gi : GaloisInsertion (adjoin R : Set A → StarSubalgebra R A) (↑) where
   choice s hs := (adjoin R s).copy s <| le_antisymm (StarSubalgebra.gc.le_u_l s) hs
   gc := StarSubalgebra.gc
   le_l_u S := (StarSubalgebra.gc (S : Set A) (adjoin R S)).1 <| le_rfl

Mathlib/Analysis/Normed/Group/Hom.lean

@@ -156,10 +156,7 @@ theorem coe_toAddMonoidHom : ⇑f.toAddMonoidHom = f :=
 
 theorem toAddMonoidHom_injective :
     Function.Injective (@NormedAddGroupHom.toAddMonoidHom V₁ V₂ _ _) := fun f g h =>
-  coe_inj <|
-    show ⇑f.toAddMonoidHom = g by
-      rw [h]
-      rfl
+  coe_inj <| by rw [←coe_toAddMonoidHom f, ←coe_toAddMonoidHom g, h]
 #align normed_add_group_hom.to_add_monoid_hom_injective NormedAddGroupHom.toAddMonoidHom_injective
 
 @[simp]
@@ -257,14 +254,13 @@ theorem le_opNorm_of_le {c : ℝ} {x} (h : ‖x‖ ≤ c) : ‖f x‖ ≤ ‖f
   le_trans (f.le_opNorm x) (mul_le_mul_of_nonneg_left h f.opNorm_nonneg)
 #align normed_add_group_hom.le_op_norm_of_le NormedAddGroupHom.le_opNorm_of_le
 
-theorem le_of_op_norm_le {c : ℝ} (h : ‖f‖ ≤ c) (x : V₁) : ‖f x‖ ≤ c * ‖x‖ :=
+theorem le_of_opNorm_le {c : ℝ} (h : ‖f‖ ≤ c) (x : V₁) : ‖f x‖ ≤ c * ‖x‖ :=
   (f.le_opNorm x).trans (mul_le_mul_of_nonneg_right h (norm_nonneg x))
-#align normed_add_group_hom.le_of_op_norm_le NormedAddGroupHom.le_of_op_norm_le
+#align normed_add_group_hom.le_of_op_norm_le NormedAddGroupHom.le_of_opNorm_le
 
 /-- continuous linear maps are Lipschitz continuous. -/
 theorem lipschitz : LipschitzWith ⟨‖f‖, opNorm_nonneg f⟩ f :=
-  LipschitzWith.of_dist_le_mul fun x y =>
-    by
+  LipschitzWith.of_dist_le_mul fun x y => by
     rw [dist_eq_norm, dist_eq_norm, ← map_sub]
     apply le_opNorm
 #align normed_add_group_hom.lipschitz NormedAddGroupHom.lipschitz
@@ -481,8 +477,7 @@ theorem opNorm_neg (f : NormedAddGroupHom V₁ V₂) : ‖-f‖ = ‖f‖ := by
 instance sub : Sub (NormedAddGroupHom V₁ V₂) :=
   ⟨fun f g =>
     { f.toAddMonoidHom - g.toAddMonoidHom with
-      bound' :=
-        by
+      bound' := by
         simp only [AddMonoidHom.sub_apply, AddMonoidHom.toFun_eq_coe, sub_eq_add_neg]
         exact (f + -g).bound' }⟩
 
@@ -503,11 +498,11 @@ theorem sub_apply (f g : NormedAddGroupHom V₁ V₂) (v : V₁) :
 section SMul
 
 variable {R R' : Type _} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R]
-  [BoundedSmul R V₂] [MonoidWithZero R'] [DistribMulAction R' V₂] [PseudoMetricSpace R']
-  [BoundedSmul R' V₂]
+  [BoundedSMul R V₂] [MonoidWithZero R'] [DistribMulAction R' V₂] [PseudoMetricSpace R']
+  [BoundedSMul R' V₂]
 
-instance smul : SMul R (NormedAddGroupHom V₁ V₂)
-    where smul r f :=
+instance smul : SMul R (NormedAddGroupHom V₁ V₂) where
+  smul r f :=
     { toFun := r • ⇑f
       map_add' := (r • f.toAddMonoidHom).map_add'
       bound' :=
@@ -544,16 +539,16 @@ instance isCentralScalar [DistribMulAction Rᵐᵒᵖ V₂] [IsCentralScalar R V
 
 end SMul
 
-instance natSMul : SMul ℕ (NormedAddGroupHom V₁ V₂)
-    where smul n f :=
+instance nsmul : SMul ℕ (NormedAddGroupHom V₁ V₂) where
+  smul n f :=
     { toFun := n • ⇑f
       map_add' := (n • f.toAddMonoidHom).map_add'
       bound' :=
         let ⟨b, hb⟩ := f.bound'
         ⟨n • b, fun v => by
           rw [Pi.smul_apply, nsmul_eq_mul, mul_assoc]
           exact (norm_nsmul_le _ _).trans (mul_le_mul_of_nonneg_left (hb _) (Nat.cast_nonneg _))⟩ }
-#align normed_add_group_hom.has_nat_scalar NormedAddGroupHom.natSMul
+#align normed_add_group_hom.has_nat_scalar NormedAddGroupHom.nsmul
 
 @[simp]
 theorem coe_nsmul (r : ℕ) (f : NormedAddGroupHom V₁ V₂) : ⇑(r • f) = r • ⇑f :=
@@ -565,7 +560,7 @@ theorem nsmul_apply (r : ℕ) (f : NormedAddGroupHom V₁ V₂) (v : V₁) : (r
   rfl
 #align normed_add_group_hom.nsmul_apply NormedAddGroupHom.nsmul_apply
 
-instance intSMul : SMul ℤ (NormedAddGroupHom V₁ V₂) where
+instance zsmul : SMul ℤ (NormedAddGroupHom V₁ V₂) where
   smul z f :=
     { toFun := z • ⇑f
       map_add' := (z • f.toAddMonoidHom).map_add'
@@ -574,7 +569,7 @@ instance intSMul : SMul ℤ (NormedAddGroupHom V₁ V₂) where
         ⟨‖z‖ • b, fun v => by
           rw [Pi.smul_apply, smul_eq_mul, mul_assoc]
           exact (norm_zsmul_le _ _).trans (mul_le_mul_of_nonneg_left (hb _) <| norm_nonneg _)⟩ }
-#align normed_add_group_hom.has_int_scalar NormedAddGroupHom.intSMul
+#align normed_add_group_hom.has_int_scalar NormedAddGroupHom.zsmul
 
 @[simp]
 theorem coe_zsmul (r : ℤ) (f : NormedAddGroupHom V₁ V₂) : ⇑(r • f) = r • ⇑f :=
@@ -618,8 +613,7 @@ instance toNormedAddCommGroup {V₁ V₂ : Type _} [NormedAddCommGroup V₁] [No
 
 /-- Coercion of a `NormedAddGroupHom` is an `AddMonoidHom`. Similar to `AddMonoidHom.coeFn`.  -/
 @[simps]
-def coeAddHom : NormedAddGroupHom V₁ V₂ →+ V₁ → V₂
-    where
+def coeAddHom : NormedAddGroupHom V₁ V₂ →+ V₁ → V₂ where
   toFun := FunLike.coe
   map_zero' := coe_zero
   map_add' := coe_add
@@ -639,10 +633,10 @@ theorem sum_apply {ι : Type _} (s : Finset ι) (f : ι → NormedAddGroupHom V
 
 
 instance distribMulActoin {R : Type _} [MonoidWithZero R] [DistribMulAction R V₂]
-    [PseudoMetricSpace R] [BoundedSmul R V₂] : DistribMulAction R (NormedAddGroupHom V₁ V₂) :=
+    [PseudoMetricSpace R] [BoundedSMul R V₂] : DistribMulAction R (NormedAddGroupHom V₁ V₂) :=
   Function.Injective.distribMulAction coeAddHom coe_injective coe_smul
 
-instance module {R : Type _} [Semiring R] [Module R V₂] [PseudoMetricSpace R] [BoundedSmul R V₂] :
+instance module {R : Type _} [Semiring R] [Module R V₂] [PseudoMetricSpace R] [BoundedSMul R V₂] :
     Module R (NormedAddGroupHom V₁ V₂) :=
   Function.Injective.module _ coeAddHom coe_injective coe_smul
 
@@ -726,14 +720,10 @@ variable {V W V₁ V₂ V₃ : Type _} [SeminormedAddCommGroup V] [SeminormedAdd
 
 /-- The inclusion of an `AddSubgroup`, as bounded group homomorphism. -/
 @[simps!]
-def incl (s : AddSubgroup V) : NormedAddGroupHom s V
-    where
+def incl (s : AddSubgroup V) : NormedAddGroupHom s V where
   toFun := (Subtype.val : s → V)
   map_add' v w := AddSubgroup.coe_add _ _ _
-  bound' :=
-    ⟨1, fun v => by
-      rw [one_mul]
-      rfl⟩
+  bound' := ⟨1, fun v => by rw [one_mul, AddSubgroup.coe_norm]⟩
 #align normed_add_group_hom.incl NormedAddGroupHom.incl
 
 theorem norm_incl {V' : AddSubgroup V} (x : V') : ‖incl _ x‖ = ‖x‖ :=
@@ -754,24 +744,15 @@ def ker : AddSubgroup V₁ :=
 #align normed_add_group_hom.ker NormedAddGroupHom.ker
 
 theorem mem_ker (v : V₁) : v ∈ f.ker ↔ f v = 0 := by
-  erw [f.toAddMonoidHom.mem_ker]
-  rfl
+  erw [f.toAddMonoidHom.mem_ker, coe_toAddMonoidHom]
 #align normed_add_group_hom.mem_ker NormedAddGroupHom.mem_ker
 
 /-- Given a normed group hom `f : V₁ → V₂` satisfying `g.comp f = 0` for some `g : V₂ → V₃`,
     the corestriction of `f` to the kernel of `g`. -/
 @[simps]
-def ker.lift (h : g.comp f = 0) : NormedAddGroupHom V₁ g.ker
-    where
-  toFun v :=
-    ⟨f v, by
-      erw [g.mem_ker]
-      show (g.comp f) v = 0
-      rw [h]
-      rfl⟩
-  map_add' v w := by
-    simp only [map_add]
-    rfl
+def ker.lift (h : g.comp f = 0) : NormedAddGroupHom V₁ g.ker where
+  toFun v := ⟨f v, by rw [g.mem_ker, ←comp_apply g f, h, zero_apply]⟩
+  map_add' v w := by simp only [map_add, AddSubmonoid.mk_add_mk]
   bound' := f.bound'
 #align normed_add_group_hom.ker.lift NormedAddGroupHom.ker.lift
 
@@ -849,7 +830,7 @@ theorem normNoninc_iff_norm_le_one : f.NormNoninc ↔ ‖f‖ ≤ 1 := by
   refine' ⟨fun h => _, fun h => fun v => _⟩
   · refine' opNorm_le_bound _ zero_le_one fun v => _
     simpa [one_mul] using h v
-  · simpa using le_of_op_norm_le f h v
+  · simpa using le_of_opNorm_le f h v
 #align normed_add_group_hom.norm_noninc.norm_noninc_iff_norm_le_one NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one
 
 theorem zero : (0 : NormedAddGroupHom V₁ V₂).NormNoninc := fun v => by simp

Mathlib/CategoryTheory/Category/Pointed.lean

@@ -57,9 +57,9 @@ theorem coe_of {X : Type _} (point : X) : ↥(of point) = X :=
 set_option linter.uppercaseLean3 false in
 #align Pointed.coe_of Pointed.coe_of
 
-alias of ← _root_.prod.Pointed
+alias of ← _root_.Prod.Pointed
 set_option linter.uppercaseLean3 false in
-#align prod.Pointed prod.Pointed
+#align prod.Pointed Prod.Pointed
 
 instance : Inhabited Pointed :=
   ⟨of ((), ())⟩
@@ -114,8 +114,7 @@ set_option linter.uppercaseLean3 false in
 /-- Constructs a isomorphism between pointed types from an equivalence that preserves the point
 between them. -/
 @[simps]
-def Iso.mk {α β : Pointed} (e : α ≃ β) (he : e α.point = β.point) : α ≅ β
-    where
+def Iso.mk {α β : Pointed} (e : α ≃ β) (he : e α.point = β.point) : α ≅ β where
   hom := ⟨e, he⟩
   inv := ⟨e.symm, e.symm_apply_eq.2 he.symm⟩
   hom_inv_id := Pointed.Hom.ext _ _ e.symm_comp_self

Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

@@ -508,7 +508,7 @@ open ZeroObject
 `X` and `Y` are isomorphic to the zero object.
 -/
 def isIsoZeroEquivIsoZero (X Y : C) : IsIso (0 : X ⟶ Y) ≃ (X ≅ 0) × (Y ≅ 0) := by
-  -- This is lame, because `prod` can't cope with `Prop`, so we can't use `equiv.prod_congr`.
+  -- This is lame, because `prod` can't cope with `Prop`, so we can't use `Equiv.prodCongr`.
   refine' (isIsoZeroEquiv X Y).trans _
   symm
   fconstructor
@@ -590,8 +590,7 @@ def monoFactorisationZero (X Y : C) : MonoFactorisation (0 : X ⟶ Y)  where
 
 /-- The factorisation through the zero object is an image factorisation.
 -/
-def imageFactorisationZero (X Y : C) : ImageFactorisation (0 : X ⟶ Y)
-    where
+def imageFactorisationZero (X Y : C) : ImageFactorisation (0 : X ⟶ Y) where
   F := monoFactorisationZero X Y
   isImage := { lift := fun F' => 0 }
 #align category_theory.limits.image_factorisation_zero CategoryTheory.Limits.imageFactorisationZero

Mathlib/CategoryTheory/Monoidal/End.lean

@@ -33,10 +33,9 @@ variable (C : Type u) [Category.{v} C]
 with tensor product given by composition of functors
 (and horizontal composition of natural transformations).
 -/
-def endofunctorMonoidalCategory : MonoidalCategory (C ⥤ C)
-    where
+def endofunctorMonoidalCategory : MonoidalCategory (C ⥤ C) where
   tensorObj F G := F ⋙ G
-  tensorHom := @fun F G F' G' α β => α ◫ β
+  tensorHom α β := α ◫ β
   tensorUnit' := 𝟭 C
   associator F G H := Functor.associator F G H
   leftUnitor F := Functor.leftUnitor F
@@ -56,16 +55,15 @@ attribute [local instance] endofunctorMonoidalCategory
 def tensoringRightMonoidal [MonoidalCategory.{v} C] : MonoidalFunctor C (C ⥤ C) :=
   {-- We could avoid needing to do this explicitly by
       -- constructing a partially applied analogue of `associatorNatIso`.
-      tensoringRight
-      C with
+      tensoringRight C with
     ε := (rightUnitorNatIso C).inv
     μ := fun X Y =>
       { app := fun Z => (α_ Z X Y).hom
         naturality := fun Z Z' f => by
           dsimp [endofunctorMonoidalCategory]
           rw [associator_naturality]
           simp }
-    μ_natural := @fun X Y X' Y' f g => by
+    μ_natural := fun f g => by
       ext Z
       dsimp [endofunctorMonoidalCategory]
       simp only [← id_tensor_comp_tensor_id g f, id_tensor_comp, ← tensor_id, Category.assoc,
@@ -134,7 +132,7 @@ theorem μ_naturality {m n : M} {X Y : C} (f : X ⟶ Y) :
   (F.toLaxMonoidalFunctor.μ m n).naturality f
 #align category_theory.μ_naturality CategoryTheory.μ_naturality
 
--- This is a simp lemma in the reverse direction via `nat_trans.naturality`.
+-- This is a simp lemma in the reverse direction via `NatTrans.naturality`.
 @[reassoc]
 theorem μ_inv_naturality {m n : M} {X Y : C} (f : X ⟶ Y) :
     (F.μIso m n).inv.app X ≫ (F.obj n).map ((F.obj m).map f) =