awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
⊢ α = β
have hβ : β.IsNonZero
Tactic: have hβ : β.IsNonZero := by
      contrapose hα
      simp only [← coroot_eq_zero_iff] at hα ⊢
      rwa [hyp]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
⊢ Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
have rw : Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
  (Weight.ker (M := L) (χ := β))
Tactic: rw [← orthogonal_span_coroot_eq_ker α, hyp, orthogonal_span_coroot_eq_ker]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
rw :
  Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := β))
⊢ Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
have rw₁ : Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot β))
  (Weight.ker (M := L) (χ := β))
Tactic: rw [← orthogonal_span_coroot_eq_ker α, hyp, orthogonal_span_coroot_eq_ker]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
rw :
  Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := β))
rw₁ :
  Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot β))
    (Weight.ker (M := L) (χ := β))
⊢ Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
have rw₂ : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := β)) (Weight.ker (M := L) (χ := β))
Tactic: rw [← orthogonal_span_coroot_eq_ker α, hyp, orthogonal_span_coroot_eq_ker]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
⊢ α = β
have this : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
Tactic: have : α.ker = β.ker := by
      rw [← orthogonal_span_coroot_eq_ker α, hyp, orthogonal_span_coroot_eq_ker]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
this_1 : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
this : Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
⊢ α = β
have h : ∀ (x : ↥H), Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) ((β : (a : ↥H) → K) x : K)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
this : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
⊢ α = β
have suffices : Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
Tactic: suffices (α : H →ₗ[K] K) = β by ext x; simpa using LinearMap.congr_fun this x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
this : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
⊢ Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
have h' : Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) (coroot α) : K)
  ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
Tactic: apply Module.Dual.eq_of_ker_eq_of_apply_eq (coroot α) this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
this : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
h' :
  Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) (coroot α) : K)
    ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
⊢ Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
have hx : Ne.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) (coroot α) : K) (0 : K)
Tactic: apply Module.Dual.eq_of_ker_eq_of_apply_eq (coroot α) this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
this : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
⊢ Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) (coroot α) : K)
    ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
have h' : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (coroot α) : K) ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
Tactic: rw [Weight.toLinear_apply, root_apply_coroot hα, hyp, Weight.toLinear_apply,
        root_apply_coroot hβ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
this : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
h' :
  Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (coroot α) : K) ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
⊢ Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) (coroot α) : K)
    ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
have h'₁ : Eq.{u_2 + 1} (α := K) (2 : K) ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
Tactic: rw [Weight.toLinear_apply, root_apply_coroot hα, hyp, Weight.toLinear_apply,
        root_apply_coroot hβ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
this : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
h' :
  Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (coroot α) : K) ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
h'₁ : Eq.{u_2 + 1} (α := K) (2 : K) ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
⊢ Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) (coroot α) : K)
    ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
have h'₂ : Eq.{u_2 + 1} (α := K) (2 : K) ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot β) : K)
Tactic: rw [Weight.toLinear_apply, root_apply_coroot hα, hyp, Weight.toLinear_apply,
        root_apply_coroot hβ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
this : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
h' :
  Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (coroot α) : K) ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
h'₁ : Eq.{u_2 + 1} (α := K) (2 : K) ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
h'₂ : Eq.{u_2 + 1} (α := K) (2 : K) ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot β) : K)
⊢ Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) (coroot α) : K)
    ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
have h'₃ : Eq.{u_2 + 1} (α := K) (2 : K) ((β : (a : ↥H) → K) (coroot β) : K)
Tactic: rw [Weight.toLinear_apply, root_apply_coroot hα, hyp, Weight.toLinear_apply,
        root_apply_coroot hβ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
this : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (Weight.ker (M := L) (χ := β))
h' :
  Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (coroot α) : K) ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
h'₁ : Eq.{u_2 + 1} (α := K) (2 : K) ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
h'₂ : Eq.{u_2 + 1} (α := K) (2 : K) ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot β) : K)
h'₃ : Eq.{u_2 + 1} (α := K) (2 : K) ((β : (a : ↥H) → K) (coroot β) : K)
⊢ Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) (coroot α) : K)
    ((Weight.toLinear K (↥H) L β : (a : ↥H) → K) (coroot α) : K)
