[Merged by Bors] - chore: remove trailing semicolons

Mathlib/Algebra/Associated.lean

@@ -1157,7 +1157,7 @@ theorem mk_dvdNotUnit_mk_iff {a b : α} :
 #align associates.mk_dvd_not_unit_mk_iff Associates.mk_dvdNotUnit_mk_iff
 
 theorem dvdNotUnit_of_lt {a b : Associates α} (hlt : a < b) : DvdNotUnit a b := by
-  constructor;
+  constructor
   · rintro rfl
     apply not_lt_of_le _ hlt
     apply dvd_zero

Mathlib/Algebra/BigOperators/Group/List.lean

@@ -527,8 +527,8 @@ lemma prod_rotate_eq_one_of_prod_eq_one :
   | a :: l, hl, n => by
     have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
     rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl;
-      rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq, ←
-        one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_self, mul_one]
+    rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq, ←
+      one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_self, mul_one]
 #align list.prod_rotate_eq_one_of_prod_eq_one List.prod_rotate_eq_one_of_prod_eq_one
 
 end Group

Mathlib/Algebra/Free.lean

@@ -276,7 +276,7 @@ instance : LawfulTraversable FreeMagma.{u} :=
       FreeMagma.recOnPure x
         (fun x ↦ by simp only [(· ∘ ·), traverse_pure, traverse_pure', functor_norm])
         (fun x y ih1 ih2 ↦ by
-          rw [traverse_mul, ih1, ih2, traverse_mul];
+          rw [traverse_mul, ih1, ih2, traverse_mul]
           simp [Functor.Comp.map_mk, Functor.map_map, (· ∘ ·), Comp.seq_mk, seq_map_assoc,
             map_seq, traverse_mul])
     naturality := fun η α β f x ↦

Mathlib/Algebra/Group/Pi/Lemmas.lean

@@ -337,10 +337,10 @@ For injections of commuting elements at the same index, see `Commute.map` -/
 theorem Pi.mulSingle_commute [∀ i, MulOneClass <| f i] :
     Pairwise fun i j => ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y) := by
   intro i j hij x y; ext k
-  by_cases h1 : i = k;
+  by_cases h1 : i = k
   · subst h1
     simp [hij]
-  by_cases h2 : j = k;
+  by_cases h2 : j = k
   · subst h2
     simp [hij]
   simp [h1, h2]

Mathlib/Algebra/Group/Subgroup/Finite.lean

@@ -258,16 +258,16 @@ section Normalizer
 
 theorem mem_normalizer_fintype {S : Set G} [Finite S] {x : G} (h : ∀ n, n ∈ S → x * n * x⁻¹ ∈ S) :
     x ∈ Subgroup.setNormalizer S := by
-  haveI := Classical.propDecidable; cases nonempty_fintype S;
-      haveI := Set.fintypeImage S fun n => x * n * x⁻¹;
-    exact fun n =>
-      ⟨h n, fun h₁ =>
-        have heq : (fun n => x * n * x⁻¹) '' S = S :=
-          Set.eq_of_subset_of_card_le (fun n ⟨y, hy⟩ => hy.2 ▸ h y hy.1)
-            (by rw [Set.card_image_of_injective S conj_injective])
-        have : x * n * x⁻¹ ∈ (fun n => x * n * x⁻¹) '' S := heq.symm ▸ h₁
-        let ⟨y, hy⟩ := this
-        conj_injective hy.2 ▸ hy.1⟩
+  haveI := Classical.propDecidable; cases nonempty_fintype S
+  haveI := Set.fintypeImage S fun n => x * n * x⁻¹
+  exact fun n =>
+    ⟨h n, fun h₁ =>
+      have heq : (fun n => x * n * x⁻¹) '' S = S :=
+        Set.eq_of_subset_of_card_le (fun n ⟨y, hy⟩ => hy.2 ▸ h y hy.1)
+          (by rw [Set.card_image_of_injective S conj_injective])
+      have : x * n * x⁻¹ ∈ (fun n => x * n * x⁻¹) '' S := heq.symm ▸ h₁
+      let ⟨y, hy⟩ := this
+      conj_injective hy.2 ▸ hy.1⟩
 #align subgroup.mem_normalizer_fintype Subgroup.mem_normalizer_fintype
 
 end Normalizer

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -220,7 +220,7 @@ def map (f : F) (S : Submonoid M) :
   carrier := f '' S
   one_mem' := ⟨1, S.one_mem, map_one f⟩
   mul_mem' := by
-    rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩;
+    rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
     exact ⟨x * y, S.mul_mem hx hy, by rw [map_mul]⟩
 #align submonoid.map Submonoid.map
 #align add_submonoid.map AddSubmonoid.map

Mathlib/Algebra/Group/Units.lean

@@ -146,7 +146,7 @@ theorem val_mk (a : α) (b h₁ h₂) : ↑(Units.mk a b h₁ h₂) = a :=
 @[to_additive (attr := ext)]
 theorem ext : Function.Injective (val : αˣ → α)
   | ⟨v, i₁, vi₁, iv₁⟩, ⟨v', i₂, vi₂, iv₂⟩, e => by
-    simp only at e; subst v'; congr;
+    simp only at e; subst v'; congr
     simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁
 #align units.ext Units.ext
 #align add_units.ext AddUnits.ext

Mathlib/Algebra/Lie/Free.lean

@@ -225,7 +225,7 @@ def lift : (X → L) ≃ (FreeLieAlgebra R X →ₗ⁅R⁆ L) where
       map_lie' := by rintro ⟨a⟩ ⟨b⟩; rw [← liftAux_map_mul]; rfl }
   invFun F := F ∘ of R
   left_inv f := by
-    ext x;
+    ext x
     simp only [liftAux, of, Quot.liftOn_mk, LieHom.coe_mk, Function.comp_apply, lib.lift_of_apply]
   right_inv F := by
     ext ⟨a⟩

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -90,7 +90,7 @@ protected theorem weight_vector_multiplication (M₁ M₂ M₃ : Type*)
   let f₁ : Module.End R (M₁ ⊗[R] M₂) := (toEnd R L M₁ x - χ₁ • ↑1).rTensor M₂
   let f₂ : Module.End R (M₁ ⊗[R] M₂) := (toEnd R L M₂ x - χ₂ • ↑1).lTensor M₁
   have h_comm_square : F ∘ₗ ↑g = (g : M₁ ⊗[R] M₂ →ₗ[R] M₃).comp (f₁ + f₂) := by
-    ext m₁ m₂;
+    ext m₁ m₂
     simp only [f₁, f₂, F, ← g.map_lie x (m₁ ⊗ₜ m₂), add_smul, sub_tmul, tmul_sub, smul_tmul,
       lie_tmul_right, tmul_smul, toEnd_apply_apply, LieModuleHom.map_smul,
       LinearMap.one_apply, LieModuleHom.coe_toLinearMap, LinearMap.smul_apply, Function.comp_apply,

Mathlib/Algebra/Module/FinitePresentation.lean

@@ -297,7 +297,7 @@ lemma Module.FinitePresentation.isLocalizedModule_map
     have := (Module.End_isUnit_iff _).mp (IsLocalizedModule.map_units (S := S) (f := g) s)
     constructor
     · exact fun _ _ e ↦ LinearMap.ext fun m ↦ this.left (LinearMap.congr_fun e m)
-    · intro h;
+    · intro h
       use ((IsLocalizedModule.map_units (S := S) (f := g) s).unit⁻¹).1 ∘ₗ h
       ext x
       exact Module.End_isUnit_apply_inv_apply_of_isUnit

Mathlib/Algebra/Module/LocalizedModule.lean

@@ -188,15 +188,15 @@ private theorem add_comm' (x y : LocalizedModule S M) : x + y = y + x :=
 private theorem zero_add' (x : LocalizedModule S M) : 0 + x = x :=
   induction_on
     (fun m s => by
-      rw [← zero_mk s, mk_add_mk, smul_zero, zero_add, mk_eq];
-        exact ⟨1, by rw [one_smul, mul_smul, one_smul]⟩)
+      rw [← zero_mk s, mk_add_mk, smul_zero, zero_add, mk_eq]
+      exact ⟨1, by rw [one_smul, mul_smul, one_smul]⟩)
     x
 
 private theorem add_zero' (x : LocalizedModule S M) : x + 0 = x :=
   induction_on
     (fun m s => by
-      rw [← zero_mk s, mk_add_mk, smul_zero, add_zero, mk_eq];
-        exact ⟨1, by rw [one_smul, mul_smul, one_smul]⟩)
+      rw [← zero_mk s, mk_add_mk, smul_zero, add_zero, mk_eq]
+      exact ⟨1, by rw [one_smul, mul_smul, one_smul]⟩)
     x
 
 instance hasNatSMul : SMul ℕ (LocalizedModule S M) where smul n := nsmulRec n

Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

