chore: tidy various files (#4466)

Mathlib/Algebra/DirectSum/Internal.lean

@@ -15,8 +15,8 @@ import Mathlib.Algebra.DirectSum.Algebra
 /-!
 # Internally graded rings and algebras
 
-This module provides `gsemiring` and `gcomm_semiring` instances for a collection of subobjects `A`
-when a `SetLike.GradedMonoid` instance is available:
+This module provides `DirectSum.GSemiring` and `DirectSum.GCommSemiring` instances for a collection
+of subobjects `A` when a `SetLike.GradedMonoid` instance is available:
 
 * `SetLike.gnonUnitalNonAssocSemiring`
 * `SetLike.gsemiring`
@@ -26,7 +26,7 @@ With these instances in place, it provides the bundled canonical maps out of a d
 subobjects into their carrier type:
 
 * `DirectSum.coeRingHom` (a `RingHom` version of `DirectSum.coeAddMonoidHom`)
-* `DirectSum.coeAlgHom` (an `AlgHom` version of `direct_sum.submodule_coe`)
+* `DirectSum.coeAlgHom` (an `AlgHom` version of `DirectSum.coeLinearMap`)
 
 Strictly the definitions in this file are not sufficient to fully define an "internal" direct sum;
 to represent this case, `(h : DirectSum.IsInternal A) [SetLike.GradedMonoid A]` is
@@ -36,7 +36,7 @@ needed. In the future there will likely be a data-carrying, constructive, typecl
 When `CompleteLattice.Independent (Set.range A)` (a weaker condition than
 `DirectSum.IsInternal A`), these provide a grading of `⨆ i, A i`, and the
 mapping `⨁ i, A i →+ ⨆ i, A i` can be obtained as
-`direct_sum.to_monoid (λ i, AddSubmonoid.inclusion $ le_iSup A i)`.
+`DirectSum.toAddMonoid (λ i, AddSubmonoid.inclusion $ le_iSup A i)`.
 
 ## tags
 
@@ -89,25 +89,22 @@ variable [DecidableEq ι]
 
 namespace SetLike
 
-/-- Build a `gnon_unital_non_assoc_semiring` instance for a collection of additive submonoids. -/
+/-- Build a `DirectSum.GNonUnitalNonAssocSemiring` instance for a collection of additive
+submonoids. -/
 instance gnonUnitalNonAssocSemiring [Add ι] [NonUnitalNonAssocSemiring R] [SetLike σ R]
     [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedMul A] :
     DirectSum.GNonUnitalNonAssocSemiring fun i => A i :=
-  {
-    SetLike.gMul
-      A with
+  { SetLike.gMul A with
     mul_zero := fun _ => Subtype.ext (MulZeroClass.mul_zero _)
     zero_mul := fun _ => Subtype.ext (MulZeroClass.zero_mul _)
     mul_add := fun _ _ _ => Subtype.ext (mul_add _ _ _)
     add_mul := fun _ _ _ => Subtype.ext (add_mul _ _ _) }
 #align set_like.gnon_unital_non_assoc_semiring SetLike.gnonUnitalNonAssocSemiring
 
-/-- Build a `gsemiring` instance for a collection of additive submonoids. -/
+/-- Build a `DirectSum.GSemiring` instance for a collection of additive submonoids. -/
 instance gsemiring [AddMonoid ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ)
     [SetLike.GradedMonoid A] : DirectSum.GSemiring fun i => A i :=
-  {
-    SetLike.gMonoid
-      A with
+  { SetLike.gMonoid A with
     mul_zero := fun _ => Subtype.ext (MulZeroClass.mul_zero _)
     zero_mul := fun _ => Subtype.ext (MulZeroClass.zero_mul _)
     mul_add := fun _ _ _ => Subtype.ext (mul_add _ _ _)
@@ -117,24 +114,22 @@ instance gsemiring [AddMonoid ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass
     natCast_succ := fun n => Subtype.ext (Nat.cast_succ n) }
 #align set_like.gsemiring SetLike.gsemiring
 
-/-- Build a `gcomm_semiring` instance for a collection of additive submonoids. -/
+/-- Build a `DirectSum.GCommSemiring` instance for a collection of additive submonoids. -/
 instance gcommSemiring [AddCommMonoid ι] [CommSemiring R] [SetLike σ R] [AddSubmonoidClass σ R]
     (A : ι → σ) [SetLike.GradedMonoid A] : DirectSum.GCommSemiring fun i => A i :=
   { SetLike.gCommMonoid A, SetLike.gsemiring A with }
 #align set_like.gcomm_semiring SetLike.gcommSemiring
 
-/-- Build a `gring` instance for a collection of additive subgroups. -/
+/-- Build a `DirectSum.GRing` instance for a collection of additive subgroups. -/
 instance gring [AddMonoid ι] [Ring R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ)
     [SetLike.GradedMonoid A] : DirectSum.GRing fun i => A i :=
-  {
-    SetLike.gsemiring
-      A with
+  { SetLike.gsemiring A with
     intCast := fun z => ⟨z, SetLike.int_cast_mem_graded _ _⟩
     intCast_ofNat := fun _n => Subtype.ext <| Int.cast_ofNat _
     intCast_negSucc_ofNat := fun n => Subtype.ext <| Int.cast_negSucc n }
 #align set_like.gring SetLike.gring
 
-/-- Build a `gcomm_semiring` instance for a collection of additive submonoids. -/
+/-- Build a `DirectSum.GCommRing` instance for a collection of additive submonoids. -/
 instance gcommRing [AddCommMonoid ι] [CommRing R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ)
     [SetLike.GradedMonoid A] : DirectSum.GCommRing fun i => A i :=
   { SetLike.gCommMonoid A, SetLike.gring A with }
@@ -165,9 +160,8 @@ theorem coe_mul_apply [AddMonoid ι] [SetLike.GradedMonoid A]
     ((r * r') n : R) =
       ∑ ij in (r.support ×ˢ r'.support).filter (fun ij : ι × ι => ij.1 + ij.2 = n),
         (r ij.1 * r' ij.2 : R) := by
-    rw [mul_eq_sum_support_ghas_mul, Dfinsupp.finset_sum_apply, AddSubmonoidClass.coe_finset_sum]
-    simp_rw [coe_of_apply, apply_ite, ZeroMemClass.coe_zero, ← Finset.sum_filter, SetLike.coe_gMul]
-
+  rw [mul_eq_sum_support_ghas_mul, Dfinsupp.finset_sum_apply, AddSubmonoidClass.coe_finset_sum]
+  simp_rw [coe_of_apply, apply_ite, ZeroMemClass.coe_zero, ← Finset.sum_filter, SetLike.coe_gMul]
 #align direct_sum.coe_mul_apply DirectSum.coe_mul_apply
 
 theorem coe_mul_apply_eq_dfinsupp_sum [AddMonoid ι] [SetLike.GradedMonoid A]
@@ -176,7 +170,8 @@ theorem coe_mul_apply_eq_dfinsupp_sum [AddMonoid ι] [SetLike.GradedMonoid A]
       else 0 := by
   rw [mul_eq_dfinsupp_sum]
   iterate 2 rw [Dfinsupp.sum_apply, Dfinsupp.sum, AddSubmonoidClass.coe_finset_sum]; congr; ext
-  dsimp only; split_ifs with h
+  dsimp only
+  split_ifs with h
   · subst h
     rw [of_eq_same]
     rfl
@@ -273,13 +268,13 @@ theorem coe_of_mul_apply_of_le {i : ι} (r : A i) (r' : ⨁ i, A i) (n : ι) (h
 theorem coe_mul_of_apply (r : ⨁ i, A i) {i : ι} (r' : A i) (n : ι) [Decidable (i ≤ n)] :
     ((r * of (fun i => A i) i r') n : R) = if i ≤ n then (r (n - i) : R) * r' else 0 := by
   split_ifs with h
-  exacts[coe_mul_of_apply_of_le _ _ _ n h, coe_mul_of_apply_of_not_le _ _ _ n h]
+  exacts [coe_mul_of_apply_of_le _ _ _ n h, coe_mul_of_apply_of_not_le _ _ _ n h]
 #align direct_sum.coe_mul_of_apply DirectSum.coe_mul_of_apply
 
 theorem coe_of_mul_apply {i : ι} (r : A i) (r' : ⨁ i, A i) (n : ι) [Decidable (i ≤ n)] :
     ((of (fun i => A i) i r * r') n : R) = if i ≤ n then (r * r' (n - i) : R) else 0 := by
   split_ifs with h
-  exacts[coe_of_mul_apply_of_le _ _ _ n h, coe_of_mul_apply_of_not_le _ _ _ n h]
+  exacts [coe_of_mul_apply_of_le _ _ _ n h, coe_of_mul_apply_of_not_le _ _ _ n h]
 #align direct_sum.coe_of_mul_apply DirectSum.coe_of_mul_apply
 
 end CanonicallyOrderedAddMonoid
@@ -291,7 +286,7 @@ end DirectSum
 
 namespace Submodule
 
-/-- Build a `galgebra` instance for a collection of `Submodule`s. -/
+/-- Build a `DirectSum.GAlgebra` instance for a collection of `Submodule`s. -/
 instance galgebra [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R] (A : ι → Submodule S R)
     [SetLike.GradedMonoid A] : DirectSum.GAlgebra S fun i => A i where
   toFun :=

Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

@@ -50,8 +50,7 @@ theorem continuous_reflTransSymmAux : Continuous reflTransSymmAux := by
   · continuity
   · continuity
   · continuity
-  · -- Porting note: was `continuity`
-    refine Continuous.mul ?_ (Continuous.sub ?_ ?_) <;> continuity
+  · continuity
   intro x hx
   -- Porting note: norm_num ignores arguments.
   rw [hx, mul_assoc]
@@ -365,13 +364,8 @@ def fundamentalGroupoidFunctor : TopCat ⥤ CategoryTheory.Grpd where
     rfl
 #align fundamental_groupoid.fundamental_groupoid_functor FundamentalGroupoid.fundamentalGroupoidFunctor
 
--- mathport name: fundamental_groupoid_functor
 scoped notation "π" => FundamentalGroupoid.fundamentalGroupoidFunctor
-
--- mathport name: fundamental_groupoid_functor.obj
 scoped notation "πₓ" => FundamentalGroupoid.fundamentalGroupoidFunctor.obj
-
--- mathport name: fundamental_groupoid_functor.map
 scoped notation "πₘ" => FundamentalGroupoid.fundamentalGroupoidFunctor.map
 
 theorem map_eq {X Y : TopCat} {x₀ x₁ : X} (f : C(X, Y)) (p : Path.Homotopic.Quotient x₀ x₁) :

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

@@ -564,7 +564,7 @@ def ContinuousLinearEquiv.piRing (ι : Type _) [Fintype ι] [DecidableEq ι] :
       rw [← nsmul_eq_mul]
       refine op_norm_le_bound _ (nsmul_nonneg (norm_nonneg g) (Fintype.card ι)) fun t => ?_
       simp_rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply,
-        LinearMap.coe_to_continuous_linear_map', LinearEquiv.piRing_symm_apply]
+        LinearMap.coe_toContinuousLinearMap', LinearEquiv.piRing_symm_apply]
       apply le_trans (norm_sum_le _ _)
       rw [smul_mul_assoc]
       refine' Finset.sum_le_card_nsmul _ _ _ fun i _ => _

Mathlib/CategoryTheory/Abelian/Projective.lean

@@ -16,19 +16,15 @@ import Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
 /-!
 # Abelian categories with enough projectives have projective resolutions
 
-When `C` is abelian `projective.d f` and `f` are exact.
+When `C` is abelian `Projective.d f` and `f` are exact.
 Hence, starting from an epimorphism `P ⟶ X`, where `P` is projective,
-we can apply `projective.d` repeatedly to obtain a projective resolution of `X`.
+we can apply `Projective.d` repeatedly to obtain a projective resolution of `X`.
 -/
 
 
 noncomputable section
 
-open CategoryTheory
-
-open CategoryTheory.Limits
-
-open Opposite
+open CategoryTheory CategoryTheory.Limits Opposite
 
 universe v u v' u'
 
@@ -38,8 +34,7 @@ open CategoryTheory.Projective
 
 variable {C : Type u} [Category.{v} C] [Abelian C]
 
-/-- When `C` is abelian, `projective.d f` and `f` are exact.
--/
+/-- When `C` is abelian, `Projective.d f` and `f` are exact. -/
 theorem exact_d_f [EnoughProjectives C] {X Y : C} (f : X ⟶ Y) : Exact (d f) f :=
   (Abelian.exact_iff _ _).2 <|
     ⟨by simp, zero_of_epi_comp (π _) <| by rw [← Category.assoc, cokernel.condition]⟩
@@ -67,11 +62,11 @@ namespace ProjectiveResolution
 
 /-!
 Our goal is to define `ProjectiveResolution.of Z : ProjectiveResolution Z`.
-The `0`-th object in this resolution will just be `projective.over Z`,
+The `0`-th object in this resolution will just be `Projective.over Z`,
 i.e. an arbitrarily chosen projective object with a map to `Z`.
-After that, we build the `n+1`-st object as `projective.syzygies`
+After that, we build the `n+1`-st object as `Projective.syzygies`
 applied to the previously constructed morphism,
-and the map to the `n`-th object as `projective.d`.
+and the map to the `n`-th object as `Projective.d`.
 -/
 
 

Mathlib/Geometry/Euclidean/Sphere/Basic.lean

@@ -78,8 +78,8 @@ theorem Sphere.mk_center_radius (s : Sphere P) : (⟨s.center, s.radius⟩ : Sph
 
 /- Porting note: is a syntactic tautology
 theorem Sphere.coe_def (s : Sphere P) : (s : Set P) = Metric.sphere s.center s.radius :=
-  rfl
-#align euclidean_geometry.sphere.coe_def EuclideanGeometry.Sphere.coe_def -/
+  rfl -/
+#noalign euclidean_geometry.sphere.coe_def
 
 @[simp]
 theorem Sphere.coe_mk (c : P) (r : ℝ) : ↑(⟨c, r⟩ : Sphere P) = Metric.sphere c r :=

Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

@@ -35,9 +35,7 @@ noncomputable section
 
 universe u v w z
 
-open Polynomial Matrix
-
-open BigOperators Polynomial
+open Polynomial Matrix BigOperators
 
 variable {R : Type u} [CommRing R]
 
@@ -54,8 +52,9 @@ theorem charmatrix_apply_natDegree [Nontrivial R] (i j : n) :
   by_cases i = j <;> simp [h, ← degree_eq_iff_natDegree_eq_of_pos (Nat.succ_pos 0)]
 #align charmatrix_apply_nat_degree charmatrix_apply_natDegree
 
-theorem charmatrix_apply_natDegree_le (i j : n) : (charmatrix M i j).natDegree ≤ ite (i = j) 1 0 :=
-  by split_ifs with h <;> simp [h, natDegree_X_sub_C_le]
+theorem charmatrix_apply_natDegree_le (i j : n) :
+    (charmatrix M i j).natDegree ≤ ite (i = j) 1 0 := by
+  split_ifs with h <;> simp [h, natDegree_X_sub_C_le]
 #align charmatrix_apply_nat_degree_le charmatrix_apply_natDegree_le
 
 namespace Matrix
@@ -68,21 +67,25 @@ theorem charpoly_sub_diagonal_degree_lt :
     sum_insert (not_mem_erase (Equiv.refl n) univ), add_comm]
   simp only [charmatrix_apply_eq, one_mul, Equiv.Perm.sign_refl, id.def, Int.cast_one,
     Units.val_one, add_sub_cancel, Equiv.coe_refl]
-  rw [← mem_degreeLT]; apply Submodule.sum_mem (degreeLT R (Fintype.card n - 1))
+  rw [← mem_degreeLT]
+  apply Submodule.sum_mem (degreeLT R (Fintype.card n - 1))
   intro c hc; rw [← C_eq_int_cast, C_mul']
   apply Submodule.smul_mem (degreeLT R (Fintype.card n - 1)) ↑↑(Equiv.Perm.sign c)
-  rw [mem_degreeLT]; apply lt_of_le_of_lt degree_le_natDegree _
+  rw [mem_degreeLT]
+  apply lt_of_le_of_lt degree_le_natDegree _
   rw [Nat.cast_withBot, Nat.cast_withBot] -- porting note: added
   rw [WithBot.coe_lt_coe]
   apply lt_of_le_of_lt _ (Equiv.Perm.fixed_point_card_lt_of_ne_one (ne_of_mem_erase hc))
   apply le_trans (Polynomial.natDegree_prod_le univ fun i : n => charmatrix M (c i) i) _
   rw [card_eq_sum_ones]; rw [sum_filter]; apply sum_le_sum
-  intros ; apply charmatrix_apply_natDegree_le
+  intros
+  apply charmatrix_apply_natDegree_le
 #align matrix.charpoly_sub_diagonal_degree_lt Matrix.charpoly_sub_diagonal_degree_lt
 
 theorem charpoly_coeff_eq_prod_coeff_of_le {k : ℕ} (h : Fintype.card n - 1 ≤ k) :
     M.charpoly.coeff k = (∏ i : n, (X - C (M i i))).coeff k := by
-  apply eq_of_sub_eq_zero; rw [← coeff_sub]; apply Polynomial.coeff_eq_zero_of_degree_lt
+  apply eq_of_sub_eq_zero; rw [← coeff_sub]
+  apply Polynomial.coeff_eq_zero_of_degree_lt
   apply lt_of_lt_of_le (charpoly_sub_diagonal_degree_lt M) ?_
   rw [Nat.cast_withBot, Nat.cast_withBot] -- porting note: added
   rw [WithBot.coe_le_coe]; apply h
@@ -97,7 +100,7 @@ theorem det_of_card_zero (h : Fintype.card n = 0) (M : Matrix n n R) : M.det = 1
 
 theorem charpoly_degree_eq_dim [Nontrivial R] (M : Matrix n n R) :
     M.charpoly.degree = Fintype.card n := by
-  by_cases Fintype.card n = 0
+  by_cases h : Fintype.card n = 0
   · rw [h]
     unfold charpoly
     rw [det_of_card_zero]
@@ -106,13 +109,9 @@ theorem charpoly_degree_eq_dim [Nontrivial R] (M : Matrix n n R) :
   rw [← sub_add_cancel M.charpoly (∏ i : n, (X - C (M i i)))]
   -- porting note: added `↑` in front of `Fintype.card n`
   have h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n) := by
-    rw [degree_eq_iff_natDegree_eq_of_pos]
-    swap
-    apply Nat.pos_of_ne_zero h
-    rw [natDegree_prod']
+    rw [degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_ne_zero h), natDegree_prod']
     simp_rw [natDegree_X_sub_C]
-    unfold Fintype.card
-    simp
+    rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]
     simp_rw [(monic_X_sub_C _).leadingCoeff]
     simp
   rw [degree_add_eq_right_of_degree_lt]
@@ -133,16 +132,15 @@ theorem charpoly_natDegree_eq_dim [Nontrivial R] (M : Matrix n n R) :
 
 theorem charpoly_monic (M : Matrix n n R) : M.charpoly.Monic := by
   nontriviality R -- porting note: was simply `nontriviality`
-  by_cases Fintype.card n = 0
+  by_cases h : Fintype.card n = 0
   · rw [charpoly, det_of_card_zero h]
     apply monic_one
   have mon : (∏ i : n, (X - C (M i i))).Monic := by
     apply monic_prod_of_monic univ fun i : n => X - C (M i i)
     simp [monic_X_sub_C]
   rw [← sub_add_cancel (∏ i : n, (X - C (M i i))) M.charpoly] at mon
   rw [Monic] at *
-  rw [leadingCoeff_add_of_degree_lt] at mon
-  rw [← mon]
+  rwa [leadingCoeff_add_of_degree_lt] at mon
   rw [charpoly_degree_eq_dim]
   rw [← neg_sub]
   rw [degree_neg]
@@ -156,13 +154,12 @@ theorem charpoly_monic (M : Matrix n n R) : M.charpoly.Monic := by
 
 theorem trace_eq_neg_charpoly_coeff [Nonempty n] (M : Matrix n n R) :
     trace M = -M.charpoly.coeff (Fintype.card n - 1) := by
-  rw [charpoly_coeff_eq_prod_coeff_of_le]; swap; rfl
-  rw [Fintype.card, prod_X_sub_C_coeff_card_pred univ (fun i : n => M i i) Fintype.card_pos,
-    neg_neg, trace]
-  rfl
+  rw [charpoly_coeff_eq_prod_coeff_of_le _ le_rfl, Fintype.card,
+    prod_X_sub_C_coeff_card_pred univ (fun i : n => M i i) Fintype.card_pos, neg_neg, trace]
+  simp_rw [diag_apply]
 #align matrix.trace_eq_neg_charpoly_coeff Matrix.trace_eq_neg_charpoly_coeff
 
--- I feel like this should use polynomial.alg_hom_eval₂_algebra_map
+-- I feel like this should use `Polynomial.algHom_eval₂_algebraMap`
 theorem matPolyEquiv_eval (M : Matrix n n R[X]) (r : R) (i j : n) :
     (matPolyEquiv M).eval ((scalar n) r) i j = (M i j).eval r := by
   unfold Polynomial.eval
@@ -188,8 +185,11 @@ theorem matPolyEquiv_eval (M : Matrix n n R[X]) (r : R) (i j : n) :
 theorem eval_det (M : Matrix n n R[X]) (r : R) :
     Polynomial.eval r M.det = (Polynomial.eval (scalar n r) (matPolyEquiv M)).det := by
   rw [Polynomial.eval, ← coe_eval₂RingHom, RingHom.map_det]
-  apply congr_arg det; ext; symm; exact matPolyEquiv_eval _ _ _ _
-                                  -- porting note: `exact` was `convert`
+  apply congr_arg det
+  ext
+  symm
+  -- porting note: `exact` was `convert`
+  exact matPolyEquiv_eval _ _ _ _
 #align matrix.eval_det Matrix.eval_det
 
 theorem det_eq_sign_charpoly_coeff (M : Matrix n n R) :