-- Mathlib/Algebra/Lie/Weights/Killing.lean
/-- For any `α` and `β`, the corresponding root spaces are orthogonal with respect to the Killing
form, provided `α + β ≠ 0`. -/
lemma killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero {α β : H → K} {x y : L}
    (hx : x ∈ rootSpace H α) (hy : y ∈ rootSpace H β) (hαβ : α + β ≠ 0) :
    killingForm K L x y = 0

Proof state:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L) x ∘ₗ (ad K L) y
hf : ∀ (γ : ↥H → K), MapsTo ⇑f ↑(rootSpace H γ) ↑(rootSpace H (σ γ))
⊢ ((killingForm K L) x) y = 0

Tactic:
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
  (LieSubmodule.iSupIndep_iff_toSubmodule.mp <| iSupIndep_genWeightSpace K H L)
  (LieSubmodule.iSup_eq_top_iff_toSubmodule.mp <| iSup_genWeightSpace_eq_top K H L)

Result:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L) x ∘ₗ (ad K L) y
hf : ∀ (γ : ↥H → K), MapsTo ⇑f ↑(rootSpace H γ) ↑(rootSpace H (σ γ))
hds : DirectSum.IsInternal fun i => ↑(genWeightSpace L i)
⊢ ((killingForm K L) x) y = 0

Proof state:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
⊢ ((killingForm K L) x) y = 0

Tactic:
let σ : (H → K) → (H → K) := fun γ ↦ α + (β + γ)

Result:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)
⊢ ((killingForm K L) x) y = 0

Proof state:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)
γ : ↥H → K
⊢ σ γ ≠ γ

Tactic:
simpa only [σ, ← add_assoc] using add_left_ne_self.mpr hαβ

Result:
no goals

Proof state:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L) x ∘ₗ (ad K L) y
hf : ∀ (γ : ↥H → K), MapsTo ⇑f ↑(rootSpace H γ) ↑(rootSpace H (σ γ))
⊢ ((killingForm K L) x) y = 0

Tactic:
classical
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
  (LieSubmodule.iSupIndep_iff_toSubmodule.mp <| iSupIndep_genWeightSpace K H L)
  (LieSubmodule.iSup_eq_top_iff_toSubmodule.mp <| iSup_genWeightSpace_eq_top K H L)
exact LinearMap.trace_eq_zero_of_mapsTo_ne hds σ hσ hf

Result:
no goals

Proof state:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L) x ∘ₗ (ad K L) y
hf : ∀ (γ : ↥H → K), MapsTo ⇑f ↑(rootSpace H γ) ↑(rootSpace H (σ γ))
hds : DirectSum.IsInternal fun i => ↑(genWeightSpace L i)
⊢ ((killingForm K L) x) y = 0

Tactic:
exact LinearMap.trace_eq_zero_of_mapsTo_ne hds σ hσ hf

Result:
no goals

Proof state:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)
⊢ ((killingForm K L) x) y = 0

Tactic:
have hσ : ∀ γ, σ γ ≠ γ := fun γ ↦ by simpa only [σ, ← add_assoc] using add_left_ne_self.mpr hαβ

Result:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
⊢ ((killingForm K L) x) y = 0

Proof state:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
⊢ ((killingForm K L) x) y = 0

Tactic:
let f : Module.End K L := (ad K L x) ∘ₗ (ad K L y)

Result:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L) x ∘ₗ (ad K L) y
⊢ ((killingForm K L) x) y = 0

Proof state:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L) x ∘ₗ (ad K L) y
⊢ ((killingForm K L) x) y = 0

Tactic:
have hf : ∀ γ, MapsTo f (rootSpace H γ) (rootSpace H (σ γ)) := fun γ ↦
  (mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L α (β + γ) hx).comp <|
    mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L β γ hy

Result:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L) x ∘ₗ (ad K L) y
hf : ∀ (γ : ↥H → K), MapsTo ⇑f ↑(rootSpace H γ) ↑(rootSpace H (σ γ))
⊢ ((killingForm K L) x) y = 0