-- 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.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 : ℕ
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}
t : R
z : L
x✝ : z ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
hz : ((traceForm R L M) z) y = 0
⊢ ((traceForm R L M) (t • z)) y = 0

Tactic:
simp [hz]

Result:
no goals

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 : y ∈ LieSubmodule.ucs (k + 1) ⊥
⊢ ((traceForm R L M) x) y = 0

Tactic:
rw [LieSubmodule.ucs_succ, LieSubmodule.mem_normalizer] at hy

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
hx : x ∈ ⊤.lcs L (k + 1)
hy : ∀ (x : L), ⁅x, y⁆ ∈ LieSubmodule.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
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

Tactic:
refine Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) hx

Result:
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

case succ.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 : ℕ
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) 0) y = 0

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

case succ.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 : ℕ
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}
t : R
z : L
x✝ : z ∈ Submodule.span R {x | ∃ x_1, ∃ n ∈ ⊤.lcs L k, ⁅x_1, n⁆ = x}
hz : ((traceForm R L M) z) y = 0
⊢ ((traceForm R L M) (t • z)) y = 0

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

Tactic:
rw [← lie_skew, map_neg, LinearMap.neg_apply, neg_eq_zero, traceForm_apply_lie_apply]

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) w) ⁅z, 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
x y : L
hx : x ∈ ⊤.lcs L 0
hy : y ∈ LieSubmodule.ucs 0 ⊥
⊢ y = 0

Tactic:
simpa using hy

Result:
no goals

Proof state:
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) w) ⁅z, y⁆ = 0

Tactic:
exact ih hw (hy _)

Result:
no goals

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 = 0
⊢ ((traceForm R L M) x) y = 0

Tactic:
simp [hy]

Result:
no goals

Proof state:
case succ.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 : ℕ
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) 0) y = 0

Tactic:
simp

Result:
no goals