chore: backports for leanprover/lean4#4814 (part 25) (#15537)

Mathlib/Algebra/Lie/Submodule.lean

@@ -36,8 +36,8 @@ universe u v w w₁ w₂
 section LieSubmodule
 
 variable (R : Type u) (L : Type v) (M : Type w)
-variable [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M]
-variable [LieRingModule L M] [LieModule R L M]
+variable [CommRing R] [LieRing L] [AddCommGroup M] [Module R M]
+variable [LieRingModule L M]
 
 /-- A Lie submodule of a Lie module is a submodule that is closed under the Lie bracket.
 This is a sufficient condition for the subset itself to form a Lie module. -/
@@ -169,10 +169,6 @@ instance {S : Type*} [Semiring S] [SMul S R] [SMul Sᵐᵒᵖ R] [Module S M] [M
     [IsScalarTower S R M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] : IsCentralScalar S N :=
   N.toSubmodule.isCentralScalar
 
-instance instLieModule : LieModule R L N where
-  lie_smul := by intro t x y; apply SetCoe.ext; apply lie_smul
-  smul_lie := by intro t x y; apply SetCoe.ext; apply smul_lie
-
 @[simp, norm_cast]
 theorem coe_zero : ((0 : N) : M) = (0 : M) :=
   rfl
@@ -197,12 +193,19 @@ theorem coe_smul (t : R) (m : N) : (↑(t • m) : M) = t • (m : M) :=
 theorem coe_bracket (x : L) (m : N) : (↑⁅x, m⁆ : M) = ⁅x, ↑m⁆ :=
   rfl
 
+variable [LieAlgebra R L] [LieModule R L M]
+
+instance instLieModule : LieModule R L N where
+  lie_smul := by intro t x y; apply SetCoe.ext; apply lie_smul
+  smul_lie := by intro t x y; apply SetCoe.ext; apply smul_lie
+
 instance [Subsingleton M] : Unique (LieSubmodule R L M) :=
   ⟨⟨0⟩, fun _ ↦ (coe_toSubmodule_eq_iff _ _).mp (Subsingleton.elim _ _)⟩
 
 end LieSubmodule
 
 section LieIdeal
+variable [LieAlgebra R L] [LieModule R L M]
 
 /-- An ideal of a Lie algebra is a Lie submodule of the Lie algebra as a Lie module over itself. -/
 abbrev LieIdeal :=
@@ -265,6 +268,7 @@ theorem Submodule.exists_lieSubmodule_coe_eq_iff (p : Submodule R M) :
 namespace LieSubalgebra
 
 variable {L}
+variable [LieAlgebra R L]
 variable (K : LieSubalgebra R L)
 
 /-- Given a Lie subalgebra `K ⊆ L`, if we view `L` as a `K`-module by restriction, it contains
@@ -301,9 +305,9 @@ end LieSubmodule
 namespace LieSubmodule
 
 variable {R : Type u} {L : Type v} {M : Type w}
-variable [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M]
-variable [LieRingModule L M] [LieModule R L M]
-variable (N N' : LieSubmodule R L M) (I J : LieIdeal R L)
+variable [CommRing R] [LieRing L] [AddCommGroup M] [Module R M]
+variable [LieRingModule L M]
+variable (N N' : LieSubmodule R L M)
 
 section LatticeStructure
 
@@ -741,9 +745,9 @@ end LieSubmodule
 section LieSubmoduleMapAndComap
 
 variable {R : Type u} {L : Type v} {L' : Type w₂} {M : Type w} {M' : Type w₁}
-variable [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L']
-variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
-variable [AddCommGroup M'] [Module R M'] [LieRingModule L M'] [LieModule R L M']
+variable [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L']
+variable [AddCommGroup M] [Module R M] [LieRingModule L M]
+variable [AddCommGroup M'] [Module R M'] [LieRingModule L M']
 
 namespace LieSubmodule
 
@@ -884,6 +888,7 @@ Submodules. -/
 end LieSubmodule
 
 namespace LieIdeal
+variable [LieAlgebra R L] [LieModule R L M] [LieModule R L M']
 
 variable (f : L →ₗ⁅R⁆ L') (I I₂ : LieIdeal R L) (J : LieIdeal R L')
 
@@ -988,7 +993,7 @@ instance subsingleton_of_bot : Subsingleton (LieIdeal R (⊥ : LieIdeal R L)) :=
 end LieIdeal
 
 namespace LieHom
-
+variable [LieAlgebra R L] [LieModule R L M] [LieModule R L M']
 variable (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (J : LieIdeal R L')
 
 /-- The kernel of a morphism of Lie algebras, as an ideal in the domain. -/
@@ -1090,7 +1095,7 @@ theorem isIdealMorphism_of_surjective (h : Function.Surjective f) : f.IsIdealMor
 end LieHom
 
 namespace LieIdeal
-
+variable [LieAlgebra R L] [LieModule R L M] [LieModule R L M']
 variable {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {J : LieIdeal R L'}
 
 @[simp]
@@ -1223,9 +1228,9 @@ end LieSubmoduleMapAndComap
 namespace LieModuleHom
 
 variable {R : Type u} {L : Type v} {M : Type w} {N : Type w₁}
-variable [CommRing R] [LieRing L] [LieAlgebra R L]
-variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
-variable [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N]
+variable [CommRing R] [LieRing L]
+variable [AddCommGroup M] [Module R M] [LieRingModule L M]
+variable [AddCommGroup N] [Module R N] [LieRingModule L N]
 variable (f : M →ₗ⁅R,L⁆ N)
 
 /-- The kernel of a morphism of Lie algebras, as an ideal in the domain. -/
@@ -1299,8 +1304,8 @@ end LieModuleHom
 namespace LieSubmodule
 
 variable {R : Type u} {L : Type v} {M : Type w}
-variable [CommRing R] [LieRing L] [LieAlgebra R L]
-variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
+variable [CommRing R] [LieRing L]
+variable [AddCommGroup M] [Module R M] [LieRingModule L M]
 variable (N : LieSubmodule R L M)
 
 @[simp]
@@ -1339,8 +1344,30 @@ end LieSubmodule
 
 section TopEquiv
 
-variable {R : Type u} {L : Type v}
-variable [CommRing R] [LieRing L] [LieAlgebra R L]
+variable (R : Type u) (L : Type v)
+variable [CommRing R] [LieRing L]
+
+variable (M : Type*) [AddCommGroup M] [Module R M] [LieRingModule L M]
+
+/-- The natural equivalence between the 'top' Lie submodule and the enclosing Lie module. -/
+def LieModuleEquiv.ofTop : (⊤ : LieSubmodule R L M) ≃ₗ⁅R,L⁆ M :=
+  { LinearEquiv.ofTop ⊤ rfl with
+    map_lie' := rfl }
+
+variable {R L}
+
+-- This lemma has always been bad, but leanprover/lean4#2644 made `simp` start noticing
+@[simp, nolint simpNF] lemma LieModuleEquiv.ofTop_apply (x : (⊤ : LieSubmodule R L M)) :
+    LieModuleEquiv.ofTop R L M x = x :=
+  rfl
+
+@[simp] lemma LieModuleEquiv.range_coe {M' : Type*}
+    [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') :
+    LieModuleHom.range (e : M →ₗ⁅R,L⁆ M') = ⊤ := by
+  rw [LieModuleHom.range_eq_top]
+  exact e.surjective
+
+variable [LieAlgebra R L] [LieModule R L M]
 
 /-- The natural equivalence between the 'top' Lie subalgebra and the enclosing Lie algebra.
 
@@ -1366,23 +1393,4 @@ def LieIdeal.topEquiv : (⊤ : LieIdeal R L) ≃ₗ⁅R⁆ L :=
 theorem LieIdeal.topEquiv_apply (x : (⊤ : LieIdeal R L)) : LieIdeal.topEquiv x = x :=
   rfl
 
-variable (R L)
-variable (M : Type*) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
-
-/-- The natural equivalence between the 'top' Lie submodule and the enclosing Lie module. -/
-def LieModuleEquiv.ofTop : (⊤ : LieSubmodule R L M) ≃ₗ⁅R,L⁆ M :=
-  { LinearEquiv.ofTop ⊤ rfl with
-    map_lie' := rfl }
-
--- This lemma has always been bad, but leanprover/lean4#2644 made `simp` start noticing
-@[simp, nolint simpNF] lemma LieModuleEquiv.ofTop_apply (x : (⊤ : LieSubmodule R L M)) :
-    LieModuleEquiv.ofTop R L M x = x :=
-  rfl
-
-@[simp] lemma LieModuleEquiv.range_coe {M' : Type*}
-    [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') :
-    LieModuleHom.range (e : M →ₗ⁅R,L⁆ M') = ⊤ := by
-  rw [LieModuleHom.range_eq_top]
-  exact e.surjective
-
 end TopEquiv

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

@@ -112,7 +112,7 @@ local macro "pderiv_simp" : tactic =>
     pderiv_X_of_ne (by decide : z ≠ x), pderiv_X_of_ne (by decide : x ≠ z),
     pderiv_X_of_ne (by decide : z ≠ y), pderiv_X_of_ne (by decide : y ≠ z)])
 
-variable {R : Type u} [CommRing R] {W' : Jacobian R} {F : Type v} [Field F] {W : Jacobian F}
+variable {R : Type u} {W' : Jacobian R} {F : Type v} [Field F] {W : Jacobian F}
 
 section Jacobian
 
@@ -127,6 +127,8 @@ lemma fin3_def_ext (X Y Z : R) : ![X, Y, Z] x = X ∧ ![X, Y, Z] y = Y ∧ ![X,
 lemma comp_fin3 {S} (f : R → S) (X Y Z : R) : f ∘ ![X, Y, Z] = ![f X, f Y, f Z] :=
   (FinVec.map_eq _ _).symm
 
+variable [CommRing R]
+
 /-- The scalar multiplication on a point representative. -/
 scoped instance instSMulPoint : SMul R <| Fin 3 → R :=
   ⟨fun u P => ![u ^ 2 * P x, u ^ 3 * P y, u * P z]⟩
@@ -224,6 +226,8 @@ lemma Y_eq_iff {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) :
 
 end Jacobian
 
+variable [CommRing R]
+
 section Equation
 
 /-! ### Weierstrass equations -/

Mathlib/Analysis/InnerProductSpace/Orientation.lean

@@ -44,7 +44,7 @@ open scoped RealInnerProductSpace
 
 namespace OrthonormalBasis
 
-variable {ι : Type*} [Fintype ι] [DecidableEq ι] [ne : Nonempty ι] (e f : OrthonormalBasis ι ℝ E)
+variable {ι : Type*} [Fintype ι] [DecidableEq ι] (e f : OrthonormalBasis ι ℝ E)
   (x : Orientation ℝ E ι)
 
 /-- The change-of-basis matrix between two orthonormal bases with the same orientation has
@@ -90,6 +90,8 @@ theorem det_eq_neg_det_of_opposite_orientation (h : e.toBasis.orientation ≠ f.
   simp [e.det_to_matrix_orthonormalBasis_of_opposite_orientation f h,
     neg_one_smul ℝ (M := E [⋀^ι]→ₗ[ℝ] ℝ)]
 
+variable [Nonempty ι]
+
 section AdjustToOrientation
 
 /-- `OrthonormalBasis.adjustToOrientation`, applied to an orthonormal basis, preserves the

Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean

@@ -192,9 +192,8 @@ noncomputable section Seminormed
 
 section Ring
 variable [SeminormedCommRing S] [SeminormedRing R] [SeminormedAddCommGroup M]
-variable [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M]
-variable [BoundedSMul S R] [BoundedSMul S M] [BoundedSMul R M] [BoundedSMul Rᵐᵒᵖ M]
-variable [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M]
+variable [Algebra S R] [Module S M]
+variable [BoundedSMul S R] [BoundedSMul S M]
 
 instance instL1SeminormedAddCommGroup : SeminormedAddCommGroup (tsze R M) :=
   inferInstanceAs <| SeminormedAddCommGroup (WithLp 1 <| R × M)
@@ -217,6 +216,9 @@ theorem nnnorm_def (x : tsze R M) : ‖x‖₊ = ‖fst x‖₊ + ‖snd x‖₊
 @[simp] theorem nnnorm_inl (r : R) : ‖(inl r : tsze R M)‖₊ = ‖r‖₊ := by simp [nnnorm_def]
 @[simp] theorem nnnorm_inr (m : M) : ‖(inr m : tsze R M)‖₊ = ‖m‖₊ := by simp [nnnorm_def]
 
+variable [Module R M] [BoundedSMul R M] [Module Rᵐᵒᵖ M] [BoundedSMul Rᵐᵒᵖ M]
+  [SMulCommClass R Rᵐᵒᵖ M]
+
 instance instL1SeminormedRing : SeminormedRing (tsze R M) where
   norm_mul
   | ⟨r₁, m₁⟩, ⟨r₂, m₂⟩ => by

Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean

@@ -24,7 +24,7 @@ non-unital Banach algebra is compact, which can be established by passing to the
 -/
 
 variable (𝕜 A : Type*) [NormedField 𝕜] [NonUnitalNormedRing A]
-variable [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A]
+variable [NormedSpace 𝕜 A]
 
 namespace WithLp
 
@@ -79,6 +79,8 @@ lemma unitization_isometry_inr :
     ((WithLp.linearEquiv 1 𝕜 (Unitization 𝕜 A)).symm.comp <| Unitization.inrHom 𝕜 A)
     unitization_norm_inr
 
+variable [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A]
+
 instance instUnitizationRing : Ring (WithLp 1 (Unitization 𝕜 A)) :=
   inferInstanceAs (Ring (Unitization 𝕜 A))
 

Mathlib/Analysis/Normed/Lp/PiLp.lean

@@ -92,7 +92,7 @@ section
 for Pi types will not trigger. -/
 variable {𝕜 p α}
 variable [SeminormedRing 𝕜] [∀ i, SeminormedAddCommGroup (β i)]
-variable [∀ i, Module 𝕜 (β i)] [∀ i, BoundedSMul 𝕜 (β i)] (c : 𝕜)
+variable [∀ i, Module 𝕜 (β i)] (c : 𝕜)
 variable (x y : PiLp p β) (i : ι)
 
 #adaptation_note
@@ -744,7 +744,7 @@ variable {ι : Type*} {κ : ι → Type*} (p : ℝ≥0∞) [Fact (1 ≤ p)]
 
 variable (𝕜) in
 /-- `LinearEquiv.piCurry` for `PiLp`, as an isometry. -/
-def _root_.LinearIsometryEquiv.piLpCurry  :
+def _root_.LinearIsometryEquiv.piLpCurry :
     PiLp p (fun i : Sigma _ => α i.1 i.2) ≃ₗᵢ[𝕜] PiLp p (fun i => PiLp p (α i)) where
   toLinearEquiv :=
     WithLp.linearEquiv _ _ _

Mathlib/Analysis/NormedSpace/DualNumber.lean

@@ -25,7 +25,7 @@ open TrivSqZeroExt
 
 variable (𝕜 : Type*) {R : Type*}
 variable [Field 𝕜] [CharZero 𝕜] [CommRing R] [Algebra 𝕜 R]
-variable [UniformSpace R] [TopologicalRing R] [CompleteSpace R] [T2Space R]
+variable [UniformSpace R] [TopologicalRing R] [T2Space R]
 
 @[simp]
 theorem exp_eps : exp 𝕜 (eps : DualNumber R) = 1 + eps :=

Mathlib/Combinatorics/Additive/Corner/Roth.lean

@@ -23,7 +23,7 @@ open Finset SimpleGraph TripartiteFromTriangles
 open Function hiding graph
 open Fintype (card)
 
-variable {G : Type*} [AddCommGroup G] [Fintype G] {A B : Finset (G × G)}
+variable {G : Type*} [AddCommGroup G] {A B : Finset (G × G)}
   {a b c d x y : G} {n : ℕ} {ε : ℝ}
 
 namespace Corners
@@ -55,7 +55,7 @@ private lemma noAccidental (hs : IsCornerFree (A : Set (G × G))) :
     simp only [mk_mem_triangleIndices] at ha hb hc
     exact .inl $ hs ⟨hc.1, hb.1, ha.1, hb.2.symm.trans ha.2⟩
 
-private lemma farFromTriangleFree_graph [DecidableEq G] (hε : ε * card G ^ 2 ≤ A.card) :
+private lemma farFromTriangleFree_graph [Fintype G] [DecidableEq G] (hε : ε * card G ^ 2 ≤ A.card) :
     (graph <| triangleIndices A).FarFromTriangleFree (ε / 9) := by
   refine farFromTriangleFree _ ?_
   simp_rw [card_triangleIndices, mul_comm_div, Nat.cast_pow, Nat.cast_add]
@@ -64,6 +64,8 @@ private lemma farFromTriangleFree_graph [DecidableEq G] (hε : ε * card G ^ 2 
 
 end Corners
 
+variable [Fintype G]
+
 open Corners
 
 

Mathlib/FieldTheory/Perfect.lean

@@ -290,6 +290,7 @@ theorem roots_expand_image_frobenius_subset [DecidableEq R] :
   convert ← roots_expand_pow_image_iterateFrobenius_subset p 1 f
   apply pow_one
 
+section PerfectRing
 variable {p n f}
 variable [PerfectRing R p]
 
@@ -342,7 +343,9 @@ theorem roots_expand_image_frobenius [DecidableEq R] :
   rw [Finset.image_toFinset, roots_expand_map_frobenius,
       (roots f).toFinset_nsmul _ (expChar_pos R p).ne']
 
-variable (p n f) [DecidableEq R]
+end PerfectRing
+
+variable [DecidableEq R]
 
 /-- If `f` is a polynomial over an integral domain `R` of characteristic `p`, then there is
 a map from the set of roots of `Polynomial.expand R p f` to the set of roots of `f`.
@@ -367,6 +370,8 @@ noncomputable def rootsExpandPowToRoots :
 @[simp]
 theorem rootsExpandPowToRoots_apply (x) : (rootsExpandPowToRoots p n f x : R) = x ^ p ^ n := rfl
 
+variable [PerfectRing R p]
+
 /-- If `f` is a polynomial over a perfect integral domain `R` of characteristic `p`, then there is
 a bijection from the set of roots of `Polynomial.expand R p f` to the set of roots of `f`.
 It's given by `x ↦ x ^ p`, see `rootsExpandEquivRoots_apply`. -/

Mathlib/Geometry/Manifold/InteriorBoundary.lean

@@ -159,7 +159,7 @@ variable {I}
   {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
   {H' : Type*} [TopologicalSpace H']
   {N : Type*} [TopologicalSpace N] [ChartedSpace H' N]
-  (J : ModelWithCorners 𝕜 E' H') [SmoothManifoldWithCorners J N] {x : M} {y : N}
+  (J : ModelWithCorners 𝕜 E' H') {x : M} {y : N}
 
 /-- The interior of `M × N` is the product of the interiors of `M` and `N`. -/
 lemma ModelWithCorners.interior_prod :

Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

@@ -31,9 +31,11 @@ section CommRing
 variable [CommRing R] [CommRing A]
 variable [AddCommGroup M₁] [AddCommGroup M₂]
 variable [Algebra R A] [Module R M₁] [Module A M₁]
-variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁]
-variable [Module R M₂] [Invertible (2 : R)]
+variable [SMulCommClass R A M₁] [IsScalarTower R A M₁]
+variable [Module R M₂]
 
+section InvertibleTwo
+variable [Invertible (2 : R)]
 
 variable (R A) in
 /-- The tensor product of two quadratic forms injects into quadratic forms on tensor products.
@@ -106,6 +108,8 @@ theorem polarBilin_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) :
     ← LinearMap.map_smul, smul_tmul', ← two_nsmul_associated R, coe_associatedHom, associated_sq,
     smul_comm, ← smul_assoc, two_smul, invOf_two_add_invOf_two, one_smul]
 
+end InvertibleTwo
+
 /-- If two quadratic forms from `A ⊗[R] M₂` agree on elements of the form `1 ⊗ m`, they are equal.
 
 In other words, if a base change exists for a quadratic form, it is unique.