awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : IsNoetherian R L
inst_5 : IsArtinian R L
H : LieSubalgebra R L
inst_6 : H.IsCartanSubalgebra
⊢ LinearMap.BilinForm.Nondegenerate (M := ↥H) (LieModule.traceForm R (↥H) L)

Tactic:
simp [LinearMap.separatingLeft_iff_ker_eq_bot,
    (LieModule.traceForm_isSymm R H L).isRefl.nondegenerate_iff_separatingLeft]

Premises used: LieModule.traceForm_isSymm, Membership.mem, Subtype, LinearMap.IsSymm.isRefl, LinearMap.separatingLeft_iff_ker_eq_bot, LinearMap.IsRefl.nondegenerate_iff_separatingLeft
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : IsKilling R L
inst_6 : Module.Free R L
inst_7 : Module.Finite R L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsArtinian R L
H : LieSubalgebra R L
inst_11 : H.IsCartanSubalgebra
⊢ IsLieAbelian.{u_3} ↥H

Tactic:
LieModule.isLieAbelian_of_ker_traceForm_eq_bot R H L <|
    ker_restrict_eq_bot_of_isCartanSubalgebra R L H

Premises used: Membership.mem, Subtype, LieModule.isLieAbelian_of_ker_traceForm_eq_bot, LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : 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) ↦ α + (β + γ)
γ : ↥H → K
⊢ σ γ ≠ γ

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

Premises used: Iff.mpr, add_assoc, add_ne_right
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : 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) ↦ α + (β + γ)
⊢ ∀ (γ : ↥H → K), σ γ ≠ γ

Tactic:
have hσ : ∀ γ, σ γ ≠ γ := fun γ ↦ by simpa only [σ, ← add_assoc] using add_ne_right.mpr hαβ
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : 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) ↦ α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L : (a : L) → End K L) x ∘ₗ (ad K L : (a : L) → End K L) y
⊢ ∀ (γ : ↥H → K), MapsTo (⇑f : (a : L) → L) (↑(rootSpace H γ) : Set L) (↑(rootSpace H (σ γ)) : Set L)

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
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : 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) ↦ α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L : (a : L) → End K L) x ∘ₗ (ad K L : (a : L) → End K L) y
hf : ∀ (γ : ↥H → K), MapsTo (⇑f : (a : L) → L) (↑(rootSpace H γ) : Set L) (↑(rootSpace H (σ γ)) : Set L)
⊢ DirectSum.IsInternal (S := Submodule K L) fun (i : ↥H → K) ↦ (↑(genWeightSpace L i) : Submodule K L)

Tactic:
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
    (LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpace K H L)
    (LieSubmodule.iSup_toSubmodule_eq_top.mpr <| iSup_genWeightSpace_eq_top K H L)
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : 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) ↦ α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L : (a : L) → End K L) x ∘ₗ (ad K L : (a : L) → End K L) y
hf : ∀ (γ : ↥H → K), MapsTo (⇑f : (a : L) → L) (↑(rootSpace H γ) : Set L) (↑(rootSpace H (σ γ)) : Set L)
hds : DirectSum.IsInternal (S := Submodule K L) fun (i : ↥H → K) ↦ (↑(genWeightSpace L i) : Submodule K L)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)

Tactic:
LinearMap.trace_eq_zero_of_mapsTo_ne hds σ hσ hf

Premises used: LinearMap.trace_eq_zero_of_mapsTo_ne
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : 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) ↦ α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L : (a : L) → End K L) x ∘ₗ (ad K L : (a : L) → End K L) y
hf : ∀ (γ : ↥H → K), MapsTo (⇑f : (a : L) → L) (↑(rootSpace H γ) : Set L) (↑(rootSpace H (σ γ)) : Set L)
hds : DirectSum.IsInternal (S := Submodule K L) fun (i : ↥H → K) ↦ (↑(genWeightSpace L i) : Submodule K L)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)

Tactic:
exact LinearMap.trace_eq_zero_of_mapsTo_ne hds σ hσ hf

Premises used: LinearMap.trace_eq_zero_of_mapsTo_ne
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : 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) ↦ α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
f : End K L := (ad K L : (a : L) → End K L) x ∘ₗ (ad K L : (a : L) → End K L) y
hf : ∀ (γ : ↥H → K), MapsTo (⇑f : (a : L) → L) (↑(rootSpace H γ) : Set L) (↑(rootSpace H (σ γ)) : Set L)
have have₁ have₂ :
  ∀ (hds : DirectSum.IsInternal (S := Submodule K L) fun (i : ↥H → K) ↦ (↑(genWeightSpace L i) : Submodule K L)),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)

Tactic:
classical
  have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
    (LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpace K H L)
    (LieSubmodule.iSup_toSubmodule_eq_top.mpr <| iSup_genWeightSpace_eq_top K H L)
  exact LinearMap.trace_eq_zero_of_mapsTo_ne hds σ hσ hf
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
h :
  ∀ (y : L),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
      ((0 : (a : L) → K) y : K)
⊢ Eq (α := L →ₗ[K] K) ((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) (0 : L →ₗ[K] K)

Tactic:
ext y
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y : L
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (β : ↥H → K), rootSpace H β) y

Tactic:
simp [iSup_genWeightSpace_eq_top K H L]

Premises used: Membership.mem, Subtype, LieModule.iSup_genWeightSpace_eq_top
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y : L
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (β : ↥H → K), rootSpace H β) y