@@ -547,13 +547,13 @@ variable [DecidableEq ι]
 @[to_additive] lemma prod_sdiff_le_prod_sdiff :
     ∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i := by
   rw [← mul_le_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
-    ← prod_union, inter_comm, sdiff_union_inter];
+    ← prod_union, inter_comm, sdiff_union_inter]
   simpa only [inter_comm] using disjoint_sdiff_inter t s
 
 @[to_additive] lemma prod_sdiff_lt_prod_sdiff :
     ∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i := by
   rw [← mul_lt_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
-    ← prod_union, inter_comm, sdiff_union_inter];
+    ← prod_union, inter_comm, sdiff_union_inter]
   simpa only [inter_comm] using disjoint_sdiff_inter t s
 
 end OrderedCancelCommMonoid

Mathlib/Algebra/Order/Group/Int.lean

@@ -125,8 +125,7 @@ theorem abs_ediv_le_abs : ∀ a b : ℤ, |a / b| ≤ |a| :=
     | _, ⟨n, Or.inr rfl⟩ => by rw [Int.ediv_neg, abs_neg]; apply this
   fun a n => by
   rw [abs_eq_natAbs, abs_eq_natAbs];
-    exact
-      ofNat_le_ofNat_of_le
+    exact ofNat_le_ofNat_of_le
         (match a, n with
         | (m : ℕ), n => Nat.div_le_self _ _
         | -[m+1], 0 => Nat.zero_le _

Mathlib/Algebra/Order/Ring/Basic.lean

@@ -48,7 +48,7 @@ theorem zero_pow_le_one : ∀ n : ℕ, (0 : R) ^ n ≤ 1
 
 theorem pow_add_pow_le (hx : 0 ≤ x) (hy : 0 ≤ y) (hn : n ≠ 0) : x ^ n + y ^ n ≤ (x + y) ^ n := by
   rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩
-  induction' k with k ih;
+  induction' k with k ih
   · have eqn : Nat.succ Nat.zero = 1 := rfl
     rw [eqn]
     simp only [pow_one, le_refl]

Mathlib/Algebra/Order/ToIntervalMod.lean

@@ -691,7 +691,7 @@ alias ⟨_, AddCommGroup.ModEq.toIcoMod_eq_toIcoMod⟩ := toIcoMod_inj
 
 theorem Ico_eq_locus_Ioc_eq_iUnion_Ioo :
     { b | toIcoMod hp a b = toIocMod hp a b } = ⋃ z : ℤ, Set.Ioo (a + z • p) (a + p + z • p) := by
-  ext1;
+  ext1
   simp_rw [Set.mem_setOf, Set.mem_iUnion, ← Set.sub_mem_Ioo_iff_left, ←
     not_modEq_iff_toIcoMod_eq_toIocMod, modEq_iff_not_forall_mem_Ioo_mod hp, not_forall,
     Classical.not_not]

Mathlib/Algebra/Polynomial/Basic.lean

@@ -348,8 +348,8 @@ instance isScalarTower {S₁ S₂} [SMul S₁ S₂] [SMulZeroClass S₁ R] [SMul
 instance isScalarTower_right {α K : Type*} [Semiring K] [DistribSMul α K] [IsScalarTower α K K] :
     IsScalarTower α K[X] K[X] :=
   ⟨by
-    rintro _ ⟨⟩ ⟨⟩;
-      simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]⟩
+    rintro _ ⟨⟩ ⟨⟩
+    simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]⟩
 #align polynomial.is_scalar_tower_right Polynomial.isScalarTower_right
 
 instance isCentralScalar {S} [SMulZeroClass S R] [SMulZeroClass Sᵐᵒᵖ R] [IsCentralScalar S R] :
