awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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 =
    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)
      α'
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, ← ht.lie_e_f, 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 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 α)
⊢ 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 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 α)
⊢ ∃ (s : K), s • h = coroot α
have 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)
    α'
Tactic: have h_eq : h = killingForm K L e f • α' := by
    simp only [hα', Subtype.ext_iff, ← ht.lie_e_f, hef]
    rw [Submodule.coe_smul_of_tower]
-- 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 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)
      α'
⊢ ∃ (s : K), s • h = coroot α
have 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 α
Tactic: use (2 • (α α')⁻¹) * (killingForm K L e f)⁻¹
-- 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 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)
have this : (↑h : L) ≠ 0
Tactic: have := ht.h_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 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
⊢ 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 : ∀
  (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: contrapose this
Cleared hypotheses: this
-- 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 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)
      α'
⊢ 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 α
have hef₀ : 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
-- 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 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)
      α'
hef₀ : Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)
⊢ 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 α
have 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) •
    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)
      α' =
  coroot α
Tactic: rw [h_eq, smul_smul, mul_assoc, inv_mul_cancel₀ hef₀, mul_one, smul_assoc, coroot]
-- 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 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)
      α'
hef₀ : 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₁ :
  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) •
      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) α' =
    coroot α
⊢ 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 α
have h₂ : HMul.hMul (β := K)
      (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))
      ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) •
    α' =
  coroot α
Tactic: rw [h_eq, smul_smul, mul_assoc, inv_mul_cancel₀ hef₀, mul_one, smul_assoc, coroot]
-- 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 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)
      α'
hef₀ : 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₁ :
  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) •
      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) α' =
    coroot α
h₂ :
  HMul.hMul (β := K)
        (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))
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) •
      α' =
    coroot α
⊢ 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 α
have h₃ : (HSMul.hSMul (α := ℕ) (β := K) 2 (((α : (a : ↥H) → K) α')⁻¹ : K) *
      HMul.hMul (α := K) (β := K) (((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f)⁻¹ : K)
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)) •
    α' =
  coroot α
Tactic: rw [h_eq, smul_smul, mul_assoc, inv_mul_cancel₀ hef₀, mul_one, smul_assoc, coroot]
-- 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 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)
      α'
hef₀ : 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₁ :
  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) •
      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) α' =
    coroot α
h₂ :
  HMul.hMul (β := K)
        (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))
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) •
      α' =
    coroot α
h₃ :
  (HSMul.hSMul (α := ℕ) (β := K) 2 (((α : (a : ↥H) → K) α')⁻¹ : K) *
        HMul.hMul (α := K) (β := K) (((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f)⁻¹ : K)
          ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)) •
      α' =
    coroot α
⊢ 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 α
have h₄ : (HSMul.hSMul (α := ℕ) (β := K) 2 (((α : (a : ↥H) → K) α')⁻¹ : K) * 1) • α' = coroot α
Tactic: rw [h_eq, smul_smul, mul_assoc, inv_mul_cancel₀ hef₀, mul_one, smul_assoc, coroot]
-- 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 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)
      α'
hef₀ : 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₁ :
  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) •
      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) α' =
    coroot α
h₂ :
  HMul.hMul (β := K)
        (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))
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) •
      α' =
    coroot α
h₃ :
  (HSMul.hSMul (α := ℕ) (β := K) 2 (((α : (a : ↥H) → K) α')⁻¹ : K) *
        HMul.hMul (α := K) (β := K) (((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f)⁻¹ : K)
          ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)) •
      α' =
    coroot α
h₄ : (HSMul.hSMul (α := ℕ) (β := K) 2 (((α : (a : ↥H) → K) α')⁻¹ : K) * 1) • α' = coroot α
⊢ 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 α
have h₅ : HSMul.hSMul (α := ℕ) (β := K) 2 (((α : (a : ↥H) → K) α')⁻¹ : K) • α' = coroot α
Tactic: rw [h_eq, smul_smul, mul_assoc, inv_mul_cancel₀ hef₀, mul_one, smul_assoc, coroot]
-- 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 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)
      α'
hef₀ : 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₁ :
  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) •
      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) α' =
    coroot α
h₂ :
  HMul.hMul (β := K)
        (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))
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) •
      α' =
    coroot α
h₃ :
  (HSMul.hSMul (α := ℕ) (β := K) 2 (((α : (a : ↥H) → K) α')⁻¹ : K) *
        HMul.hMul (α := K) (β := K) (((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f)⁻¹ : K)
          ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)) •
      α' =
    coroot α
h₄ : (HSMul.hSMul (α := ℕ) (β := K) 2 (((α : (a : ↥H) → K) α')⁻¹ : K) * 1) • α' = coroot α
h₅ : HSMul.hSMul (α := ℕ) (β := K) 2 (((α : (a : ↥H) → K) α')⁻¹ : K) • α' = coroot α
⊢ 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 α
have h₆ : HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul.{u_2, u_3, u_3} (α := K) (((α : (a : ↥H) → K) α')⁻¹ : K) α') = coroot α
Tactic: rw [h_eq, smul_smul, mul_assoc, inv_mul_cancel₀ hef₀, mul_one, smul_assoc, coroot]