Tactic:
have hy : y ∈ ⨆ β, rootSpace H β := by simp [iSup_genWeightSpace_eq_top K H L]
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y_1 : L
β : ↥H → K
y : L
hy : y ∈ rootSpace H β
pos :
  ∀ (hαβ : α + β = 0),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
      ((0 : (a : L) → K) y : K)
neg :
  ∀ (hαβ : ¬α + β = 0),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
      ((0 : (a : L) → K) y : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)

Tactic:
by_cases hαβ : α + β = 0
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y_1 : L
β : ↥H → K
y : L
hy : y ∈ rootSpace H β
hαβ : α + β = 0
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)

Tactic:
hx' _ (add_eq_zero_iff_neg_eq.mp hαβ ▸ hy)

Premises used: Eq.rec, add_eq_zero_iff_neg_eq, Iff.mp, Eq.symm
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y_1 : L
β : ↥H → K
y : L
hy : y ∈ rootSpace H β
hαβ : α + β = 0
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)

Tactic:
exact hx' _ (add_eq_zero_iff_neg_eq.mp hαβ ▸ hy)
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y_1 : L
β : ↥H → K
y : L
hy : y ∈ rootSpace H β
hαβ : ¬α + β = 0
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)

Tactic:
killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero K L H hx hy hαβ

Premises used: LieAlgebra.killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y_1 : L
β : ↥H → K
y : L
hy : y ∈ rootSpace H β
hαβ : ¬α + β = 0
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)

Tactic:
exact killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero K L H hx hy hαβ

Premises used: LieAlgebra.killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y : L
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) 0 : K)
    ((0 : (a : L) → K) 0 : K)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y x_1 y_1 : L
hx_1 : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) x_1
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) y_1
h :
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) x_1 : K)
    ((0 : (a : L) → K) x_1 : K)
h_1 :
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y_1 : K)
    ((0 : (a : L) → K) y_1 : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) (x_1 + y_1) : K)
    ((0 : (a : L) → K) (x_1 + y_1) : K)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' :
  ∀ y ∈ rootSpace H (-α),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
y : L
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (β : ↥H → K), rootSpace H β) y
h :
  ∀ (β : ↥H → K) (y : L) (hy : y ∈ rootSpace H β),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
      ((0 : (a : L) → K) y : K)
h₁ :
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) 0 : K)
    ((0 : (a : L) → K) 0 : K)
h₂ :
  ∀ (x_1 y : L),
    Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) x_1 →
      Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : ↥H → K), rootSpace H i) y →
        Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) x_1 : K)
            ((0 : (a : L) → K) x_1 : K) →
          Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
              ((0 : (a : L) → K) y : K) →
            Eq.{u_2 + 1} (α := K)
              ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) (x_1 + y) : K)
              ((0 : (a : L) → K) (x_1 + y) : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((0 : (a : L) → K) y : K)

Tactic:
induction hy using LieSubmodule.iSup_induction' with
  | mem β y hy =>
    by_cases hαβ : α + β = 0
    · exact hx' _ (add_eq_zero_iff_neg_eq.mp hαβ ▸ hy)
    · exact killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero K L H hx hy hαβ
  | zero => simp
  | add => simp_all
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
pos : ∀ (hα : α.IsZero), Ne (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
neg : ∀ (hα : ¬α.IsZero), Ne (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
⊢ Ne (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥

Tactic:
by_cases hα : α.IsZero

Premises used: LieModule.Weight.IsZero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : α.IsZero
⊢ Ne (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) ⊥

Tactic:
α.genWeightSpace_ne_bot

Premises used: LieModule.Weight.genWeightSpace_ne_bot
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : α.IsZero
h : Eq (α := ↥H → K) (-(⇑α : (a : ↥H) → K)) (⇑α : (a : ↥H) → K)
⊢ Ne (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥

Tactic:
convert! α.genWeightSpace_ne_bot

Premises used: LieModule.Weight.genWeightSpace_ne_bot
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : α.IsZero
h : Eq (α := ↥H → K) (-0) 0
h₁ h₂ : Eq (α := ↥H → K) 0 0
⊢ Eq (α := ↥H → K) (-(⇑α : (a : ↥H) → K)) (⇑α : (a : ↥H) → K)

Tactic:
rw [hα, neg_zero]

Premises used: neg_zero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
neg :
  ∀ (x : L) (hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x) (x_ne0 : x ≠ 0),
    False
⊢ False

Tactic:
obtain ⟨x, hx, x_ne0⟩ := α.exists_ne_zero

Premises used: LieModule.Weight.exists_ne_zero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
y : L
hy : y ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) ⊥ y

Tactic:
rw [rootSpace, e] at hy

Premises used: LieAlgebra.rootSpace
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
y : L
hy : Membership.mem (γ := LieSubmodule K (↥H) L) ⊥ y
rw : Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) 0 : K) (0 : K)
rw₁ rw₂ : Eq.{u_2 + 1} (α := K) 0 0
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)

Tactic:
rw [hy, map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
⊢ Membership.mem (γ := Submodule K L) (LinearMap.ker (killingForm K L)) x

Tactic:
have := mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg K L H hx
        (fun y hy ↦ by rw [rootSpace, e] at hy; rw [hy, map_zero])
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
this : Membership.mem (γ := Submodule K L) (LinearMap.ker (killingForm K L)) x
⊢ Membership.mem (γ := Submodule K L) ⊥ x

Tactic:
rw [ker_killingForm_eq_bot] at this

Premises used: LieAlgebra.IsKilling.ker_killingForm_eq_bot
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
this : Membership.mem (γ := Submodule K L) ⊥ x
⊢ False

Tactic:
x_ne0 this