have h'₄ : Eq.{u_2 + 1} (α := K) 2 2
Tactic: rw [Weight.toLinear_apply, root_apply_coroot hα, hyp, Weight.toLinear_apply,
        root_apply_coroot hβ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
⊢ α = β
have if : ∀ (hα : α.IsZero), α = β
Tactic: if hα : α.IsZero then
    have hβ : β.IsZero := by
      rw [← coroot_eq_zero_iff] at hα ⊢
      rwa [← hyp]
    ext
    simp [hα.eq, hβ.eq]
  else
    have hβ : β.IsNonZero := by
      contrapose hα
      simp only [← coroot_eq_zero_iff] at hα ⊢
      rwa [hyp]
    have : α.ker = β.ker := by
      rw [← orthogonal_span_coroot_eq_ker α, hyp, orthogonal_span_coroot_eq_ker]
    suffices (α : H →ₗ[K] K) = β by ext x; simpa using LinearMap.congr_fun this x
    apply Module.Dual.eq_of_ker_eq_of_apply_eq (coroot α) this
    · rw [Weight.toLinear_apply, root_apply_coroot hα, hyp, Weight.toLinear_apply,
        root_apply_coroot hβ]
    · simp [root_apply_coroot hα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
hyp : coroot α = coroot β
if : ∀ (hα : α.IsZero), α = β
⊢ α = β
have if₁ : ∀ (hα : ¬α.IsZero), α = β
Tactic: if hα : α.IsZero then
    have hβ : β.IsZero := by
      rw [← coroot_eq_zero_iff] at hα ⊢
      rwa [← hyp]
    ext
    simp [hα.eq, hβ.eq]
  else
    have hβ : β.IsNonZero := by
      contrapose hα
      simp only [← coroot_eq_zero_iff] at hα ⊢
      rwa [hyp]
    have : α.ker = β.ker := by
      rw [← orthogonal_span_coroot_eq_ker α, hyp, orthogonal_span_coroot_eq_ker]
    suffices (α : H →ₗ[K] K) = β by ext x; simpa using LinearMap.congr_fun this x
    apply Module.Dual.eq_of_ker_eq_of_apply_eq (coroot α) this
    · rw [Weight.toLinear_apply, root_apply_coroot hα, hyp, Weight.toLinear_apply,
        root_apply_coroot hβ]
    · simp [root_apply_coroot hα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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
⊢ ∃ (h : L) (e : L) (f : L),
    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
have obtain : ∀ (e : L) (heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)) (he₀ : e ≠ 0),
  ∃ (h : L) (e : L) (f : L),
    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
Tactic: obtain ⟨e, heα : e ∈ rootSpace H α, he₀ : e ≠ 0⟩ := α.exists_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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 : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
he₀ : e ≠ 0
⊢ ∃ f ∈ rootSpace H (-(⇑α : (a : ↥H) → 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)
have contrapose! : ∀
  (he₀ :
    ∀ (f : L) (_ : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))),
      Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)),
  e = 0
Tactic: contrapose! he₀
Cleared hypotheses: he₀
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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 : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
he₀ : e ≠ 0
⊢ ∃ (h : L) (e : L) (f : L),
    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
have obtain : ∀ (f' : L) (hfα : f' ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
  (hf : Ne.{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) (e : L) (f : L),
    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
Tactic: obtain ⟨f', hfα, hf⟩ : ∃ f ∈ rootSpace H (-α), killingForm K L e f ≠ 0 := by
    contrapose! he₀
    simpa using mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg K L H heα he₀
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
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 : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hf : Ne.{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) (e : L) (f : L),
    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
have hef : ⁅e, f'⁆ =
  HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := L)
    ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K)
    (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)
Tactic: have hef := lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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 : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hf : Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K) (0 : K)
hef :
  ⁅e, f'⁆ =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := L)
      ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K)
      (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)
h : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) ⁅e, f'⁆ ⋯
⊢ h =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := ↥H)
      ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K)
      (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
have simp : HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := L)
    ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K)
    (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) =
  (↑(HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := ↥H)
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K)
        (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)) :
    L)
Tactic: simp only [h, Subtype.ext_iff, hef]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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 : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hf : Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K) (0 : K)
hef :
  ⁅e, f'⁆ =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := L)
      ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K)
      (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)
h : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) ⁅e, f'⁆ ⋯
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := L)
      ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K)
      (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) =
    (↑(HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := ↥H)
          ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K)
          (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)) :
      L)
have rw : HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := L)
    ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K)
    (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := L)
    ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K)
    (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)
Tactic: rw [Submodule.coe_smul_of_tower]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
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 : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hf : Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K) (0 : K)
hef :
  ⁅e, f'⁆ =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := L)
      ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K)
      (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)
h : ↥H := Subtype.mk (p := fun (x : L) ↦ x ∈ H) ⁅e, f'⁆ ⋯
⊢ Ne.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (0 : K)
have this : h =
  HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := ↥H)
    ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K)
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
Tactic: have : h = killingForm K L e f' • (cartanEquivDual H).symm α := by
      simp only [h, Subtype.ext_iff, hef]
      rw [Submodule.coe_smul_of_tower]