-- Mathlib/Algebra/Lie/TraceForm.lean
/-- The upper and lower central series of `L` are orthogonal wrt the trace form of any Lie module
`M`. -/
lemma traceForm_eq_zero_if_mem_lcs_of_mem_ucs {x y : L} (k : ℕ)
    (hx : x ∈ (⊤ : LieIdeal R L).lcs L k) (hy : y ∈ (⊥ : LieIdeal R L).ucs k) :
    traceForm R L M x y = 0

Proof state:
case succ
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 : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hx : x ∈ ⊤.lcs L (k + 1)
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.ucs k ⊥
⊢ ((traceForm R L M) x) y = 0

Tactic:
simp_rw [LieIdeal.lcs_succ, ← LieSubmodule.mem_toSubmodule,
  LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_top, true_and] at hx

Result:
case succ
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 : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.ucs k ⊥
hx : x ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
⊢ ((traceForm R L M) x) y = 0

Proof state:
case zero
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
x y : L
hx : x ∈ ⊤.lcs L 0
hy : y ∈ LieSubmodule.ucs 0 ⊥
⊢ ((traceForm R L M) x) y = 0

Tactic:
replace hy : y = 0 := by simpa using hy

Result:
case zero
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
x y : L
hx : x ∈ ⊤.lcs L 0
hy : y = 0
⊢ ((traceForm R L M) x) y = 0

Proof state:
case succ.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 : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.ucs k ⊥
hx : x ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
z w : L
x✝¹ : z ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
x✝ : w ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
hz : ((traceForm R L M) z) y = 0
hw : ((traceForm R L M) w) y = 0
⊢ ((traceForm R L M) (z + w)) y = 0

Tactic:
simp [hz, hw]

Result:
no goals

Proof state:
case succ.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 : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.ucs k ⊥
hx : x ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
⊢ ∀ x ∈ {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}, ((traceForm R L M) x) y = 0

Tactic:
rintro - ⟨z, w, hw, rfl⟩

Result:
case succ.refine_1.intro.intro.intro
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 : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.ucs k ⊥
hx : x ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
z w : L
hw : w ∈ ⊤.lcs L k
⊢ ((traceForm R L M) ⁅z, w⁆) y = 0