chore: tidy various files (leanprover-community#13860)

Author: Ruben-VandeVelde

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -241,7 +241,7 @@ theorem first_vote_pos :
       · norm_cast
         rw [mul_comm _ (p + 1), ← Nat.succ_eq_add_one p, Nat.succ_add, Nat.succ_mul_choose_eq,
           mul_comm]
-      all_goals simp [(Nat.choose_pos <| (le_add_iff_nonneg_right _).2 zero_le').ne.symm]
+      all_goals simp [(Nat.choose_pos <| le_add_of_nonneg_right zero_le').ne']
     · simp
 #align ballot.first_vote_pos Ballot.first_vote_pos
 

Mathlib/Algebra/Associated.lean

@@ -1180,19 +1180,19 @@ section CancelCommMonoidWithZero
 variable [CancelCommMonoidWithZero α]
 
 instance instPartialOrder : PartialOrder (Associates α) where
-    le_antisymm := mk_surjective.forall₂.2 fun _a _b hab hba => mk_eq_mk_iff_associated.2 <|
-      associated_of_dvd_dvd (dvd_of_mk_le_mk hab) (dvd_of_mk_le_mk hba)
+  le_antisymm := mk_surjective.forall₂.2 fun _a _b hab hba => mk_eq_mk_iff_associated.2 <|
+    associated_of_dvd_dvd (dvd_of_mk_le_mk hab) (dvd_of_mk_le_mk hba)
 
 instance instOrderedCommMonoid : OrderedCommMonoid (Associates α) where
-    mul_le_mul_left := fun a _ ⟨d, hd⟩ c => hd.symm ▸ mul_assoc c a d ▸ le_mul_right
+  mul_le_mul_left := fun a _ ⟨d, hd⟩ c => hd.symm ▸ mul_assoc c a d ▸ le_mul_right
 
 instance instCancelCommMonoidWithZero : CancelCommMonoidWithZero (Associates α) :=
-{ (by infer_instance : CommMonoidWithZero (Associates α)) with
-  mul_left_cancel_of_ne_zero := by
-    rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h
-    rcases Quotient.exact' h with ⟨u, hu⟩
-    have hu : a * (b * ↑u) = a * c := by rwa [← mul_assoc]
-    exact Quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩ }
+  { (by infer_instance : CommMonoidWithZero (Associates α)) with
+    mul_left_cancel_of_ne_zero := by
+      rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h
+      rcases Quotient.exact' h with ⟨u, hu⟩
+      have hu : a * (b * ↑u) = a * c := by rwa [← mul_assoc]
+      exact Quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩ }
 
 theorem _root_.associates_irreducible_iff_prime [DecompositionMonoid α] {p : Associates α} :
     Irreducible p ↔ Prime p := irreducible_iff_prime
@@ -1212,9 +1212,9 @@ theorem one_or_eq_of_le_of_prime {p m : Associates α} (hp : Prime p) (hle : m 
 #align associates.one_or_eq_of_le_of_prime Associates.one_or_eq_of_le_of_prime
 
 instance : CanonicallyOrderedCommMonoid (Associates α) where
-  exists_mul_of_le := fun h => h
-  le_self_mul := fun _ b => ⟨b, rfl⟩
-  bot_le := fun _ => one_le
+  exists_mul_of_le h := h
+  le_self_mul _ b := ⟨b, rfl⟩
+  bot_le _ := one_le
 
 theorem dvdNotUnit_iff_lt {a b : Associates α} : DvdNotUnit a b ↔ a < b :=
   dvd_and_not_dvd_iff.symm

Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean

@@ -320,11 +320,11 @@ def toSheafify : M₀ ⟶ (restrictScalars α).obj (sheafify α φ).val where
     simpa using (Sheafify.map_smul_eq α φ (α.app _ r₀) (φ.app _ m₀) (𝟙 _)
       r₀ (by aesop) m₀ (by simp)).symm
 
-instance : Presheaf.IsLocallyInjective J (toSheafify α φ).hom :=
-  by dsimp; infer_instance
+instance : Presheaf.IsLocallyInjective J (toSheafify α φ).hom := by
+  dsimp; infer_instance
 
-instance : Presheaf.IsLocallySurjective J (toSheafify α φ).hom :=
-  by dsimp; infer_instance
+instance : Presheaf.IsLocallySurjective J (toSheafify α φ).hom := by
+  dsimp; infer_instance
 
 variable [J.WEqualsLocallyBijective AddCommGroupCat.{v}]
 

Mathlib/Algebra/GeomSum.lean

@@ -497,7 +497,7 @@ theorem geom_sum_alternating_of_le_neg_one [StrictOrderedRing α] (hx : x + 1 
 
 theorem geom_sum_alternating_of_lt_neg_one [StrictOrderedRing α] (hx : x + 1 < 0) (hn : 1 < n) :
     if Even n then (∑ i ∈ range n, x ^ i) < 0 else 1 < ∑ i ∈ range n, x ^ i := by
-  have hx0 : x < 0 := ((le_add_iff_nonneg_right _).2 zero_le_one).trans_lt hx
+  have hx0 : x < 0 := (le_add_of_nonneg_right zero_le_one).trans_lt hx
   refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
   · simp only [geom_sum_two, lt_add_iff_pos_left, ite_true, gt_iff_lt, hx, even_two]
   clear hn

Mathlib/Algebra/Lie/Semisimple/Basic.lean

@@ -116,7 +116,7 @@ open CompleteLattice IsCompactlyGenerated
 variable {R L}
 variable [IsSemisimple R L]
 
-lemma isSimple_of_isAtom  (I : LieIdeal R L) (hI : IsAtom I) : IsSimple R I where
+lemma isSimple_of_isAtom (I : LieIdeal R L) (hI : IsAtom I) : IsSimple R I where
   non_abelian := IsSemisimple.non_abelian_of_isAtom I hI
   eq_bot_or_eq_top := by
     -- Suppose that `J` is an ideal of `I`.

Mathlib/Algebra/Lie/Weights/Cartan.lean

@@ -72,9 +72,9 @@ theorem lie_mem_weightSpace_of_mem_weightSpace {χ₁ χ₂ : H → R} {x : L} {
 lemma toEnd_pow_apply_mem {χ₁ χ₂ : H → R} {x : L} {m : M}
     (hx : x ∈ rootSpace H χ₁) (hm : m ∈ weightSpace M χ₂) (n) :
     (toEnd R L M x ^ n : Module.End R M) m ∈ weightSpace M (n • χ₁ + χ₂) := by
-  induction n
-  · simpa using hm
-  · next n IH =>
+  induction n with
+  | zero => simpa using hm
+  | succ n IH =>
     simp only [pow_succ', LinearMap.mul_apply, toEnd_apply_apply,
       Nat.cast_add, Nat.cast_one, rootSpace]
     convert lie_mem_weightSpace_of_mem_weightSpace hx IH using 2

Mathlib/Algebra/Lie/Weights/Killing.lean

@@ -260,13 +260,14 @@ lemma isSemisimple_ad_of_mem_isCartanSubalgebra {x : L} (hx : x ∈ H) :
   replace h_der (y z : L) : S ⁅y, z⁆ = ⁅S y, z⁆ + ⁅y, S z⁆ := by
     have hy : y ∈ ⨆ α : H → K, rootSpace H α := by simp [iSup_weightSpace_eq_top]
     have hz : z ∈ ⨆ α : H → K, rootSpace H α := by simp [iSup_weightSpace_eq_top]
-    induction hy using LieSubmodule.iSup_induction'
-    · induction hz using LieSubmodule.iSup_induction'
-      · next α y hy β z hz => exact h_der y z α β hy hz
-      · simp
-      · next h h' => simp only [lie_add, map_add, h, h']; abel
-    · simp
-    · next h h' => simp only [add_lie, map_add, h, h']; abel
+    induction hy using LieSubmodule.iSup_induction' with
+    | hN α y hy =>
+      induction hz using LieSubmodule.iSup_induction' with
+      | hN β z hz => exact h_der y z α β hy hz
+      | h0 => simp
+      | hadd _ _ _ _ h h' => simp only [lie_add, map_add, h, h']; abel
+    | h0 => simp
+    | hadd _ _ _ _ h h' => simp only [add_lie, map_add, h, h']; abel
   /- An equivalent form of the derivation axiom used in `LieDerivation`. -/
   replace h_der : ∀ y z : L, S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆ := by
     simp_rw [← lie_skew (S _) _, add_comm, ← sub_eq_add_neg] at h_der; assumption
@@ -419,16 +420,16 @@ lemma traceForm_eq_zero_of_mem_ker_of_mem_span_coroot {α : Weight K H L} {x y :
     (hx : x ∈ α.ker) (hy : y ∈ K ∙ coroot α) :
     traceForm K H L x y = 0 := by
   rw [← coe_corootSpace_eq_span_singleton, LieSubmodule.mem_coeSubmodule, mem_corootSpace'] at hy
-  induction hy using Submodule.span_induction'
-  · next z hz =>
+  induction hy using Submodule.span_induction' with
+  | mem z hz =>
     obtain ⟨u, hu, v, -, huv⟩ := hz
     change killingForm K L (x : L) (z : L) = 0
     replace hx : α x = 0 := by simpa using hx
     rw [← huv, ← traceForm_apply_lie_apply, ← LieSubalgebra.coe_bracket_of_module,
       lie_eq_smul_of_mem_rootSpace hu, hx, zero_smul, map_zero, LinearMap.zero_apply]
-  · simp
-  · next hx hy => simp [hx, hy]
-  · next hz => simp [hz]
+  | zero => simp
+  | add _ _ _ _ hx hy => simp [hx, hy]
+  | smul _ _ _ hz => simp [hz]
 
 @[simp] lemma orthogonal_span_coroot_eq_ker (α : Weight K H L) :
     (traceForm K H L).orthogonal (K ∙ coroot α) = α.ker := by

Mathlib/Algebra/Polynomial/Derivative.lean

@@ -488,7 +488,7 @@ theorem iterate_derivative_X_pow_eq_natCast_mul (n k : ℕ) :
   induction' k with k ih
   · erw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
   · rw [Function.iterate_succ_apply', ih, derivative_natCast_mul, derivative_X_pow, C_eq_natCast,
-      Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul];
+      Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]
     simp [mul_comm, mul_assoc, mul_left_comm]
 set_option linter.uppercaseLean3 false in
 #align polynomial.iterate_derivative_X_pow_eq_nat_cast_mul Polynomial.iterate_derivative_X_pow_eq_natCast_mul

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -333,8 +333,7 @@ theorem SLOnGLPos_smul_apply (s : SL(2, ℤ)) (g : GL(2, ℝ)⁺) (z : ℍ) :
 #align upper_half_plane.SL_on_GL_pos_smul_apply UpperHalfPlane.ModularGroup.SLOnGLPos_smul_apply
 
 instance SL_to_GL_tower : IsScalarTower SL(2, ℤ) GL(2, ℝ)⁺ ℍ where
-  smul_assoc := by
-    intro s g z
+  smul_assoc s g z := by
     simp only [SLOnGLPos_smul_apply]
     apply mul_smul'
 #align upper_half_plane.SL_to_GL_tower UpperHalfPlane.ModularGroup.SL_to_GL_tower
@@ -349,8 +348,7 @@ theorem subgroup_on_glpos_smul_apply (s : Γ) (g : GL(2, ℝ)⁺) (z : ℍ) :
 #align upper_half_plane.subgroup_on_GL_pos_smul_apply UpperHalfPlane.ModularGroup.subgroup_on_glpos_smul_apply
 
 instance subgroup_on_glpos : IsScalarTower Γ GL(2, ℝ)⁺ ℍ where
-  smul_assoc := by
-    intro s g z
+  smul_assoc s g z := by
     simp only [subgroup_on_glpos_smul_apply]
     apply mul_smul'
 #align upper_half_plane.subgroup_on_GL_pos UpperHalfPlane.ModularGroup.subgroup_on_glpos

Mathlib/Analysis/Convex/Body.lean

@@ -234,7 +234,7 @@ theorem iInter_smul_eq_self [T2Space V] {u : ℕ → ℝ≥0} (K : ConvexBody V)
     refine lt_of_le_of_lt ?_ hn
     exact mul_le_mul_of_nonneg_left (hC_bdd _ hyK) (abs_nonneg _)
   · refine Set.mem_iInter.mpr (fun n => Convex.mem_smul_of_zero_mem K.convex h_zero h ?_)
-    exact (le_add_iff_nonneg_right _).mpr (by positivity)
+    exact le_add_of_nonneg_right (by positivity)
 
 end SeminormedAddCommGroup