-- Mathlib/Algebra/Lie/TraceForm.lean
lemma trace_toEnd_eq_zero_of_mem_lcs
    {k : ℕ} {x : L} (hk : 1 ≤ k) (hx : x ∈ lowerCentralSeries R L L k) :
    trace R _ (toEnd R L M x) = 0

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ lowerCentralSeries R L L 1
⊢ x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}

Tactic:
rw [lowerCentralSeries_succ, ← LieSubmodule.mem_toSubmodule,
  LieSubmodule.lieIdeal_oper_eq_linear_span'] at hx

Result:
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L L 0, ⁅x_1, n⁆ = x}
⊢ x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}

Proof state:
case refine_1
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
⊢ ∀ (x : L) (h : x ∈ {m | ∃ u v, ⁅u, v⁆ = m}), (fun x x_1 => (trace R M) (φ x) = 0) x ⋯

Tactic:
intro y ⟨u, v, huv⟩

Result:
case refine_1
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
y u v : L
huv : ⁅u, v⁆ = y
⊢ (trace R M) (φ y) = 0

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L L 0, ⁅x_1, n⁆ = x}
⊢ x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}

Tactic:
simpa using hx

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
⊢ (trace R M) (φ x) = 0

Tactic:
refine Submodule.span_induction (p := fun x _ ↦ trace R _ (toEnd R L M x) = 0)
  ?_ ?_ (fun u v _ _ hu hv ↦ ?_) (fun t u _ hu ↦ ?_) hx

Result:
case refine_1
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
⊢ ∀ (x : L) (h : x ∈ {m | ∃ u v, ⁅u, v⁆ = m}), (fun x x_1 => (trace R M) (φ x) = 0) x ⋯

case refine_2
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
⊢ (fun x x_1 => (trace R M) (φ x) = 0) 0 ⋯

case refine_3
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
u v : L
x✝¹ : u ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
x✝ : v ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
hu : (fun x x_1 => (trace R M) (φ x) = 0) u x✝¹
hv : (fun x x_1 => (trace R M) (φ x) = 0) v x✝
⊢ (fun x x_1 => (trace R M) (φ x) = 0) (u + v) ⋯

case refine_4
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
t : R
u : L
x✝ : u ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
hu : (fun x x_1 => (trace R M) (φ x) = 0) u x✝
⊢ (fun x x_1 => (trace R M) (φ x) = 0) (t • u) ⋯

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ lowerCentralSeries R L L 1
⊢ (trace R M) (φ x) = 0

Tactic:
replace hx : x ∈ Submodule.span R {m | ∃ u v : L, ⁅u, v⁆ = m} := by
  rw [lowerCentralSeries_succ, ← LieSubmodule.mem_toSubmodule,
    LieSubmodule.lieIdeal_oper_eq_linear_span'] at hx
  simpa using hx

Result:
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
⊢ (trace R M) (φ x) = 0

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ lowerCentralSeries R L L k
⊢ (trace R M) (φ x) = 0

Tactic:
replace hx : x ∈ lowerCentralSeries R L L 1 := antitone_lowerCentralSeries _ _ _ hk hx

Result:
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ lowerCentralSeries R L L 1
⊢ (trace R M) (φ x) = 0

Proof state:
case refine_1
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
y u v : L
huv : ⁅u, v⁆ = y
⊢ (trace R M) (φ y) = 0

Tactic:
simp [← huv]

Result:
no goals

Proof state:
case refine_4
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
t : R
u : L
x✝ : u ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
hu : (fun x x_1 => (trace R M) (φ x) = 0) u x✝
⊢ (fun x x_1 => (trace R M) (φ x) = 0) (t • u) ⋯

Tactic:
simp [hu]

Result:
no goals

Proof state:
case refine_2
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
⊢ (fun x x_1 => (trace R M) (φ x) = 0) 0 ⋯

Tactic:
simp

Result:
no goals

Proof state:
case refine_3
R : Type u_1
L : Type u_3
M : Type u_4
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 : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
u v : L
x✝¹ : u ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
x✝ : v ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
hu : (fun x x_1 => (trace R M) (φ x) = 0) u x✝¹
hv : (fun x x_1 => (trace R M) (φ x) = 0) v x✝
⊢ (fun x x_1 => (trace R M) (φ x) = 0) (u + v) ⋯

Tactic:
simp [hu, hv]

Result:
no goals