awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
h : ↥H
ht : IsSl2Triple (↑h : L) e f
key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
hef :
  ⁅e, f⁆ =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      (↑α' : L)
hα' : α' = ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
h_eq :
  h =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      α'
h₁ :
  HMul.hMul (β := K) (HSMul.hSMul (α := ℕ) (β := K) 2 (((α : (a : ↥H) → K) α')⁻¹ : K))
        (((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f)⁻¹ : K) •
      h =
    coroot α
⊢ ∃ (s : K), s • h = coroot α

Tactic:
use (2 • (α α')⁻¹) * (killingForm K L e f)⁻¹

Premises used: killingForm, Inv.inv, HSMul.hSMul, OfNat.ofNat, DFunLike.coe
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
h : ↥H
ht : IsSl2Triple (↑h : L) e f
key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
hef :
  ⁅e, f⁆ =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      (↑α' : L)
hα' : α' = ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
h_eq :
  h =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      α'
⊢ (↑h : L) ≠ 0

Tactic:
have := ht.h_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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
h : ↥H
ht : IsSl2Triple (↑h : L) e f
key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
hef :
  ⁅e, f⁆ =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      (↑α' : L)
hα' : α' = ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
h_eq :
  h =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      α'
this : (↑h : L) ≠ 0
contrapose :
  ∀
    (this :
      Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)),
    (↑h : L) = 0
⊢ Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)

Tactic:
contrapose this
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
h : ↥H
ht : IsSl2Triple (↑h : L) e f
key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
hef :
  ⁅e, f⁆ =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      (↑α' : L)
hα' : α' = ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
h_eq :
  h =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      α'
this : Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)
⊢ (↑h : L) = 0

Tactic:
simpa [this] using h_eq
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
h : ↥H
ht : IsSl2Triple (↑h : L) e f
key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
hef :
  ⁅e, f⁆ =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      (↑α' : L)
hα' : α' = ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
h_eq :
  h =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      α'
⊢ Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)

Tactic:
have hef₀ : killingForm K L e f ≠ 0 := by
    have := ht.h_ne_zero
    contrapose this
    simpa [this] using h_eq
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
this : ¬1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
convert_to : finrank.{u_2, u_3} K ↥(↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L) ≠ 0
⊢ finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K)) ≠ 0

Tactic:
convert_to finrank K (rootSpace H α).toSubmodule ≠ 0

Premises used: LieSubmodule.toSubmodule, Membership.mem, Subtype, LieAlgebra.rootSpace, DFunLike.coe, Module.finrank
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
this : ¬1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
⊢ finrank.{u_2, u_3} K ↥(↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L) ≠ 0

Tactic:
simpa using α.genWeightSpace_ne_bot

Premises used: LieModule.Weight.genWeightSpace_ne_bot
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
this : ¬1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
⊢ finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K)) ≠ 0

Tactic:
have h₀ : finrank K (rootSpace H α) ≠ 0 := by
      convert_to finrank K (rootSpace H α).toSubmodule ≠ 0
      simpa using α.genWeightSpace_ne_bot
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
this : ¬1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h₀ : finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K)) ≠ 0
⊢ finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K)) = 1

Tactic:
lia
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
suffices : ¬1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
⊢ finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K)) = 1

Tactic:
suffices ¬ 1 < finrank K (rootSpace H α) by
    have h₀ : finrank K (rootSpace H α) ≠ 0 := by
      convert_to finrank K (rootSpace H α).toSubmodule ≠ 0
      simpa using α.genWeightSpace_ne_bot
    lia
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
obtain :
  ∀ (h e f : L) (ht : IsSl2Triple h e f) (heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K))
    (hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))), False
⊢ False

Tactic:
obtain ⟨h, e, f, ht, heα, hfα⟩ := exists_isSl2Triple_of_weight_isNonZero hα

Premises used: LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
rwa rwa₁ rwa₂ rwa₃ : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
⊢ finrank K K < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))

Tactic:
rwa [finrank_self]

Premises used: Module.finrank_self
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
⊢ F.ker ≠ ⊥

Tactic:
have hF : LinearMap.ker F ≠ ⊥ := F.ker_ne_bot_of_finrank_lt <| by rwa [finrank_self]
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
hF : F.ker ≠ ⊥
obtain :
  ∀ (y : L) (hyα : y ∈ rootSpace H (⇑α : (a : ↥H) → K))
    (hy : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ∈ F.ker)
    (hy₀ : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ≠ 0), False
