-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem lieIdeal_oper_eq_linear_span [LieModule R L M] :
    (↑⁅I, N⁆ : Submodule R M) = Submodule.span R { ⁅(x : L), (n : M)⁆ | (x : I) (n : N) }

Proof state:
case refine_1.intro.intro.refine_2.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅↑x, ↑n⁆ = m''
⊢ ⁅↑x, ⁅y, ↑n⁆⁆ ∈ s

Tactic:
use x, ⟨⁅y, ↑n⁆, N.lie_mem n.property⟩

Result:
no goals

Proof state:
case refine_1.intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅↑x, ↑n⁆ = m''
⊢ ⁅y, m''⁆ ∈ Submodule.span R s

Tactic:
rw [← hm'', leibniz_lie]

Result:
case refine_1.intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅↑x, ↑n⁆ = m''
⊢ ⁅⁅y, ↑x⁆, ↑n⁆ + ⁅↑x, ⁅y, ↑n⁆⁆ ∈ Submodule.span R s

Proof state:
case a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
aux : ∀ (y : L), ∀ m' ∈ Submodule.span R s, ⁅y, m'⁆ ∈ Submodule.span R s
⊢ ⁅I, N⁆ ≤
    let __src := Submodule.span R s;
    { toSubmodule := __src, lie_mem := ⋯ }

Tactic:
rw [lieIdeal_oper_eq_span, lieSpan_le]

Result:
case a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
aux : ∀ (y : L), ∀ m' ∈ Submodule.span R s, ⁅y, m'⁆ ∈ Submodule.span R s
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆
    ↑(let __src := Submodule.span R s;
      { toSubmodule := __src, lie_mem := ⋯ })

Proof state:
case refine_3
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
⊢ ∀ (x y_1 : M) (hx : x ∈ Submodule.span R s) (hy : y_1 ∈ Submodule.span R s),
    (fun m' x => ⁅y, m'⁆ ∈ Submodule.span R s) x hx →
      (fun m' x => ⁅y, m'⁆ ∈ Submodule.span R s) y_1 hy → (fun m' x => ⁅y, m'⁆ ∈ Submodule.span R s) (x + y_1) ⋯

Tactic:
intro m₁ m₂ _ _ hm₁ hm₂

Result:
case refine_3
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m₁ m₂ : M
hx✝ : m₁ ∈ Submodule.span R s
hy✝ : m₂ ∈ Submodule.span R s
hm₁ : ⁅y, m₁⁆ ∈ Submodule.span R s
hm₂ : ⁅y, m₂⁆ ∈ Submodule.span R s
⊢ ⁅y, m₁ + m₂⁆ ∈ Submodule.span R s

Proof state:
case a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ ↑⁅I, N⁆

Tactic:
rw [lieIdeal_oper_eq_span]

Result:
case a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ ↑(lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x})

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ ∀ (y : L), ∀ m' ∈ Submodule.span R s, ⁅y, m'⁆ ∈ Submodule.span R s

Tactic:
intro y m' hm'

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
⊢ ⁅y, m'⁆ ∈ Submodule.span R s

Proof state:
case refine_4
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
t : R
m'' : M
hx✝ : m'' ∈ Submodule.span R s
hm'' : ⁅y, m''⁆ ∈ Submodule.span R s
⊢ ⁅y, t • m''⁆ ∈ Submodule.span R s

Tactic:
rw [lie_smul]

Result:
case refine_4
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
t : R
m'' : M
hx✝ : m'' ∈ Submodule.span R s
hm'' : ⁅y, m''⁆ ∈ Submodule.span R s
⊢ t • ⁅y, m''⁆ ∈ Submodule.span R s

Proof state:
case a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
aux : ∀ (y : L), ∀ m' ∈ Submodule.span R s, ⁅y, m'⁆ ∈ Submodule.span R s
⊢ ↑⁅I, N⁆ ≤ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
change _ ≤ ({ Submodule.span R s with lie_mem := fun hm' => aux _ _ hm' } : LieSubmodule R L M)

Result:
case a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
aux : ∀ (y : L), ∀ m' ∈ Submodule.span R s, ⁅y, m'⁆ ∈ Submodule.span R s
⊢ ⁅I, N⁆ ≤
    let __src := Submodule.span R s;
    { toSubmodule := __src, lie_mem := ⋯ }

Proof state:
case a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
aux : ∀ (y : L), ∀ m' ∈ Submodule.span R s, ⁅y, m'⁆ ∈ Submodule.span R s
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆
    ↑(let __src := Submodule.span R s;
      { toSubmodule := __src, lie_mem := ⋯ })

Tactic:
exact Submodule.subset_span

Result:
no goals