-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma disjoint_ker_weight_corootSpace (α : Weight K H L) :
    Disjoint α.ker (corootSpace α)

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✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
x : ↥H
x✝ : x ∈ Weight.ker ⊓ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
hx : x ∈ ↑(LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
hαx : α x = 0
⊢ x = 0

Tactic:
exact eq_zero_of_apply_eq_zero_of_mem_corootSpace x α hαx hx

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✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
x : ↥H
x✝ : x ∈ Weight.ker ⊓ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
hαx : x ∈ ↑Weight.ker
hx : x ∈ ↑(LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
⊢ x = 0

Tactic:
replace hαx : α x = 0 := by simpa using hαx

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✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
x : ↥H
x✝ : x ∈ Weight.ker ⊓ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
hx : x ∈ ↑(LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
hαx : α x = 0
⊢ x = 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✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
⊢ Weight.ker ⊓ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule = ⊥

Tactic:
refine (Submodule.eq_bot_iff _).mpr fun x ⟨hαx, hx⟩ ↦ ?_

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✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
x : ↥H
x✝ : x ∈ Weight.ker ⊓ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
hαx : x ∈ ↑Weight.ker
hx : x ∈ ↑(LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
⊢ x = 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✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
x : ↥H
x✝ : x ∈ Weight.ker ⊓ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
hαx : x ∈ ↑Weight.ker
hx : x ∈ ↑(LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
⊢ α x = 0

Tactic:
simpa using hαx

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✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
⊢ Disjoint Weight.ker (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule

Tactic:
rw [disjoint_iff]

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✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
⊢ Weight.ker ⊓ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule = ⊥