-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem bot_lie : ⁅(⊥ : LieIdeal R L), N⁆ = ⊥

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
this : ⁅⊥, N⁆ ≤ ⊥
⊢ ⁅⊥, N⁆ = ⊥

Tactic:
exact le_bot_iff.mp this

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
⊢ ⁅⊥, N⁆ = ⊥

Tactic:
suffices ⁅(⊥ : LieIdeal R L), N⁆ ≤ ⊥ by exact le_bot_iff.mp this

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
⊢ ⁅⊥, N⁆ ≤ ⊥

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
⊢ ⁅⊥, N⁆ ≤ ⊥

Tactic:
rw [lieIdeal_oper_eq_span, lieSpan_le]

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
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑⊥

Proof state:
case intro.mk.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
m : M
x : L
n : ↥N
hx✝ : x ∈ ⊥
hx : x = 0
hn : ⁅↑⟨x, hx✝⟩, ↑n⁆ = m
⊢ ⁅↑⟨x, hx✝⟩, ↑n⁆ ∈ ↑⊥

Tactic:
simp [hx]

Result:
no goals

Proof state:
case intro.mk.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
m : M
x : L
n : ↥N
hx : x ∈ ⊥
hn : ⁅↑⟨x, hx⟩, ↑n⁆ = m
⊢ ⁅↑⟨x, hx⟩, ↑n⁆ ∈ ↑⊥

Tactic:
rw [mem_bot] at hx

Result:
case intro.mk.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
m : M
x : L
n : ↥N
hx✝ : x ∈ ⊥
hx : x = 0
hn : ⁅↑⟨x, hx✝⟩, ↑n⁆ = m
⊢ ⁅↑⟨x, hx✝⟩, ↑n⁆ ∈ ↑⊥

Proof state:
case intro.mk.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
m : M
x : L
hx : x ∈ ⊥
n : ↥N
hn : ⁅↑⟨x, hx⟩, ↑n⁆ = m
⊢ m ∈ ↑⊥

Tactic:
rw [← hn]

Result:
case intro.mk.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
m : M
x : L
hx : x ∈ ⊥
n : ↥N
hn : ⁅↑⟨x, hx⟩, ↑n⁆ = m
⊢ ⁅↑⟨x, hx⟩, ↑n⁆ ∈ ↑⊥

Proof state:
case intro.mk.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
m : M
x : L
hx : x ∈ ⊥
n : ↥N
hn : ⁅↑⟨x, hx⟩, ↑n⁆ = m
⊢ ⁅↑⟨x, hx⟩, ↑n⁆ ∈ ↑⊥

Tactic:
change x ∈ (⊥ : LieIdeal R L) at hx

Result:
case intro.mk.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
m : M
x : L
n : ↥N
hx : x ∈ ⊥
hn : ⁅↑⟨x, hx⟩, ↑n⁆ = m
⊢ ⁅↑⟨x, hx⟩, ↑n⁆ ∈ ↑⊥

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
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑⊥

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

Result:
case intro.mk.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
m : M
x : L
hx : x ∈ ⊥
n : ↥N
hn : ⁅↑⟨x, hx⟩, ↑n⁆ = m
⊢ m ∈ ↑⊥