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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
this : ⁅I, N⁆ ≤ ⊥
⊢ ⁅I, N⁆ = ⊥

case this
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ ⁅I, N⁆ ≤ ⊥
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ ⁅I, N⁆ = ⊥
suffices : ⁅I, N⁆ ≤ ⊥
case this
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ ⁅I, N⁆ ≤ ⊥
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
this : ⁅I, N⁆ ≤ ⊥
⊢ ⁅I, N⁆ = ⊥

case this
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ ⁅I, N⁆ ≤ ⊥
exact le_bot_iff.mp this
case this
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑⊥
case this
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ ⁅I, N⁆ ≤ ⊥
rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]
case this.intro.intro
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : { x // x ∈ I }
n : { x // x ∈ N }
h : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑⊥
case this
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑⊥
rintro m ⟨x, n, h⟩
case this.intro.intro
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : { x // x ∈ I }
n : { x // x ∈ N }
h : 0 = m
⊢ m ∈ ↑⊥
case this.intro.intro
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : { x // x ∈ I }
n : { x // x ∈ N }
h : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑⊥
rw [trivial_lie_zero] at h
no goals
case this.intro.intro
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
N N' : LieSubmodule R L M
I J : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : { x // x ∈ I }
n : { x // x ∈ N }
h : 0 = m
⊢ m ∈ ↑⊥
simp [← h]