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

Proof state:
case e_s.h.mp
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
m : M
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → m ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
rintro ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩

Result:
case e_s.h.mp.intro.mk.intro.mk
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
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Proof state:
case e_s.h.mpr
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
m : M
⊢ m ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x} → m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rintro ⟨x, hx, n, hn, rfl⟩

Result:
case e_s.h.mpr.intro.intro.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
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ⁅x, n⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case e_s.h.mp.intro.mk.intro.mk
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
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
exact ⟨x, hx, n, hn, rfl⟩

Result:
no goals

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
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
congr

Result:
case e_s
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
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Proof state:
case e_s.h.mpr.intro.intro.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
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ⁅x, n⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
exact ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩

Result:
no goals

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
⊢ ↑⁅I, N⁆ = Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
rw [lieIdeal_oper_eq_linear_span]

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
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Proof state:
case e_s
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
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
ext m

Result:
case e_s.h
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
m : M
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ↔ m ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Proof state:
case e_s.h
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
m : M
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ↔ m ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
constructor

Result:
case e_s.h.mp
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
m : M
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → m ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

case e_s.h.mpr
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
m : M
⊢ m ∈ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x} → m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}