chore: tidy various files (#21872)

Author: Ruben-VandeVelde

Mathlib/Algebra/Azumaya/Basic.lean

@@ -43,7 +43,7 @@ noncomputable abbrev tensorEquivEnd : R ⊗[R] Rᵐᵒᵖ ≃ₐ[R] Module.End R
   Algebra.TensorProduct.lid R Rᵐᵒᵖ|>.trans <|
   AlgEquiv.ofRingEquiv (f := Module.moduleEndSelf R) fun r ↦ by ext; simp
 
-lemma coe_tensorEquivEnd: tensorEquivEnd R = AlgHom.mulLeftRight R R := by
+lemma coe_tensorEquivEnd : tensorEquivEnd R = AlgHom.mulLeftRight R R := by
   ext; simp
 
 instance id : IsAzumaya R R where
@@ -63,7 +63,7 @@ End R A   ------------> End R B
           e.conj
 ```
 -/
-lemma mulLeftRight_comp_congr (e : A ≃ₐ[R] B):
+lemma mulLeftRight_comp_congr (e : A ≃ₐ[R] B) :
     (AlgHom.mulLeftRight R B).comp (Algebra.TensorProduct.congr e e.op).toAlgHom =
     (e.toLinearEquiv.algConj).toAlgHom.comp (AlgHom.mulLeftRight R A) := by
   apply AlgHom.ext
@@ -80,7 +80,7 @@ theorem of_AlgEquiv (e : A ≃ₐ[R] B) [IsAzumaya R A] : IsAzumaya R B :=
   let _ : Module.Finite R B := .equiv e.toLinearEquiv
   ⟨Function.Bijective.of_comp_iff (AlgHom.mulLeftRight R B)
     (Algebra.TensorProduct.congr e e.op).bijective |>.1 <| by
-    erw [← AlgHom.coe_comp, mulLeftRight_comp_congr]
+    rw [← AlgEquiv.coe_algHom, ← AlgHom.coe_comp, mulLeftRight_comp_congr]
     simp [AlgHom.mulLeftRight_bij]⟩
 
 end IsAzumaya

Mathlib/Algebra/Azumaya/Matrix.lean

@@ -35,7 +35,7 @@ abbrev AlgHom.mulLeftRightMatrix_inv :
   map_add' f1 f2 := by simp [add_smul, Finset.sum_add_distrib]
   map_smul' r f := by simp [MulAction.mul_smul, Finset.smul_sum]
 
-lemma AlgHom.mulLeftRightMatrix.inv_comp:
+lemma AlgHom.mulLeftRightMatrix.inv_comp :
     (AlgHom.mulLeftRightMatrix_inv R n).comp
     (AlgHom.mulLeftRight R (Matrix n n R)).toLinearMap = .id :=
   Basis.ext (Basis.tensorProduct (Matrix.stdBasis _ _ _)
@@ -44,13 +44,15 @@ lemma AlgHom.mulLeftRightMatrix.inv_comp:
     simp [stdBasis_eq_stdBasisMatrix, ite_and, Fintype.sum_prod_type,
       mulLeftRight_apply, stdBasisMatrix, Matrix.mul_apply]
 
-lemma AlgHom.mulLeftRightMatrix.comp_inv:
+lemma AlgHom.mulLeftRightMatrix.comp_inv :
     (AlgHom.mulLeftRight R (Matrix n n R)).toLinearMap.comp
     (AlgHom.mulLeftRightMatrix_inv R n) = .id := by
   ext f : 1
   apply Basis.ext (Matrix.stdBasis _ _ _)
   intro ⟨i, j⟩
-  simp [AlgHom.mulLeftRight_apply, stdBasis_eq_stdBasisMatrix]
+  simp only [LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, map_sum,
+    _root_.map_smul, stdBasis_eq_stdBasisMatrix, LinearMap.coeFn_sum, Finset.sum_apply,
+    LinearMap.smul_apply, LinearMap.id_coe, id_eq]
   ext k l
   simp [sum_apply, Matrix.mul_apply, Finset.sum_mul, Finset.mul_sum, stdBasisMatrix,
     Fintype.sum_prod_type, ite_and]

Mathlib/Algebra/Category/Ring/Adjunctions.lean

@@ -6,7 +6,6 @@ Authors: Kim Morrison, Johannes Hölzl, Andrew Yang
 import Mathlib.Algebra.Category.Ring.Colimits
 import Mathlib.Algebra.MvPolynomial.CommRing
 import Mathlib.CategoryTheory.Comma.Over.Pullback
--- import Mathlib.Algebra.Category.Mon
 
 /-!
 # Adjunctions in `CommRingCat`

Mathlib/Algebra/Central/Defs.lean

@@ -47,7 +47,7 @@ variable (k D : Type*) [Field k] [Ring D] [Algebra k D]
 variable [Algebra.IsCentral k D] [IsSimpleRing D]
 variable [FiniteDimensional k D]
 ```
-where `FiniteDimensional k D` is almost always assumed in most references, but some results does not
+where `FiniteDimensional k D` is almost always assumed in most references, but some results do not
 need this assumption.
 
 ## Tags

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -1217,7 +1217,7 @@ variable (G₀ : Type*) [CommGroupWithZero G₀] [DecidableEq G₀]
 instance (priority := 100) : NormalizedGCDMonoid G₀ where
   normUnit x := if h : x = 0 then 1 else (Units.mk0 x h)⁻¹
   normUnit_zero := dif_pos rfl
-  normUnit_mul := fun {x y} x0 y0 => Units.eq_iff.1 (by simp [x0, y0, mul_comm])
+  normUnit_mul {x y} x0 y0 := Units.eq_iff.1 (by simp [x0, y0, mul_comm])
   normUnit_coe_units u := by simp
   gcd a b := if a = 0 ∧ b = 0 then 0 else 1
   lcm a b := if a = 0 ∨ b = 0 then 0 else 1

Mathlib/Algebra/Group/Subgroup/Finite.lean

@@ -152,7 +152,6 @@ theorem card_le_of_le {H K : Subgroup G} [Finite K] (h : H ≤ K) : Nat.card H 
 theorem card_map_of_injective {H : Type*} [Group H] {K : Subgroup G} {f : G →* H}
     (hf : Function.Injective f) :
     Nat.card (map f K) = Nat.card K := by
-  -- simp only [← SetLike.coe_sort_coe]
   apply Nat.card_image_of_injective hf
 
 @[to_additive]

Mathlib/Algebra/Group/Submonoid/Basic.lean

@@ -50,8 +50,6 @@ submonoid, submonoids
 
 assert_not_exists MonoidWithZero
 
--- Only needed for notation
--- Only needed for notation
 variable {M : Type*} {N : Type*}
 variable {A : Type*}
 

Mathlib/Algebra/Lie/Abelian.lean

@@ -161,8 +161,8 @@ def maxTrivHom (f : M →ₗ⁅R,L⁆ N) : maxTrivSubmodule R L M →ₗ⁅R,L
   toFun m := ⟨f m, fun x =>
     (LieModuleHom.map_lie _ _ _).symm.trans <|
       (congr_arg f (m.property x)).trans (LieModuleHom.map_zero _)⟩
-  map_add' m n := by ext; simp [Function.comp_apply]
-  map_smul' t m := by ext; simp [Function.comp_apply]
+  map_add' m n := by ext; simp
+  map_smul' t m := by ext; simp
   map_lie' {x m} := by simp
 
 @[norm_cast, simp]

Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean

@@ -285,16 +285,15 @@ theorem le_trailingDegree_mul : p.trailingDegree + q.trailingDegree ≤ (p * q).
   obtain ⟨⟨i, j⟩, hij, hpq⟩ := exists_ne_zero_of_sum_ne_zero hn
   refine
     (add_le_add (min_le (mem_support_iff.mpr (left_ne_zero_of_mul hpq)))
-          (min_le (mem_support_iff.mpr (right_ne_zero_of_mul hpq)))).trans
-      (le_of_eq ?_)
+          (min_le (mem_support_iff.mpr (right_ne_zero_of_mul hpq)))).trans_eq ?_
   rwa [← WithTop.coe_add, WithTop.coe_eq_coe, ← mem_antidiagonal]
 
 theorem le_natTrailingDegree_mul (h : p * q ≠ 0) :
     p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree := by
   have hp : p ≠ 0 := fun hp => h (by rw [hp, zero_mul])
   have hq : q ≠ 0 := fun hq => h (by rw [hq, mul_zero])
