case mp
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 : ℕ
N : LieSubmodule R L M
h : IsTrivial L M
⊢ lowerCentralSeries R L M 1 = ⊥

case mpr
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 : ℕ
N : LieSubmodule R L M
h : lowerCentralSeries R L M 1 = ⊥
⊢ IsTrivial L M
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 : ℕ
N : LieSubmodule R L M
⊢ IsTrivial L M ↔ lowerCentralSeries R L M 1 = ⊥
constructor <;> intro h
case mp
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 : ℕ
N : LieSubmodule R L M
h : IsTrivial L M
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑⊥
case mp
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 : ℕ
N : LieSubmodule R L M
h : IsTrivial L M
⊢ lowerCentralSeries R L M 1 = ⊥
erw [eq_bot_iff, LieSubmodule.lieSpan_le]
case mp.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
k : ℕ
N : LieSubmodule R L M
h : IsTrivial L M
m : M
x : { x // x ∈ ⊤ }
n : { x // x ∈ ⊤ }
hn : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑⊥
case mp
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 : ℕ
N : LieSubmodule R L M
h : IsTrivial L M
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑⊥
rintro m ⟨x, n, hn⟩
case mp.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
k : ℕ
N : LieSubmodule R L M
h : IsTrivial L M
m : M
x : { x // x ∈ ⊤ }
n : { x // x ∈ ⊤ }
hn : ⁅↑x, ↑n⁆ = m
⊢ 0 ∈ ↑⊥
case mp.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
k : ℕ
N : LieSubmodule R L M
h : IsTrivial L M
m : M
x : { x // x ∈ ⊤ }
n : { x // x ∈ ⊤ }
hn : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑⊥
rw [← hn, h.trivial]
no goals
case mp.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
k : ℕ
N : LieSubmodule R L M
h : IsTrivial L M
m : M
x : { x // x ∈ ⊤ }
n : { x // x ∈ ⊤ }
hn : ⁅↑x, ↑n⁆ = m
⊢ 0 ∈ ↑⊥
simp
case mpr
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 : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
⊢ IsTrivial L M
case mpr
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 : ℕ
N : LieSubmodule R L M
h : lowerCentralSeries R L M 1 = ⊥
⊢ IsTrivial L M
rw [LieSubmodule.eq_bot_iff] at h
case mpr.trivial
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 : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
⊢ ∀ (x : L) (m : M), ⁅x, m⁆ = 0
case mpr
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 : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
⊢ IsTrivial L M
apply IsTrivial.mk
case mpr.trivial
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 : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
x : L
m : M
⊢ ⁅x, m⁆ = 0
case mpr.trivial
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 : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
⊢ ∀ (x : L) (m : M), ⁅x, m⁆ = 0
intro x m
case mpr.trivial.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 : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
x : L
m : M
⊢ ⁅x, m⁆ ∈ lowerCentralSeries R L M 1
case mpr.trivial
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 : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
x : L
m : M
⊢ ⁅x, m⁆ = 0
apply h
case mpr.trivial.a.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 : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
x : L
m : M
⊢ ⁅x, m⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case mpr.trivial.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 : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
x : L
m : M
⊢ ⁅x, m⁆ ∈ lowerCentralSeries R L M 1
apply LieSubmodule.subset_lieSpan
case mpr.trivial.a.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 : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
x : L
m : M
⊢ ∃ a a_1, ⁅a, a_1⁆ = ⁅x, m⁆
case mpr.trivial.a.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 : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
x : L
m : M
⊢ ⁅x, m⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
simp only [LieSubmodule.top_coe, Subtype.exists, LieSubmodule.mem_top, exists_prop, true_and,
  Set.mem_setOf]
no goals
case mpr.trivial.a.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 : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
x : L
m : M
⊢ ∃ a a_1, ⁅a, a_1⁆ = ⁅x, m⁆
exact ⟨x, m, rfl⟩