@@ -1303,7 +1303,7 @@ protected instance repr [Repr R] [DecidableEq R] : Repr R[X] :=
           if coeff p n = 1
           then (80, "X ^ " ++ Nat.repr n)
           else (70, "C " ++ reprArg (coeff p n) ++ " * X ^ " ++ Nat.repr n))
-      (p.support.sort (· ≤ ·));
+      (p.support.sort (· ≤ ·))
     match termPrecAndReprs with
     | [] => "0"
     | [(tprec, t)] => if prec ≥ tprec then Lean.Format.paren t else t

Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean

@@ -44,7 +44,7 @@ noncomputable def cardPowDegree : AbsoluteValue Fq[X] ℤ :=
   have card_pos : 0 < Fintype.card Fq := Fintype.card_pos_iff.mpr inferInstance
   have pow_pos : ∀ n, 0 < (Fintype.card Fq : ℤ) ^ n := fun n =>
     pow_pos (Int.natCast_pos.mpr card_pos) n
-  letI := Classical.decEq Fq;
+  letI := Classical.decEq Fq
   { toFun := fun p => if p = 0 then 0 else (Fintype.card Fq : ℤ) ^ p.natDegree
     nonneg' := fun p => by
       dsimp

Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

@@ -53,8 +53,8 @@ theorem natDegree_comp_le : natDegree (p.comp q) ≤ natDegree p * natDegree q :
               _ ≤ natDegree (C (coeff p n)) + n • ↑(natDegree q) :=
                 (add_le_add_left (nsmul_le_nsmul_right (@degree_le_natDegree _ _ q) n) _)
               _ = (n * natDegree q : ℕ) := by
-                rw [natDegree_C, Nat.cast_zero, zero_add, nsmul_eq_mul];
-                  simp
+                rw [natDegree_C, Nat.cast_zero, zero_add, nsmul_eq_mul]
+                simp
               _ ≤ (natDegree p * natDegree q : ℕ) :=
                 WithBot.coe_le_coe.2 <|
                   mul_le_mul_of_nonneg_right (le_natDegree_of_ne_zero (mem_support_iff.1 hn))

Mathlib/Algebra/Polynomial/Div.lean

@@ -265,8 +265,8 @@ theorem modByMonic_add_div (p : R[X]) {q : R[X]} (hq : Monic q) : p %ₘ q + q *
 
 theorem divByMonic_eq_zero_iff [Nontrivial R] (hq : Monic q) : p /ₘ q = 0 ↔ degree p < degree q :=
   ⟨fun h => by
-    have := modByMonic_add_div p hq;
-      rwa [h, mul_zero, add_zero, modByMonic_eq_self_iff hq] at this,
+    have := modByMonic_add_div p hq
+    rwa [h, mul_zero, add_zero, modByMonic_eq_self_iff hq] at this,
   fun h => by
     classical
     have : ¬degree q ≤ degree p := not_le_of_gt h
@@ -298,13 +298,13 @@ theorem degree_divByMonic_le (p q : R[X]) : degree (p /ₘ q) ≤ degree p :=
   else
     if hq : Monic q then
       if h : degree q ≤ degree p then by
-        haveI := Nontrivial.of_polynomial_ne hp0;
-            rw [← degree_add_divByMonic hq h, degree_eq_natDegree hq.ne_zero,
-              degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 (not_lt.2 h))];
-          exact WithBot.coe_le_coe.2 (Nat.le_add_left _ _)
+        haveI := Nontrivial.of_polynomial_ne hp0
+        rw [← degree_add_divByMonic hq h, degree_eq_natDegree hq.ne_zero,
+          degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 (not_lt.2 h))]
+        exact WithBot.coe_le_coe.2 (Nat.le_add_left _ _)
       else by