-  have (p : R[X]) : WithTop.some (natTrailingDegree p) = Nat.cast (natTrailingDegree p) := rfl
-  rw [← WithTop.coe_le_coe, WithTop.coe_add, this p, this q, this (p * q),
+  rw [← WithTop.coe_le_coe, WithTop.coe_add, ← Nat.cast_withTop (natTrailingDegree p),
+    ← Nat.cast_withTop (natTrailingDegree q), ← Nat.cast_withTop (natTrailingDegree (p * q)),
     ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq,
     ← trailingDegree_eq_natTrailingDegree h]
   exact le_trailingDegree_mul
@@ -329,12 +328,10 @@ theorem natTrailingDegree_mul' (h : p.trailingCoeff * q.trailingCoeff ≠ 0) :
     (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree := by
   have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
   have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
-  have aux1 n : Nat.cast n = WithTop.some (n) := rfl
-  have aux2 (p : R[X]) : WithTop.some (natTrailingDegree p) = Nat.cast (natTrailingDegree p) := rfl
   apply natTrailingDegree_eq_of_trailingDegree_eq_some
-  rw [trailingDegree_mul' h, aux1 (natTrailingDegree p + natTrailingDegree q),
-    WithTop.coe_add, aux2 p, aux2 q, ← trailingDegree_eq_natTrailingDegree hp, ←
-    trailingDegree_eq_natTrailingDegree hq]
+  rw [trailingDegree_mul' h, Nat.cast_withTop (natTrailingDegree p + natTrailingDegree q),
+    WithTop.coe_add, ← Nat.cast_withTop, ← Nat.cast_withTop,
+    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]
 
 theorem natTrailingDegree_mul [NoZeroDivisors R] (hp : p ≠ 0) (hq : q ≠ 0) :
     (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree :=

Mathlib/Algebra/Polynomial/Expand.lean

@@ -133,9 +133,7 @@ theorem natDegree_expand (p : ℕ) (f : R[X]) : (expand R p f).natDegree = f.nat
   by_cases hf : f = 0
   · rw [hf, map_zero, natDegree_zero, zero_mul]
   have hf1 : expand R p f ≠ 0 := mt (expand_eq_zero hp).1 hf
-  rw [← WithBot.coe_eq_coe]
-  convert (degree_eq_natDegree hf1).symm
-  symm
+  rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hf1]
   refine le_antisymm ((degree_le_iff_coeff_zero _ _).2 fun n hn => ?_) ?_
   · rw [coeff_expand hp]
     split_ifs with hpn