-- Mathlib/Algebra/Lie/Character.lean
theorem lieCharacter_apply_of_mem_derived (χ : LieCharacter R L) {x : L}
    (h : x ∈ derivedSeries R L 1) : χ x = 0

Proof state:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ ∀ (a : R), ∀ x ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, χ x = 0 → χ (a • x) = 0

Tactic:
intro t y _ hy

Result:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
t : R
y : L
hx✝ : y ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
hy : χ y = 0
⊢ χ (t • y) = 0

Proof state:
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

Tactic:
rw [derivedSeries_def, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero, ←
  LieSubmodule.mem_toSubmodule, LieSubmodule.lieIdeal_oper_eq_linear_span] at h

Result:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ χ x = 0

Proof state:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ χ x = 0

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ h

Result:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ ∀ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, χ 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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ χ 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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ ∀ (x y : L),
    x ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} →
      y ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → χ 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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ ∀ (a : R), ∀ x ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, χ x = 0 → χ (a • x) = 0

Proof state:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ ∀ x ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, χ x = 0

Tactic:
rintro y ⟨⟨z, hz⟩, ⟨⟨w, hw⟩, rfl⟩⟩

Result:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
z : L
hz : z ∈ ⊤
w : L
hw : w ∈ ⊤
⊢ χ ⁅↑⟨z, hz⟩, ↑⟨w, hw⟩⁆ = 0

Proof state:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ χ 0 = 0

Tactic:
exact χ.map_zero

Result:
no goals

Proof state:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ ∀ (x y : L),
    x ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} →
      y ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → χ x = 0 → χ y = 0 → χ (x + y) = 0

Tactic:
intro y z _ _ hy hz

Result:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y z : L
hx✝ : y ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
hy✝ : z ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
hy : χ y = 0
hz : χ z = 0
⊢ χ (y + z) = 0

Proof state:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
t : R
y : L
hx✝ : y ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
hy : χ y = 0
⊢ χ (t • y) = 0

Tactic:
rw [LieHom.map_smul, hy, smul_zero]

Result:
no goals

Proof state:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
z : L
hz : z ∈ ⊤
w : L
hw : w ∈ ⊤
⊢ χ ⁅↑⟨z, hz⟩, ↑⟨w, hw⟩⁆ = 0

Tactic:
apply lieCharacter_apply_lie

Result:
no goals

Proof state:
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 {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y z : L
hx✝ : y ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
hy✝ : z ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
hy : χ y = 0
hz : χ z = 0
⊢ χ (y + z) = 0

Tactic:
rw [LieHom.map_add, hy, hz, add_zero]

Result:
no goals