doc: Change old Lean 3 commands to Lean 4 in implementation notes (#1…

…0707)

I changed Lean's 3 old "variables" command to Lean's 4 command "variable" in some implementation notes.
I might have missed some

Co-authored-by: Omar Mohsen <36500353+OmarMohsenGit@users.noreply.github.com>

Mathlib/Algebra/Algebra/Basic.lean

@@ -56,12 +56,12 @@ structure morphism `algebraMap R A r * x`.
 
 As a result, there are two ways to talk about an `R`-algebra `A` when `A` is a semiring:
 1. ```lean
-   variables [CommSemiring R] [Semiring A]
-   variables [Algebra R A]
+   variable [CommSemiring R] [Semiring A]
+   variable [Algebra R A]
    ```
 2. ```lean
-   variables [CommSemiring R] [Semiring A]
-   variables [Module R A] [SMulCommClass R A A] [IsScalarTower R A A]
+   variable [CommSemiring R] [Semiring A]
+   variable [Module R A] [SMulCommClass R A A] [IsScalarTower R A A]
    ```
 
 The first approach implies the second via typeclass search; so any lemma stated with the second set

Mathlib/Algebra/Invertible/Defs.lean

@@ -40,7 +40,7 @@ users can choose which instances to use at the point of use.
 
 For example, here's how you can use an `Invertible 1` instance:
 ```lean
-variables {α : Type*} [Monoid α]
+variable {α : Type*} [Monoid α]
 
 def something_that_needs_inverses (x : α) [Invertible x] := sorry
 

Mathlib/Algebra/Jordan/Basic.lean

@@ -28,7 +28,7 @@ Jordan algebras arising this way are said to be special.
 
 A real Jordan algebra `A` can be introduced by
 ```lean
-variables {A : Type*} [NonUnitalNonAssocRing A] [Module ℝ A] [SMulCommClass ℝ A A]
+variable {A : Type*} [NonUnitalNonAssocRing A] [Module ℝ A] [SMulCommClass ℝ A A]
   [IsScalarTower ℝ A A] [IsCommJordan A]
 ```
 

Mathlib/Algebra/Module/Bimodule.lean

@@ -18,8 +18,8 @@ and `S` acting contravariantly ("on the right"). The compatibility condition is
 
 This situation can be set up in Mathlib as:
 ```lean
-variables (R S M : Type*) [Ring R] [Ring S]
-variables [AddCommGroup M] [Module R M] [Module Sᵐᵒᵖ M] [SMulCommClass R Sᵐᵒᵖ M]
+variable (R S M : Type*) [Ring R] [Ring S]
+variable [AddCommGroup M] [Module R M] [Module Sᵐᵒᵖ M] [SMulCommClass R Sᵐᵒᵖ M]
 ```
 The key fact is:
 ```lean

Mathlib/Algebra/TrivSqZeroExt.lean

@@ -21,13 +21,13 @@ It is a square-zero extension because `M^2 = 0`.
 Note that expressing this requires bimodules; we write these in general for a
 not-necessarily-commutative `R` as:
 ```lean
-variables {R M : Type*} [Semiring R] [AddCommMonoid M]
-variables [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
+variable {R M : Type*} [Semiring R] [AddCommMonoid M]
+variable [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
 ```
 If we instead work with a commutative `R'` acting symmetrically on `M`, we write
 ```lean
-variables {R' M : Type*} [CommSemiring R'] [AddCommMonoid M]
-variables [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M]
+variable {R' M : Type*} [CommSemiring R'] [AddCommMonoid M]
+variable [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M]
 ```
 noting that in this context `IsCentralScalar R' M` implies `SMulCommClass R' R'ᵐᵒᵖ M`.
 

Mathlib/Analysis/NormedSpace/Basic.lean

@@ -265,8 +265,8 @@ section NormedAlgebra
 See the implementation notes for `Algebra` for a discussion about non-unital algebras. Following
 the strategy there, a non-unital *normed* algebra can be written as:
 ```lean
-variables [NormedField 𝕜] [NonUnitalSeminormedRing 𝕜']
-variables [NormedSpace 𝕜 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜']
+variable [NormedField 𝕜] [NonUnitalSeminormedRing 𝕜']
+variable [NormedSpace 𝕜 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜']
 ```
 -/
 class NormedAlgebra (𝕜 : Type*) (𝕜' : Type*) [NormedField 𝕜] [SeminormedRing 𝕜'] extends

Mathlib/MeasureTheory/Function/L1Space.lean

@@ -434,7 +434,7 @@ end NormedSpace
 /-! ### The predicate `Integrable` -/
 
 
--- variables [measurable_space β] [measurable_space γ] [measurable_space δ]
+-- variable [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ]
 /-- `Integrable f μ` means that `f` is measurable and that the integral `∫⁻ a, ‖f a‖ ∂μ` is finite.
   `Integrable f` means `Integrable f volume`. -/
 def Integrable {α} {_ : MeasurableSpace α} (f : α → β) (μ : Measure α := by volume_tac) : Prop :=

Mathlib/Topology/Basic.lean

@@ -1841,7 +1841,7 @@ However, lemmas with this conclusion are not nice to use in practice because
 1. They confuse the elaborator. The following two examples fail, because of limitations in the
   elaboration process.
   ```
-  variables {M : Type*} [Add M] [TopologicalSpace M] [ContinuousAdd M]
+  variable {M : Type*} [Add M] [TopologicalSpace M] [ContinuousAdd M]
   example : Continuous (λ x : M, x + x) :=
   continuous_add.comp _