-        unfold divByMonic divModByMonicAux;
-          simp [dif_pos hq, h, false_and_iff, if_false, degree_zero, bot_le]
+        unfold divByMonic divModByMonicAux
+        simp [dif_pos hq, h, false_and_iff, if_false, degree_zero, bot_le]
     else (divByMonic_eq_of_not_monic p hq).symm ▸ bot_le
 #align polynomial.degree_div_by_monic_le Polynomial.degree_divByMonic_le
 

Mathlib/Algebra/Polynomial/FieldDivision.lean

@@ -362,9 +362,9 @@ theorem mod_eq_self_iff (hq0 : q ≠ 0) : p % q = p ↔ degree p < degree q :=
 
 theorem div_eq_zero_iff (hq0 : q ≠ 0) : p / q = 0 ↔ degree p < degree q :=
   ⟨fun h => by
-    have := EuclideanDomain.div_add_mod p q;
-      rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this,
-    fun h => by
+    have := EuclideanDomain.div_add_mod p q
+    rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this,
+  fun h => by
     have hlt : degree p < degree (q * C (leadingCoeff q)⁻¹) := by
       rwa [degree_mul_leadingCoeff_inv q hq0]
     have hm : Monic (q * C (leadingCoeff q)⁻¹) := monic_mul_leadingCoeff_inv hq0
