-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem coe_lowerCentralSeries_eq_int [LieModule R L M] (k : ℕ) :
    (lowerCentralSeries R L M k : Set M) = (lowerCentralSeries ℤ L M k : Set M)

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ↑↑(lowerCentralSeries R L M k) = ↑↑(lowerCentralSeries ℤ L M k)
⊢ ↑↑⁅⊤, lowerCentralSeries R L M k⁆ = ↑↑⁅⊤, lowerCentralSeries ℤ L M k⁆

Tactic:
rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']

Result:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ↑↑(lowerCentralSeries R L M k) = ↑↑(lowerCentralSeries ℤ L M k)
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
⊢ ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries ℤ L M k)

Tactic:
rw [← LieSubmodule.coe_toSubmodule, ← LieSubmodule.coe_toSubmodule]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
⊢ ↑↑(lowerCentralSeries R L M k) = ↑↑(lowerCentralSeries ℤ L M k)

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ↑↑(lowerCentralSeries R L M k) = ↑↑(lowerCentralSeries ℤ L M k)
⊢ ↑↑(lowerCentralSeries R L M (k + 1)) = ↑↑(lowerCentralSeries ℤ L M (k + 1))

Tactic:
rw [lowerCentralSeries_succ, lowerCentralSeries_succ]

Result:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ↑↑(lowerCentralSeries R L M k) = ↑↑(lowerCentralSeries ℤ L M k)
⊢ ↑↑⁅⊤, lowerCentralSeries R L M k⁆ = ↑↑⁅⊤, lowerCentralSeries ℤ L M k⁆

Proof state:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ ↑↑(lowerCentralSeries R L M 0) = ↑↑(lowerCentralSeries ℤ L M 0)

Tactic:
rfl

Result:
no goals

Proof state:
case succ.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (x : M), x ∈ lowerCentralSeries R L M k ↔ x ∈ lowerCentralSeries ℤ L M k
⊢ ↑(Submodule.span ℤ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}) ≤
    ↑(Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x})

Tactic:
exact coe_lowerCentralSeries_eq_int_aux _ _ L M k

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (x : M), x ∈ lowerCentralSeries R L M k ↔ x ∈ lowerCentralSeries ℤ L M k
⊢ ↑(Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Tactic:
apply le_antisymm

Result:
case succ.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (x : M), x ∈ lowerCentralSeries R L M k ↔ x ∈ lowerCentralSeries ℤ L M k
⊢ ↑(Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x}) ≤
    ↑(Submodule.span ℤ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

case succ.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (x : M), x ∈ lowerCentralSeries R L M k ↔ x ∈ lowerCentralSeries ℤ L M k
⊢ ↑(Submodule.span ℤ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x}) ≤
    ↑(Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (x : M), x ∈ ↑↑(lowerCentralSeries R L M k) ↔ x ∈ ↑↑(lowerCentralSeries ℤ L M k)
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Tactic:
simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih

Result:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (x : M), x ∈ lowerCentralSeries R L M k ↔ x ∈ lowerCentralSeries ℤ L M k
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ↑↑(lowerCentralSeries R L M k) = ↑↑(lowerCentralSeries ℤ L M k)
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Tactic:
rw [Set.ext_iff] at ih

Result:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (x : M), x ∈ ↑↑(lowerCentralSeries R L M k) ↔ x ∈ ↑↑(lowerCentralSeries ℤ L M k)
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Proof state:
case succ.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (x : M), x ∈ lowerCentralSeries R L M k ↔ x ∈ lowerCentralSeries ℤ L M k
⊢ ↑(Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x}) ≤
    ↑(Submodule.span ℤ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Tactic:
exact coe_lowerCentralSeries_eq_int_aux _ _ L M k

Result:
no goals