chore: tidy various files (#24331)

Author: Ruben-VandeVelde

Mathlib/Algebra/Algebra/Operations.lean

@@ -523,12 +523,11 @@ theorem mem_span_mul_finite_of_mem_mul {P Q : Submodule R A} {x : A} (hx : x ∈
 variable {M N P}
 
 theorem mem_span_singleton_mul {x y : A} : x ∈ span R {y} * P ↔ ∃ z ∈ P, y * z = x := by
-  simp_rw [mul_eq_map₂, (· * ·), map₂_span_singleton_eq_map]
-  rfl
+  simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map, mem_map, LinearMap.mul_apply_apply]
 
 theorem mem_mul_span_singleton {x y : A} : x ∈ P * span R {y} ↔ ∃ z ∈ P, z * y = x := by
-  simp_rw [mul_eq_map₂, (· * ·), map₂_span_singleton_eq_map_flip]
-  rfl
+  simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map_flip, mem_map, LinearMap.flip_apply,
+    LinearMap.mul_apply_apply]
 
 lemma span_singleton_mul {x : A} {p : Submodule R A} :
     Submodule.span R {x} * p = x • p := ext fun _ ↦ mem_span_singleton_mul
@@ -541,8 +540,8 @@ lemma mem_smul_iff_inv_mul_mem {S} [DivisionSemiring S] [Algebra R S] {x : S} {p
 
 lemma mul_mem_smul_iff {S} [CommRing S] [Algebra R S] {x : S} {p : Submodule R S} {y : S}
     (hx : x ∈ nonZeroDivisors S) :
-    x * y ∈ x • p ↔ y ∈ p :=
-  show Exists _ ↔ _ by simp [mul_cancel_left_mem_nonZeroDivisors hx]
+    x * y ∈ x • p ↔ y ∈ p := by
+  simp [mem_smul_pointwise_iff_exists, mul_cancel_left_mem_nonZeroDivisors hx]
 
 variable (M N) in
 theorem mul_smul_mul_eq_smul_mul_smul (x y : R) : (x * y) • (M * N) = (x • M) * (y • N) := by
@@ -801,10 +800,8 @@ theorem mem_div_iff_forall_mul_mem {x : A} {I J : Submodule R A} : x ∈ I / J 
   Iff.refl _
 
 theorem mem_div_iff_smul_subset {x : A} {I J : Submodule R A} : x ∈ I / J ↔ x • (J : Set A) ⊆ I :=
-  ⟨fun h y ⟨y', hy', xy'_eq_y⟩ => by
-    rw [← xy'_eq_y]
-    apply h
-    assumption, fun h _ hy => h (Set.smul_mem_smul_set hy)⟩
+  ⟨fun h y ⟨y', hy', xy'_eq_y⟩ => by rw [← xy'_eq_y]; exact h _ hy',
+    fun h _ hy => h (Set.smul_mem_smul_set hy)⟩
 
 theorem le_div_iff {I J K : Submodule R A} : I ≤ J / K ↔ ∀ x ∈ I, ∀ z ∈ K, x * z ∈ J :=
   Iff.refl _
@@ -813,9 +810,7 @@ theorem le_div_iff_mul_le {I J K : Submodule R A} : I ≤ J / K ↔ I * K ≤ J
   rw [le_div_iff, mul_le]
 
 theorem one_le_one_div {I : Submodule R A} : 1 ≤ 1 / I ↔ I ≤ 1 := by
-  constructor; all_goals intro hI
-  · rwa [le_div_iff_mul_le, one_mul] at hI
-  · rwa [le_div_iff_mul_le, one_mul]
+  rw [le_div_iff_mul_le, one_mul]
 
 @[simp]
 theorem one_mem_div {I J : Submodule R A} : 1 ∈ I / J ↔ J ≤ I := by
@@ -836,7 +831,7 @@ theorem mul_one_div_le_one {I : Submodule R A} : I * (1 / I) ≤ 1 := by
 protected theorem map_div {B : Type*} [CommSemiring B] [Algebra R B] (I J : Submodule R A)
     (h : A ≃ₐ[R] B) : (I / J).map h.toLinearMap = I.map h.toLinearMap / J.map h.toLinearMap := by
   ext x
-  simp only [mem_map, mem_div_iff_forall_mul_mem]
+  simp only [mem_map, mem_div_iff_forall_mul_mem, AlgEquiv.toLinearMap_apply]
   constructor
   · rintro ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
     exact ⟨x * y, hx _ hy, map_mul h x y⟩
@@ -845,9 +840,7 @@ protected theorem map_div {B : Type*} [CommSemiring B] [Algebra R B] (I J : Subm
     obtain ⟨xz, xz_mem, hxz⟩ := hx (h z) ⟨z, hz, rfl⟩
     convert xz_mem
     apply h.injective
-    rw [map_mul, h.apply_symm_apply]
-    simp only [AlgEquiv.toLinearMap_apply] at hxz
-    rw [hxz]
+    rw [map_mul, h.apply_symm_apply, hxz]
 
 end Quotient
 

Mathlib/Algebra/Polynomial/Laurent.lean

@@ -513,39 +513,38 @@ instance isLocalization : IsLocalization.Away (X : R[X]) R[T;T⁻¹] :=
       exact ⟨1, rfl⟩ }
 
 theorem mk'_mul_T (p : R[X]) (n : ℕ) :
-  IsLocalization.mk' R[T;T⁻¹] p (⟨X^n, n, rfl⟩ : Submonoid.powers (X : R[X])) * T n =
-    toLaurent p := by
+    IsLocalization.mk' R[T;T⁻¹] p (⟨X^n, n, rfl⟩ : Submonoid.powers (X : R[X])) * T n =
+      toLaurent p := by
   rw [←toLaurent_X_pow, ←algebraMap_eq_toLaurent, IsLocalization.mk'_spec, algebraMap_eq_toLaurent]
 
 @[simp]
-theorem mk'_eq (p : R[X]) (n : ℕ) : IsLocalization.mk' R[T;T⁻¹] p
-  (⟨X^n, n, rfl⟩ : Submonoid.powers (X : R[X])) = toLaurent p * T (-n) := by
+theorem mk'_eq (p : R[X]) (n : ℕ) :
+    IsLocalization.mk' R[T;T⁻¹] p (⟨X^n, n, rfl⟩ : Submonoid.powers (X : R[X])) =
+      toLaurent p * T (-n) := by
   rw [←IsUnit.mul_left_inj (isUnit_T n), mul_T_assoc, neg_add_cancel, T_zero, mul_one]
   exact mk'_mul_T p n
 
-theorem mk'_one_X_pow (n : ℕ) : IsLocalization.mk' R[T;T⁻¹] 1
-  (⟨X^n, n, rfl⟩ : Submonoid.powers (X : R[X])) = T (-n) := by
+theorem mk'_one_X_pow (n : ℕ) :
+    IsLocalization.mk' R[T;T⁻¹] 1 (⟨X^n, n, rfl⟩ : Submonoid.powers (X : R[X])) = T (-n) := by
   rw [mk'_eq 1 n, toLaurent_one, one_mul]
 
 @[simp]
-theorem mk'_one_X : IsLocalization.mk' R[T;T⁻¹] 1
-  (⟨X, 1, pow_one X⟩ : Submonoid.powers (X : R[X])) = T (-1) := by
+theorem mk'_one_X :
+    IsLocalization.mk' R[T;T⁻¹] 1 (⟨X, 1, pow_one X⟩ : Submonoid.powers (X : R[X])) = T (-1) := by
   convert mk'_one_X_pow 1
   exact (pow_one X).symm
 
 /-- Given a ring homomorphism `f : R →+* S` and a unit `x` in `S`, the induced homomorphism
 `R[T;T⁻¹] →+* S` sending `T` to `x` and `T⁻¹` to `x⁻¹`. -/
 def eval₂ : R[T;T⁻¹] →+* S :=
-  IsLocalization.lift (M := Submonoid.powers (X : R[X])) (g := Polynomial.eval₂RingHom f x) (by
+  IsLocalization.lift (M := Submonoid.powers (X : R[X])) (g := Polynomial.eval₂RingHom f x) <| by
     rintro ⟨y, n, rfl⟩
-    simpa only [coe_eval₂RingHom, eval₂_X_pow] using IsUnit.pow n x.isUnit
-  )
+    simpa only [coe_eval₂RingHom, eval₂_X_pow] using x.isUnit.pow n
 
 @[simp]
 theorem eval₂_toLaurent (p : R[X]) : eval₂ f x (toLaurent p) = Polynomial.eval₂ f x p := by
   unfold eval₂
-  rw [←algebraMap_eq_toLaurent, IsLocalization.lift_eq]
-  rfl
+  rw [←algebraMap_eq_toLaurent, IsLocalization.lift_eq, coe_eval₂RingHom]
 
 theorem eval₂_T_n (n : ℕ) : eval₂ f x (T n) = x ^ n := by
   rw [←Polynomial.toLaurent_X_pow, eval₂_toLaurent, eval₂_X_pow]
@@ -562,8 +561,7 @@ theorem eval₂_T (n : ℤ) : eval₂ f x (T n) = (x ^ n).val := by
   · lift n to ℕ using hn
     apply eval₂_T_n
   · obtain ⟨m, rfl⟩ := Int.exists_eq_neg_ofNat (Int.le_of_not_le hn)
-    rw [eval₂_T_neg_n, zpow_neg]
-    rfl
+    rw [eval₂_T_neg_n, zpow_neg, zpow_natCast, ← inv_pow, Units.val_pow_eq_pow_val]
 
 @[simp]
 theorem eval₂_C (r : R) : eval₂ f x (C r) = f r := by
@@ -579,11 +577,10 @@ theorem eval₂_C_mul_T_neg_n (r : R) (n : ℕ) : eval₂ f x (C r * T (-n)) =
 theorem eval₂_C_mul_T (r : R) (n : ℤ) : eval₂ f x (C r * T n) = f r * (x ^ n).val := by
   by_cases hn : 0 ≤ n
   · lift n to ℕ using hn
-    rw [map_mul, eval₂_C, eval₂_T_n]
-    rfl
+    rw [map_mul, eval₂_C, eval₂_T_n, zpow_natCast, Units.val_pow_eq_pow_val]
   · obtain ⟨m, rfl⟩ := Int.exists_eq_neg_ofNat (Int.le_of_not_le hn)
-    rw [map_mul, eval₂_C, eval₂_T_neg_n, zpow_neg]
-    rfl
+    rw [map_mul, eval₂_C, eval₂_T_neg_n, zpow_neg, zpow_natCast, ← inv_pow,
+      Units.val_pow_eq_pow_val]
 
 end CommSemiring
 

Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

@@ -77,7 +77,7 @@ lemma Cover.exists_eq (𝒰 : X.Cover P) (x : X) : ∃ i y, (𝒰.map i).base y
   ⟨_, 𝒰.covers x⟩
 
 /-- Given a family of schemes with morphisms to `X` satisfying `P` that jointly
-cover `X`, this an associated `P`-cover of `X`. -/
+cover `X`, `Cover.mkOfCovers` is an associated `P`-cover of `X`. -/
 @[simps]
 def Cover.mkOfCovers (J : Type*) (obj : J → Scheme.{u}) (map : (j : J) → obj j ⟶ X)
     (covers : ∀ x, ∃ j y, (map j).base y = x)

Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

@@ -92,7 +92,7 @@ lemma cons (L : List ℕ) (hL : IsAdmissible (m + 1) L) (a : ℕ) (ha : a ≤ m)
 
 /-- The tail of an `m`-admissible list is (m+1)-admissible. -/
 lemma tail (a : ℕ) (l : List ℕ) (h : IsAdmissible m (a::l)) :
-      IsAdmissible (m + 1) l := by
+    IsAdmissible (m + 1) l := by
   refine ⟨(List.sorted_cons.mp h.sorted).right, ?_⟩
   intro k _
   simpa [Nat.add_assoc, Nat.add_comm 1] using h.le (k + 1) (by simpa)
@@ -122,7 +122,7 @@ def simplicialInsert (a : ℕ) : List ℕ → List ℕ
   | [] => [a]
   | b :: l => if a < b then a :: b :: l else b :: simplicialInsert (a + 1) l
 
-/-- `simplicialInsert ` just adds one to the length. -/
+/-- `simplicialInsert` just adds one to the length. -/
 lemma simplicialInsert_length (a : ℕ) (L : List ℕ) :
     (simplicialInsert a L).length = L.length + 1 := by
   induction L generalizing a with

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Pi.lean

@@ -39,15 +39,15 @@ lemma cfcₙ_map_pi (f : R → R) (a : ∀ i, A i)
     (hf : ContinuousOn f (⋃ i, quasispectrum R (a i)) := by cfc_cont_tac)
     (ha : p a := by cfc_tac) (ha' : ∀ i, q i (a i) := by cfc_tac) :
     cfcₙ f a = fun i => cfcₙ f (a i) := by
-  by_cases hempty : Nonempty ι
-  · by_cases hf₀ : f 0 = 0
+  cases isEmpty_or_nonempty ι with
+  | inr h =>
+    by_cases hf₀ : f 0 = 0
     · ext i
       let φ := Pi.evalNonUnitalStarAlgHom S A i
       exact φ.map_cfcₙ f a (by rwa [Pi.quasispectrum_eq]) hf₀ (continuous_apply i) ha (ha' i)
-    · simp only [cfcₙ_apply_of_not_map_zero _ hf₀]; rfl
-  · simp only [not_nonempty_iff] at hempty
-    ext i
-    exact hempty.elim i
+    · simp only [cfcₙ_apply_of_not_map_zero _ hf₀, Pi.zero_def]
+  | inl h =>
+    exact Subsingleton.elim _ _
 
 end nonunital_pi
 

Mathlib/Analysis/Complex/Periodic.lean

@@ -167,7 +167,7 @@ variable {h : ℝ} {f : ℂ → ℂ}
 
 theorem boundedAtFilter_cuspFunction (hh : 0 < h) (h_bd : BoundedAtFilter I∞ f) :
     BoundedAtFilter (𝓝[≠] 0) (cuspFunction h f) := by
-  refine (h_bd.comp_tendsto <| invQParam_tendsto hh).congr' ?_ (by rfl)
+  refine (h_bd.comp_tendsto <| invQParam_tendsto hh).congr' ?_ (by simp)
   refine eventually_nhdsWithin_of_forall fun q hq ↦ ?_
   rw [cuspFunction_eq_of_nonzero _ _ hq, comp_def]
 

Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean

@@ -138,32 +138,20 @@ lemma star_mem_range_charAlgHom (he : Continuous e) (hL : Continuous fun p : V 
   simp only [charAlgHom_apply, Finsupp.support_embDomain, Finset.sum_map,
     Finsupp.embDomain_apply, star_apply, star_sum, star_mul', Circle.star_addChar]
   rw [Finsupp.support_mapRange_of_injective (star_zero _) y star_injective]
-  simp_rw [← map_neg (L u)]
-  rfl
+  simp [z, f]
 
 /-- The star-subalgebra of polynomials. -/
 noncomputable
 def charPoly (he : Continuous e) (hL : Continuous fun p : V × W ↦ L p.1 p.2) :
     StarSubalgebra ℂ (V →ᵇ ℂ) where
   toSubalgebra := (charAlgHom he hL).range
-  star_mem' := by
-    intro x hx
-    exact star_mem_range_charAlgHom he hL hx
+  star_mem' hx := star_mem_range_charAlgHom he hL hx
 
 lemma mem_charPoly (f : V →ᵇ ℂ) :
     f ∈ charPoly he hL
       ↔ ∃ w : AddMonoidAlgebra ℂ W, f = fun x ↦ ∑ a ∈ w.support, w a * (e (L x a) : ℂ) := by
   change f ∈ (charAlgHom he hL).range ↔ _
-  rw [AlgHom.mem_range]
-  constructor
-  · rintro ⟨y, rfl⟩
-    refine ⟨y, ?_⟩
-    ext
-    simp
-  · rintro ⟨y, h⟩
-    refine ⟨y, ?_⟩
-    ext
-    simp [h]
+  simp [BoundedContinuousFunction.ext_iff, funext_iff, eq_comm]
 
 lemma char_mem_charPoly (w : W) : char he hL w ∈ charPoly he hL := by
   rw [mem_charPoly]

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

@@ -515,11 +515,10 @@ lemma sqrt_rpow_nnreal {a : A} {x : ℝ≥0} : sqrt (a ^ (x : ℝ)) = a ^ (x / 2
   by_cases htriv : 0 ≤ a
   case neg => simp [sqrt_eq_cfc, rpow_def, cfc_apply_of_not_predicate a htriv]
   case pos =>
-    by_cases hx : x = 0
-    case pos => simp [hx, rpow_zero _ htriv]
-    case neg =>
-      have h₁ : 0 < x := lt_of_le_of_ne (by simp) (Ne.symm hx)
-      have h₂ : (x : ℝ) / 2 = NNReal.toReal (x / 2) := rfl
+    cases eq_zero_or_pos x with
+    | inl hx => simp [hx, rpow_zero _ htriv]
+    | inr h₁ =>
+      have h₂ : (x : ℝ) / 2 = NNReal.toReal (x / 2) := by simp
       have h₃ : 0 < x / 2 := by positivity
       rw [← nnrpow_eq_rpow h₁, h₂, ← nnrpow_eq_rpow h₃, sqrt_nnrpow (A := A)]
 

Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean

@@ -9,11 +9,6 @@ import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Algebra.Module.BigOperators
 import Mathlib.Algebra.Module.Pi
 
-/-! -/
--- fake module docstring just so that I can disable the long line linter without getting linted for
--- a missing module docstring!
-
-set_option linter.style.longLine false in
 /-!
 # Incidence algebras
 
@@ -66,7 +61,8 @@ Here are some additions to this file that could be made in the future:
 
 * [Aigner, *Combinatorial Theory, Chapter IV*][aigner1997]
 * [Jacobson, *Basic Algebra I, 8.6*][jacobson1974]
-* [Doubilet, Rota, Stanley, *On the foundations of Combinatorial Theory VI*][doubilet_rota_stanley_vi]
+* [Doubilet, Rota, Stanley, *On the foundations of Combinatorial Theory
+  VI*][doubilet_rota_stanley_vi]
 * [Spiegel, O'Donnell, *Incidence Algebras*][spiegel_odonnel1997]
 * [Kung, Rota, Yan, *Combinatorics: The Rota Way, Chapter 3*][kung_rota_yan2009]
 -/
@@ -385,7 +381,7 @@ private lemma muFun_apply (a b : α) :
 def mu : IncidenceAlgebra 𝕜 α :=
   ⟨muFun 𝕜, fun a b ↦ not_imp_comm.1 fun h ↦ by
     rw [muFun_apply] at h
-    split_ifs at h  with hab
+    split_ifs at h with hab
     · exact hab.le
     · rw [neg_eq_zero] at h
       obtain ⟨⟨x, hx⟩, -⟩ := exists_ne_zero_of_sum_ne_zero h
@@ -446,7 +442,7 @@ private def mu' : IncidenceAlgebra 𝕜 α :=
     not_imp_comm.1 fun h ↦ by
       dsimp only at h
       rw [muFun'_apply] at h
-      split_ifs at h  with hab
+      split_ifs at h with hab
       · exact hab.le
       · rw [neg_eq_zero] at h
         obtain ⟨⟨x, hx⟩, -⟩ := exists_ne_zero_of_sum_ne_zero h
@@ -522,7 +518,7 @@ lemma mu_toDual (a b : α) : mu 𝕜 (toDual a) (toDual b) = mu 𝕜 b a := by
   let mud : IncidenceAlgebra 𝕜 αᵒᵈ :=
     { toFun := fun a b ↦ mu 𝕜 (ofDual b) (ofDual a)
       eq_zero_of_not_le' := fun a b hab ↦ apply_eq_zero_of_not_le (by exact hab) _ }
-  suffices mu 𝕜 = mud by rw [this]; rfl
+  suffices mu 𝕜 = mud by simp_rw [this, mud, coe_mk, ofDual_toDual]
   suffices mud * zeta 𝕜 = 1 by
     rw [← mu_mul_zeta] at this
     apply_fun (· * mu 𝕜) at this
@@ -571,10 +567,12 @@ lemma moebius_inversion_top (f g : α → 𝕜) (h : ∀ x, g x = ∑ y ∈ Ici
     _ = ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by
       simp_rw [mul_apply, sum_mul]
     _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z := by
-      simp [mu_mul_zeta 𝕜, ← add_sum_Ioi_eq_sum_Ici]
+      simp only [mu_mul_zeta 𝕜, one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici, le_refl,
+        ↓reduceIte, ← add_sum_Ioi_eq_sum_Ici, left_eq_add]
       exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_le
     _ = f x := by
-      simp [one_apply, ← add_sum_Ioi_eq_sum_Ici]
+      simp only [one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici,
+        ← add_sum_Ioi_eq_sum_Ici, le_refl, ↓reduceIte, add_eq_left]
       exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_le
 
 end InversionTop

Mathlib/Combinatorics/SimpleGraph/Diam.lean

@@ -415,28 +415,23 @@ lemma center_eq_univ_iff_radius_eq_ediam [Nonempty α] :
     exact le_antisymm (le_iInf fun u ↦ (h u).ge) ((h Classical.ofNonempty) ▸ radius_le_eccent)
 
 lemma center_eq_univ_of_subsingleton [Subsingleton α] : G.center = Set.univ := by
-  rw [← Set.univ_subset_iff]
-  intro u h
-  rw [mem_center_iff, eccent_eq_zero_of_subsingleton u]
-  cases isEmpty_or_nonempty α
-  · rw [Set.univ_eq_empty_iff.mpr ‹_›] at h
-    exact h.elim
-  · symm
-    rw [radius_eq_zero_iff]
-    tauto
+  rw [Set.eq_univ_iff_forall]
+  intro u
+  rw [mem_center_iff, eccent_eq_zero_of_subsingleton u, eq_comm, radius_eq_zero_iff]
+  tauto
 
 lemma center_bot : (⊥ : SimpleGraph α).center = Set.univ := by
   cases subsingleton_or_nontrivial α
   · exact center_eq_univ_of_subsingleton
-  · rw [← Set.univ_subset_iff]
-    intro u h
+  · rw [Set.eq_univ_iff_forall]
+    intro u
     rw [mem_center_iff, eccent_bot, radius_bot]
 
 lemma center_top : (⊤ : SimpleGraph α).center = Set.univ := by
   cases subsingleton_or_nontrivial α
   · exact center_eq_univ_of_subsingleton
-  · rw [← Set.univ_subset_iff]
-    intro u h
+  · rw [Set.eq_univ_iff_forall]
+    intro u
     rw [mem_center_iff, eccent_top, radius_top]
 
 end center