-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem coe_lowerCentralSeries_eq_int_aux (R₁ R₂ L M : Type*)
    [CommRing R₁] [CommRing R₂] [AddCommGroup M]
    [LieRing L] [LieAlgebra R₁ L] [LieAlgebra R₂ L] [Module R₁ M] [Module R₂ M] [LieRingModule L M]
    [LieModule R₁ L M] (k : ℕ) :
    let I := lowerCentralSeries R₂ L M k; let S : Set M := {⁅a, b⁆ | (a : L) (b ∈ I)}
    (Submodule.span R₁ S : Set M) ≤ (Submodule.span R₂ S : Set M)

Proof state:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
hx : x ∈ ↑(Submodule.span R₁ S)
⊢ x ∈ ↑(Submodule.span R₂ S)

Tactic:
simp only [SetLike.mem_coe] at hx ⊢

Result:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
hx : x ∈ Submodule.span R₁ S
⊢ x ∈ Submodule.span R₂ S

Proof state:
case zero
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
⊢ 0 ∈ Submodule.span R₂ S

Tactic:
exact Submodule.zero_mem _

Result:
no goals

Proof state:
case smul_mem.intro.intro.intro
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
c : R₁
a : L
b : M
hb : b ∈ I
⊢ ⁅c • a, b⁆ ∈ Submodule.span R₂ S

Tactic:
exact Submodule.subset_span ⟨c • a, b, hb, rfl⟩

Result:
no goals

Proof state:
case smul_mem.intro.intro.intro
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
c : R₁
a : L
b : M
hb : b ∈ I
⊢ c • ⁅a, b⁆ ∈ Submodule.span R₂ S

Tactic:
rw [← smul_lie]

Result:
case smul_mem.intro.intro.intro
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
c : R₁
a : L
b : M
hb : b ∈ I
⊢ ⁅c • a, b⁆ ∈ Submodule.span R₂ S

Proof state:
case add
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x y z : M
hy₁ : y ∈ Submodule.span R₁ S
hz₁ : z ∈ Submodule.span R₁ S
hy₂ : y ∈ Submodule.span R₂ S
hz₂ : z ∈ Submodule.span R₂ S
⊢ y + z ∈ Submodule.span R₂ S

Tactic:
exact Submodule.add_mem _ hy₂ hz₂

Result:
no goals

Proof state:
case smul_mem
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
c : R₁
y : M
hy : y ∈ S
⊢ c • y ∈ Submodule.span R₂ S

Tactic:
obtain ⟨a, b, hb, rfl⟩ := hy

Result:
case smul_mem.intro.intro.intro
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
c : R₁
a : L
b : M
hb : b ∈ I
⊢ c • ⁅a, b⁆ ∈ Submodule.span R₂ S

Proof state:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
⊢ let I := lowerCentralSeries R₂ L M k;
  let S := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x};
  ↑(Submodule.span R₁ S) ≤ ↑(Submodule.span R₂ S)

Tactic:
intro I S x hx

Result:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
hx : x ∈ ↑(Submodule.span R₁ S)
⊢ x ∈ ↑(Submodule.span R₂ S)

Proof state:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
hx : x ∈ Submodule.span R₁ S
⊢ x ∈ Submodule.span R₂ S

Tactic:
induction hx using Submodule.closure_induction with
| zero => exact Submodule.zero_mem _
| add y z hy₁ hz₁ hy₂ hz₂ => exact Submodule.add_mem _ hy₂ hz₂
| smul_mem c y hy =>
    obtain ⟨a, b, hb, rfl⟩ := hy
    rw [← smul_lie]
    exact Submodule.subset_span ⟨c • a, b, hb, rfl⟩

Result:
no goals