⊢ False

Tactic:
obtain ⟨⟨y, hyα⟩, hy, hy₀⟩ := (Submodule.ne_bot_iff _).mp hF

Premises used: Submodule.ne_bot_iff, Iff.mp
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H (⇑α : (a : ↥H) → K)
hy : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ∈ F.ker
hy₀ : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ≠ 0
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) y : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)

Tactic:
simpa [F, traceForm_comm] using hy

Premises used: LieModule.traceForm_comm
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H (⇑α : (a : ↥H) → K)
hy : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ∈ F.ker
hy₀ : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ≠ 0
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) y : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)

Tactic:
have : killingForm K L y f = 0 := by simpa [F, traceForm_comm] using 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H (⇑α : (a : ↥H) → K)
hy : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ∈ F.ker
hy₀ : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ≠ 0
this : Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) y : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)
⊢ ⁅y, f⁆ = 0

Tactic:
simpa [this] using lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg hyα hfα

Premises used: LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H (⇑α : (a : ↥H) → K)
hy : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ∈ F.ker
hy₀ : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ≠ 0
⊢ ⁅y, f⁆ = 0

Tactic:
replace hy : ⁅y, f⁆ = 0 := by
    have : killingForm K L y f = 0 := by simpa [F, traceForm_comm] using hy
    simpa [this] using lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg hyα 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H (⇑α : (a : ↥H) → K)
hy₀ : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ≠ 0
hy : ⁅y, f⁆ = 0
⊢ y ≠ 0

Tactic:
simpa [LieSubmodule.mk_eq_zero] using hy₀

Premises used: LieSubmodule.mk_eq_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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H (⇑α : (a : ↥H) → K)
hy₀ : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ≠ 0
hy : ⁅y, f⁆ = 0
⊢ ⁅-h, y⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) (-2) y

Tactic:
simp only [neg_smul, neg_lie, ht.h_eq_coroot hα heα hfα,
        ← H.coe_bracket_of_module, lie_eq_smul_of_mem_rootSpace hyα (coroot α),
        root_apply_coroot hα]

Premises used: neg_smul, LieAlgebra.IsKilling.coroot, LieSubalgebra.coe_bracket_of_module, IsSl2Triple.h_eq_coroot, neg_lie, LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace, LieAlgebra.IsKilling.root_apply_coroot
-- 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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H (⇑α : (a : ↥H) → K)
hy₀ : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ≠ 0
hy : ⁅y, f⁆ = 0
rw : -⁅y, f⁆ = 0
rw₁ : Eq.{u_3 + 1} (α := L) (-0) 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := L) 0 0
⊢ ⁅f, y⁆ = 0

Tactic:
rw [← lie_skew, hy, neg_zero]

Premises used: lie_skew, neg_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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H (⇑α : (a : ↥H) → K)
hy₀ : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ≠ 0
hy : ⁅y, f⁆ = 0
⊢ IsSl2Triple.HasPrimitiveVectorWith.{u_2, u_3, u_3} (R := K) ⋯ y (-2)

Tactic:
have P : ht.symm.HasPrimitiveVectorWith y (-2 : K) :=
    { ne_zero := by simpa [LieSubmodule.mk_eq_zero] using hy₀
      lie_h := by simp only [neg_smul, neg_lie, ht.h_eq_coroot hα heα hfα,
        ← H.coe_bracket_of_module, lie_eq_smul_of_mem_rootSpace hyα (coroot α),
        root_apply_coroot hα]
      lie_e := by rw [← lie_skew, hy, neg_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 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H (⇑α : (a : ↥H) → K)
hy₀ : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ≠ 0
hy : ⁅y, f⁆ = 0
P : IsSl2Triple.HasPrimitiveVectorWith.{u_2, u_3, u_3} (R := K) ⋯ y (-2)
obtain : ∀ (n : ℕ) (hn : Eq.{u_2 + 1} (α := K) (-2) (↑n : K)), False
⊢ False

Tactic:
obtain ⟨n, hn⟩ := P.exists_nat

Premises used: IsSl2Triple.HasPrimitiveVectorWith.exists_nat