chore(*): remove empty lines between variable statements (#11418)

Empty lines were removed by executing the following Python script twice
```python
import os
import re


# Loop through each file in the repository
for dir_path, dirs, files in os.walk('.'):
  for filename in files:
    if filename.endswith('.lean'):
      file_path = os.path.join(dir_path, filename)

      # Open the file and read its contents
      with open(file_path, 'r') as file:
        content = file.read()

      # Use a regular expression to replace sequences of "variable" lines separated by empty lines
      # with sequences without empty lines
      modified_content = re.sub(r'(variable.*\n)\n(variable(?! .* in))', r'\1\2', content)

      # Write the modified content back to the file
      with open(file_path, 'w') as file:
        file.write(modified_content)
```

Archive/Imo/Imo1975Q1.lean

@@ -30,9 +30,7 @@ open scoped BigOperators
 /- Let `n` be a natural number, `x` and `y` be as in the problem statement and `σ` be the
 permutation of natural numbers such that `z = y ∘ σ` -/
 variable (n : ℕ) (σ : Equiv.Perm ℕ) (hσ : {x | σ x ≠ x} ⊆ Finset.Icc 1 n) (x y : ℕ → ℝ)
-
 variable (hx : AntitoneOn x (Finset.Icc 1 n))
-
 variable (hy : AntitoneOn y (Finset.Icc 1 n))
 
 theorem imo1975_q1 :

Archive/Imo/Imo2019Q2.lean

@@ -68,9 +68,7 @@ set_option linter.uppercaseLean3 false
 attribute [local instance] FiniteDimensional.of_fact_finrank_eq_two
 
 variable (V : Type*) (Pt : Type*)
-
 variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]
-
 variable [NormedAddTorsor V Pt] [hd2 : Fact (finrank ℝ V = 2)]
 
 namespace Imo2019Q2

Archive/Wiedijk100Theorems/SolutionOfCubic.lean

@@ -44,11 +44,8 @@ section Field
 open Polynomial
 
 variable {K : Type*} [Field K]
-
 variable [Invertible (2 : K)] [Invertible (3 : K)]
-
 variable (a b c d : K)
-
 variable {ω p q r s t : K}
 
 theorem cube_root_of_unity_sum (hω : IsPrimitiveRoot ω 3) : 1 + ω + ω ^ 2 = 0 := by

Mathlib/Algebra/Algebra/Basic.lean

@@ -585,7 +585,6 @@ end CommSemiring
 section Ring
 
 variable [CommRing R]
-
 variable (R)
 
 /-- A `Semiring` that is an `Algebra` over a commutative ring carries a natural `Ring` structure.

Mathlib/Algebra/Algebra/Equiv.lean

