R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ↑χ x = 0
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ derivedSeries R L 1
⊢ ↑χ x = 0
rw [derivedSeries_def, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero, ←
  LieSubmodule.mem_coeSubmodule, LieSubmodule.lieIdeal_oper_eq_linear_span] at h
case refine'_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ∀ (x : L), x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → ↑χ x = 0

case refine'_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ↑χ 0 = 0

case refine'_3
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ∀ (x y : L), ↑χ x = 0 → ↑χ y = 0 → ↑χ (x + y) = 0

case refine'_4
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ∀ (a : R) (x : L), ↑χ x = 0 → ↑χ (a • x) = 0
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ↑χ x = 0
refine' Submodule.span_induction h _ _ _ _
case refine'_1.intro.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
z : L
hz : z ∈ ⊤
w : L
hw : w ∈ ⊤
⊢ ↑χ ⁅↑{ val := z, property := hz }, ↑{ val := w, property := hw }⁆ = 0
case refine'_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ∀ (x : L), x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → ↑χ x = 0
rintro y ⟨⟨z, hz⟩, ⟨⟨w, hw⟩, rfl⟩⟩
no goals
case refine'_1.intro.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
z : L
hz : z ∈ ⊤
w : L
hw : w ∈ ⊤
⊢ ↑χ ⁅↑{ val := z, property := hz }, ↑{ val := w, property := hw }⁆ = 0
apply lieCharacter_apply_lie
no goals
case refine'_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ↑χ 0 = 0
exact χ.map_zero
case refine'_3
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
y z : L
hy : ↑χ y = 0
hz : ↑χ z = 0
⊢ ↑χ (y + z) = 0
case refine'_3
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ∀ (x y : L), ↑χ x = 0 → ↑χ y = 0 → ↑χ (x + y) = 0
intro y z hy hz
no goals
case refine'_3
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
y z : L
hy : ↑χ y = 0
hz : ↑χ z = 0
⊢ ↑χ (y + z) = 0
rw [LieHom.map_add, hy, hz, add_zero]
case refine'_4
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
t : R
y : L
hy : ↑χ y = 0
⊢ ↑χ (t • y) = 0
case refine'_4
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ∀ (a : R) (x : L), ↑χ x = 0 → ↑χ (a • x) = 0
intro t y hy
no goals
case refine'_4
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
t : R
y : L
hy : ↑χ y = 0
⊢ ↑χ (t • y) = 0
rw [LieHom.map_smul, hy, smul_zero]