@@ -390,10 +390,9 @@ theorem degree_div_le (p q : R[X]) : degree (p / q) ≤ degree p := by
 
 theorem degree_div_lt (hp : p ≠ 0) (hq : 0 < degree q) : degree (p / q) < degree p := by
   have hq0 : q ≠ 0 := fun hq0 => by simp [hq0] at hq
-  rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq0];
-    exact
-      degree_divByMonic_lt _ (monic_mul_leadingCoeff_inv hq0) hp
-        (by rw [degree_mul_leadingCoeff_inv _ hq0]; exact hq)
+  rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq0]
+  exact degree_divByMonic_lt _ (monic_mul_leadingCoeff_inv hq0) hp
+    (by rw [degree_mul_leadingCoeff_inv _ hq0]; exact hq)
 #align polynomial.degree_div_lt Polynomial.degree_div_lt
 
 theorem isUnit_map [Field k] (f : R →+* k) : IsUnit (p.map f) ↔ IsUnit p := by

Mathlib/Algebra/Polynomial/Identities.lean

@@ -103,7 +103,7 @@ for some `z` in the ring.
 -/
 def evalSubFactor (f : R[X]) (x y : R) : { z : R // f.eval x - f.eval y = z * (x - y) } := by
   refine ⟨f.sum fun i r => r * (powSubPowFactor x y i).val, ?_⟩
-  delta eval; rw [eval₂_eq_sum, eval₂_eq_sum];
+  delta eval; rw [eval₂_eq_sum, eval₂_eq_sum]
   simp only [sum, ← Finset.sum_sub_distrib, Finset.sum_mul]
   dsimp
   congr with i

Mathlib/Algebra/Polynomial/RingDivision.lean

@@ -149,8 +149,8 @@ theorem degree_le_mul_left (p : R[X]) (hq : q ≠ 0) : degree p ≤ degree (p *
   classical
   exact if hp : p = 0 then by simp only [hp, zero_mul, le_refl]
   else by
-    rw [degree_mul, degree_eq_natDegree hp, degree_eq_natDegree hq];
-      exact WithBot.coe_le_coe.2 (Nat.le_add_right _ _)
+    rw [degree_mul, degree_eq_natDegree hp, degree_eq_natDegree hq]
+    exact WithBot.coe_le_coe.2 (Nat.le_add_right _ _)
 #align polynomial.degree_le_mul_left Polynomial.degree_le_mul_left
 
 theorem natDegree_le_of_dvd {p q : R[X]} (h1 : p ∣ q) (h2 : q ≠ 0) : p.natDegree ≤ q.natDegree := by
@@ -435,9 +435,9 @@ theorem le_rootMultiplicity_iff {p : R[X]} (p0 : p ≠ 0) {a : R} {n : ℕ} :
   rw [rootMultiplicity_eq_nat_find_of_nonzero p0, @Nat.le_find_iff _ (_)]
   simp_rw [Classical.not_not]
   refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
-  cases' n with n;
+  cases' n with n
   · rw [pow_zero]
-    apply one_dvd;
+    apply one_dvd
   · exact h n n.lt_succ_self
 #align polynomial.le_root_multiplicity_iff Polynomial.le_rootMultiplicity_iff
 
@@ -802,8 +802,8 @@ theorem exists_multiset_roots [DecidableEq R] :
             congr
             exact mod_cast Multiset.card_cons _ _
           _ ≤ degree p := by
-            rw [← degree_add_divByMonic (monic_X_sub_C x) hdeg, degree_X_sub_C, add_comm];
-              exact add_le_add (le_refl (1 : WithBot ℕ)) htd,
+            rw [← degree_add_divByMonic (monic_X_sub_C x) hdeg, degree_X_sub_C, add_comm]
+            exact add_le_add (le_refl (1 : WithBot ℕ)) htd,
         by
           change ∀ (a : R), count a (x ::ₘ t) = rootMultiplicity a p
           intro a
@@ -821,7 +821,7 @@ termination_by p => natDegree p
 decreasing_by {
   simp_wf
   apply (Nat.cast_lt (α := WithBot ℕ)).mp
-  simp only [degree_eq_natDegree hp, degree_eq_natDegree hd0] at wf;
+  simp only [degree_eq_natDegree hp, degree_eq_natDegree hd0] at wf
   assumption}
 #align polynomial.exists_multiset_roots Polynomial.exists_multiset_roots
 
@@ -871,7 +871,7 @@ theorem Monic.irreducible_of_irreducible_map (f : R[X]) (h_mon : Monic f)
     (congr_arg (Polynomial.map φ) h).trans (Polynomial.map_mul φ)).imp ?_ ?_ <;>
       apply isUnit_of_isUnit_leadingCoeff_of_isUnit_map <;>
     apply isUnit_of_mul_eq_one
-  · exact q;
+  · exact q
   · rw [mul_comm]
     exact q
 #align polynomial.monic.irreducible_of_irreducible_map Polynomial.Monic.irreducible_of_irreducible_map

Mathlib/AlgebraicGeometry/Cover/Open.lean

@@ -408,7 +408,7 @@ lemma OpenCover.ext_elem {X : Scheme.{u}} {U : Opens X} (f g : Γ(X, U)) (𝒰 :
       Set.mem_iUnion, Set.mem_inter_iff, Set.mem_range, SetLike.mem_coe, exists_and_right]
     refine ⟨?_, hx⟩
     simpa using ⟨_, 𝒰.covers x⟩
-  · intro x;
+  · intro x
     replace h := h (𝒰.f x)
     rw [← IsOpenImmersion.map_ΓIso_inv] at h
     exact (IsOpenImmersion.ΓIso (𝒰.map (𝒰.f x)) U).commRingCatIsoToRingEquiv.symm.injective h

Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

@@ -415,7 +415,7 @@ theorem exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated (X : Scheme.{u}) (U :
         X.presheaf.map (homOfLE <| inf_le_right).op
           (X.presheaf.map (homOfLE le_sup_right).op f ^ (Finset.univ.sup n + n₁) * y₂) := by
       fapply X.sheaf.eq_of_locally_eq' fun i : s => i.1.1
-      · refine fun i => homOfLE ?_; erw [hs];
+      · refine fun i => homOfLE ?_; erw [hs]
         -- Porting note: have to add argument explicitly
         exact @le_iSup (Opens X) s _ (fun (i : s) => (i : Opens X)) i
       · exact le_of_eq hs

Mathlib/AlgebraicGeometry/Spec.lean

@@ -338,7 +338,7 @@ set_option linter.uppercaseLean3 false in
 theorem Spec_Γ_naturality {R S : CommRingCat.{u}} (f : R ⟶ S) :
     f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op := by
   -- Porting note: `ext` failed to pick up one of the three lemmas
-  refine RingHom.ext fun x => Subtype.ext <| funext fun x' => ?_; symm;
+  refine RingHom.ext fun x => Subtype.ext <| funext fun x' => ?_; symm
   apply Localization.localRingHom_to_map
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.Spec_Γ_naturality AlgebraicGeometry.Spec_Γ_naturality

Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

@@ -313,7 +313,7 @@ theorem D_subset_differentiable_set {K : Set (E →L[𝕜] F)} (hK : IsComplete
     refine ⟨(1 / 2) ^ (n e + 1), P, fun y hy => ?_⟩
     -- We need to show that `f (x + y) - f x - f' y` is small. For this, we will work at scale
     -- `k` where `k` is chosen with `‖y‖ ∼ 2 ^ (-k)`.
-    by_cases y_pos : y = 0;
+    by_cases y_pos : y = 0
     · simp [y_pos]
     have yzero : 0 < ‖y‖ := norm_pos_iff.mpr y_pos
     have y_lt : ‖y‖ < (1 / 2) ^ (n e + 1) := by simpa using mem_ball_iff_norm.1 hy

Mathlib/Analysis/Complex/PhragmenLindelof.lean

@@ -354,7 +354,7 @@ nonrec theorem quadrant_I (hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0))
     (hre : ∀ x : ℝ, 0 ≤ x → ‖f x‖ ≤ C) (him : ∀ x : ℝ, 0 ≤ x → ‖f (x * I)‖ ≤ C) (hz_re : 0 ≤ z.re)
     (hz_im : 0 ≤ z.im) : ‖f z‖ ≤ C := by
   -- The case `z = 0` is trivial.
-  rcases eq_or_ne z 0 with (rfl | hzne);
+  rcases eq_or_ne z 0 with (rfl | hzne)
   · exact hre 0 le_rfl
   -- Otherwise, `z = e ^ ζ` for some `ζ : ℂ`, `0 < Im ζ < π / 2`.
   obtain ⟨ζ, hζ, rfl⟩ : ∃ ζ : ℂ, ζ.im ∈ Icc 0 (π / 2) ∧ exp ζ = z := by

Mathlib/Analysis/Complex/Schwarz.lean

@@ -154,7 +154,7 @@ open ball with center `f c` and radius `R₂`, then for any `z` in the former di
 theorem dist_le_div_mul_dist_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
     (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
     dist (f z) (f c) ≤ R₂ / R₁ * dist z c := by
-  rcases eq_or_ne z c with (rfl | hne);
+  rcases eq_or_ne z c with (rfl | hne)
   · simp only [dist_self, mul_zero, le_rfl]
   simpa only [dslope_of_ne _ hne, slope_def_module, norm_smul, norm_inv, ← div_eq_inv_mul, ←
     dist_eq_norm, div_le_iff (dist_pos.2 hne)] using norm_dslope_le_div_of_mapsTo_ball hd h_maps hz