@@ -89,10 +89,8 @@ section Semiring
 
 variable [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃]
 variable [Semiring A₁'] [Semiring A₂'] [Semiring A₃']
-
 variable [Algebra R A₁] [Algebra R A₂] [Algebra R A₃]
 variable [Algebra R A₁'] [Algebra R A₂'] [Algebra R A₃']
-
 variable (e : A₁ ≃ₐ[R] A₂)
 
 instance : EquivLike (A₁ ≃ₐ[R] A₂) A₁ A₂ where
@@ -818,7 +816,6 @@ end Semiring
 section CommSemiring
 
 variable [CommSemiring R] [CommSemiring A₁] [CommSemiring A₂]
-
 variable [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂)
 
 -- Porting note: Added nonrec
@@ -838,7 +835,6 @@ end CommSemiring
 section Ring
 
 variable [CommSemiring R] [Ring A₁] [Ring A₂]
-
 variable [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂)
 
 protected theorem map_neg (x) : e (-x) = -e x :=

Mathlib/Algebra/Algebra/Hom.lean

@@ -91,7 +91,6 @@ variable {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} {D : Type v₁}
 section Semiring
 
 variable [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Semiring D]
-
 variable [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D]
 
 -- Porting note: we don't port specialized `CoeFun` instances if there is `DFunLike` instead
@@ -452,7 +451,6 @@ end Semiring
 section CommSemiring
 
 variable [CommSemiring R] [CommSemiring A] [CommSemiring B]
-
 variable [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B)
 
 protected theorem map_multiset_prod (s : Multiset A) : φ s.prod = (s.map φ).prod :=
@@ -474,7 +472,6 @@ end CommSemiring
 section Ring
 
 variable [CommSemiring R] [Ring A] [Ring B]
-
 variable [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B)
 
 protected theorem map_neg (x) : φ (-x) = -φ x :=
@@ -548,7 +545,6 @@ end
 namespace Algebra
 
 variable (R : Type u) (A : Type v)
-
 variable [CommSemiring R] [Semiring A] [Algebra R A]
 
 /-- `AlgebraMap` as an `AlgHom`. -/
@@ -589,7 +585,6 @@ end Algebra
 namespace MulSemiringAction
 
 variable {M G : Type*} (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A]
-
 variable [Monoid M] [MulSemiringAction M A] [SMulCommClass M R A]
 
 /-- Each element of the monoid defines an algebra homomorphism.

Mathlib/Algebra/Algebra/NonUnitalHom.lean

@@ -114,11 +114,8 @@ end NonUnitalAlgHomClass
 namespace NonUnitalAlgHom
 
 variable {R A B C} [Monoid R]
-
 variable [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
-
 variable [NonUnitalNonAssocSemiring B] [DistribMulAction R B]
-
 variable [NonUnitalNonAssocSemiring C] [DistribMulAction R C]
 
 -- Porting note: Replaced with DFunLike instance

Mathlib/Algebra/Algebra/Operations.lean

@@ -70,13 +70,11 @@ end SubMulAction
 namespace Submodule
 
 variable {ι : Sort uι}
-
 variable {R : Type u} [CommSemiring R]
 
 section Ring
 
 variable {A : Type v} [Semiring A] [Algebra R A]
-
 variable (S T : Set A) {M N P Q : Submodule R A} {m n : A}
 
 /-- `1 : Submodule R A` is the submodule R of A. -/
@@ -204,7 +202,6 @@ theorem span_mul_span : span R S * span R T = span R (S * T) :=
 #align submodule.span_mul_span Submodule.span_mul_span
 
 variable {R}
-
 variable (M N P Q)
 
 @[simp]
@@ -625,7 +622,6 @@ end Ring
 section CommRing
 
 variable {A : Type v} [CommSemiring A] [Algebra R A]
-
 variable {M N : Submodule R A} {m n : A}
 
 theorem mul_mem_mul_rev (hm : m ∈ M) (hn : n ∈ N) : n * m ∈ M * N :=

Mathlib/Algebra/Algebra/Pi.lean

@@ -32,9 +32,7 @@ variable {R : Type*}
 
 -- The family of types already equipped with instances
 variable {f : I → Type v}
-
 variable (x y : ∀ i, f i) (i : I)
-
 variable (I f)
 
 instance algebra {r : CommSemiring R} [s : ∀ i, Semiring (f i)] [∀ i, Algebra R (f i)] :
@@ -104,9 +102,7 @@ instance Function.algebra {R : Type*} (I : Type*) (A : Type*) [CommSemiring R] [
 namespace AlgHom
 
 variable {R : Type u} {A : Type v} {B : Type w} {I : Type*}
-
 variable [CommSemiring R] [Semiring A] [Semiring B]
-
 variable [Algebra R A] [Algebra R B]
 
 /-- `R`-algebra homomorphism between the function spaces `I → A` and `I → B`, induced by an

Mathlib/Algebra/Algebra/Prod.lean

@@ -22,9 +22,7 @@ The R-algebra structure on `(i : I) → A i` when each `A i` is an R-algebra.
 
 
 variable {R A B C : Type*}
-
 variable [CommSemiring R]
-
 variable [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C]
 
 namespace Prod

Mathlib/Algebra/Algebra/Spectrum.lean

@@ -48,7 +48,6 @@ universe u v
 section Defs
 
 variable (R : Type u) {A : Type v}
-
 variable [CommSemiring R] [Ring A] [Algebra R A]
 
 local notation "↑ₐ" => algebraMap R A
@@ -97,7 +96,6 @@ namespace spectrum
 section ScalarSemiring
 
 variable {R : Type u} {A : Type v}
-
 variable [CommSemiring R] [Ring A] [Algebra R A]
 
 local notation "σ" => spectrum R
@@ -291,7 +289,6 @@ end ScalarSemiring
 section ScalarRing
 
 variable {R : Type u} {A : Type v}
-
 variable [CommRing R] [Ring A] [Algebra R A]
 
 local notation "σ" => spectrum R
@@ -340,7 +337,6 @@ end ScalarRing
 section ScalarField
 
 variable {𝕜 : Type u} {A : Type v}
-
 variable [Field 𝕜] [Ring A] [Algebra 𝕜 A]
 
 local notation "σ" => spectrum 𝕜
@@ -408,7 +404,6 @@ namespace AlgHom
 section CommSemiring
 
 variable {F R A B : Type*} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B]
-
 variable [FunLike F A B] [AlgHomClass F R A B]
 
 local notation "σ" => spectrum R
@@ -429,7 +424,6 @@ end CommSemiring
 section CommRing
 
 variable {F R A B : Type*} [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R B]
-
 variable [FunLike F A R] [AlgHomClass F R A R]
 
 local notation "σ" => spectrum R

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -38,9 +38,7 @@ add_decl_doc Subalgebra.toSubsemiring
 namespace Subalgebra
 
 variable {R' : Type u'} {R : Type u} {A : Type v} {B : Type w} {C : Type w'}
-
 variable [CommSemiring R]
-
 variable [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C]
 
 instance : SetLike (Subalgebra R A) A where
@@ -510,7 +508,6 @@ end Subalgebra
 namespace Submodule
 
 variable {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
-
 variable (p : Submodule R A)
 
 /-- A submodule containing `1` and closed under multiplication is a subalgebra. -/
@@ -560,11 +557,8 @@ end Submodule
 namespace AlgHom
 
 variable {R' : Type u'} {R : Type u} {A : Type v} {B : Type w} {C : Type w'}
-
 variable [CommSemiring R]
-
 variable [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C]
-
 variable (φ : A →ₐ[R] B)
 
 /-- Range of an `AlgHom` as a subalgebra. -/
@@ -665,7 +659,6 @@ end AlgHom
 namespace AlgEquiv
 
 variable {R : Type u} {A : Type v} {B : Type w}
-
 variable [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
 
 /-- Restrict an algebra homomorphism with a left inverse to an algebra isomorphism to its range.
@@ -726,7 +719,6 @@ end AlgEquiv
 namespace Algebra
 
 variable (R : Type u) {A : Type v} {B : Type w}
-
 variable [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
 
 /-- The minimal subalgebra that includes `s`. -/
@@ -950,9 +942,7 @@ namespace Subalgebra
 open Algebra
 
 variable {R : Type u} {A : Type v} {B : Type w}
-
 variable [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
-
 variable (S : Subalgebra R A)
 
 /-- The top subalgebra is isomorphic to the algebra.

Mathlib/Algebra/Algebra/Subalgebra/Tower.lean

@@ -38,9 +38,7 @@ variable (R : Type u) (S : Type v) (A : Type w) (B : Type u₁) (M : Type v₁)
 namespace Algebra
 
 variable [CommSemiring R] [Semiring A] [Algebra R A]
-
 variable [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M]
-
 variable {A}
 
 theorem lmul_algebraMap (x : R) : Algebra.lmul R A (algebraMap R A x) = Algebra.lsmul R R A x :=
@@ -54,7 +52,6 @@ namespace IsScalarTower
 section Semiring
 
 variable [CommSemiring R] [CommSemiring S] [Semiring A]
-
 variable [Algebra R S] [Algebra S A]
 
 instance subalgebra (S₀ : Subalgebra R S) : IsScalarTower S₀ S A :=
@@ -79,9 +76,7 @@ open IsScalarTower
 section Semiring
 
 variable {S A B} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B]
-
 variable [Algebra R S] [Algebra S A] [Algebra R A] [Algebra S B] [Algebra R B]
-
 variable [IsScalarTower R S A] [IsScalarTower R S B]
 
 /-- Given a tower `A / ↥U / S / R` of algebras, where `U` is an `S`-subalgebra of `A`, reinterpret
@@ -149,7 +144,6 @@ namespace IsScalarTower
 open Subalgebra
 
 variable [CommSemiring R] [CommSemiring S] [CommSemiring A]
-
 variable [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A]
 
 theorem adjoin_range_toAlgHom (t : Set A) :

Mathlib/Algebra/Algebra/Tower.lean

@@ -33,7 +33,6 @@ namespace Algebra
 variable [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
 variable [AddCommMonoid M] [Module R M] [Module A M] [Module B M]
 variable [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M]
-
 variable {A}
 
 
@@ -83,9 +82,7 @@ namespace IsScalarTower
 section Module
 
 variable [CommSemiring R] [Semiring A] [Algebra R A]
-
 variable [MulAction A M]
-
 variable {R} {M}
 
 theorem algebraMap_smul [SMul R M] [IsScalarTower R A M] (r : R) (x : M) :
@@ -107,9 +104,7 @@ end Module
 section Semiring
 
 variable [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B]
-
 variable [Algebra R S] [Algebra S A] [Algebra S B]
-
 variable {R S A}
 
 theorem of_algebraMap_eq [Algebra R A]
@@ -124,9 +119,7 @@ theorem of_algebraMap_eq' [Algebra R A]
 #align is_scalar_tower.of_algebra_map_eq' IsScalarTower.of_algebraMap_eq'
 
 variable (R S A)
-
 variable [Algebra R A] [Algebra R B]
-
 variable [IsScalarTower R S A] [IsScalarTower R S B]
 
 theorem algebraMap_eq : algebraMap R A = (algebraMap S A).comp (algebraMap R S) :=
@@ -199,13 +192,9 @@ end IsScalarTower
 section Homs
 
 variable [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B]
-
 variable [Algebra R S] [Algebra S A] [Algebra S B]
-
 variable [Algebra R A] [Algebra R B]
-
 variable [IsScalarTower R S A] [IsScalarTower R S B]
-
 variable {A S B}
 
 open IsScalarTower
@@ -271,9 +260,7 @@ end Homs
 namespace Submodule
 
 variable {M}
-
 variable [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M]
-
 variable [Module R M] [Module A M] [IsScalarTower R A M]
 
 /-- If `A` is an `R`-algebra such that the induced morphism `R →+* A` is surjective, then the
@@ -302,7 +289,6 @@ namespace Submodule
 section Module
 
 variable [Semiring R] [Semiring S] [AddCommMonoid A]
-
 variable [Module R S] [Module S A] [Module R A] [IsScalarTower R S A]
 
 open IsScalarTower
@@ -345,7 +331,6 @@ end Module
 section Algebra
 
 variable [CommSemiring R] [Semiring S] [AddCommMonoid A]
-
 variable [Algebra R S] [Module S A] [Module R A] [IsScalarTower R S A]
 
 /-- A variant of `Submodule.span_image` for `algebraMap`. -/