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
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'⁆ ⋯
hh : Ne.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (0 : K)
f : L := HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • f'
⊢ ∃ (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⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
Tactic: replace hef : ⁅⁅e, f⁆, e⁆ = 2 • e := by
    have : ⁅⁅e, f'⁆, e⁆ = α h • e := lie_eq_smul_of_mem_rootSpace heα h
    rw [lie_smul, smul_lie, this, ← smul_assoc, smul_eq_mul, mul_assoc, inv_mul_cancel₀ hh,
      mul_one, two_smul, two_smul]
-- 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_1 :
  ⁅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'⁆ ⋯
hh : Ne.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (0 : K)
f : L := HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • f'
hef : ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
⊢ ∃ (h : L) (e : L) (f : L),
    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
have refine_1 : ∀ (contra : ⁅e, f⁆ = 0), False
Tactic: refine ⟨⁅e, f⁆, e, f, ⟨fun contra ↦ ?_, rfl, hef, ?_⟩, heα, Submodule.smul_mem _ _ 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_1 :
  ⁅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'⁆ ⋯
hh : Ne.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (0 : K)
f : L := HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • f'
hef : ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
refine_1 : ∀ (contra : ⁅e, f⁆ = 0), False
⊢ ∃ (h : L) (e : L) (f : L),
    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
have refine_2 : ⁅⁅e, f⁆, f⁆ = -HSMul.hSMul (α := ℕ) 2 f
Tactic: refine ⟨⁅e, f⁆, e, f, ⟨fun contra ↦ ?_, rfl, hef, ?_⟩, heα, Submodule.smul_mem _ _ hfα⟩
-- 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_1 :
  ⁅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'⁆ ⋯
hh : Ne.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (0 : K)
f : L := HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • f'
hef : ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
contra : ⁅e, f⁆ = 0
⊢ False
have hef₁ : Bracket.bracket (L := L) 0 e = HSMul.hSMul (α := ℕ) 2 e
Tactic: rw [contra] at hef
Cleared hypotheses: hef, contra
-- 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_1 :
  ⁅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'⁆ ⋯
hh : Ne.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (0 : K)
f : L := HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • f'
hef : Bracket.bracket (L := L) 0 e = HSMul.hSMul (α := ℕ) 2 e
contra : ⁅e, f⁆ = 0
⊢ False
have this : IsAddTorsionFree L
Tactic: have : IsAddTorsionFree L := .of_isTorsionFree K L
-- 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_1 :
  ⁅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'⁆ ⋯
hh : Ne.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (0 : K)
f : L := HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • f'
hef : Bracket.bracket (L := L) 0 e = HSMul.hSMul (α := ℕ) 2 e
contra : ⁅e, f⁆ = 0
this : IsAddTorsionFree L
⊢ False
have hef₁ : e = 0
Tactic: simp only [zero_lie, eq_comm (a := (0 : L)), smul_eq_zero, OfNat.ofNat_ne_zero, false_or] at hef
Cleared hypotheses: hef
-- 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_1 :
  ⁅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'⁆ ⋯
hh : Ne.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (0 : K)
f : L := HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • f'
hef : ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅⁅e, f⁆, f⁆ = -HSMul.hSMul (α := ℕ) 2 f
have this : ⁅⁅e, f'⁆, f'⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) (-(α : (a : ↥H) → K) h : K) f'
Tactic: have : ⁅⁅e, f'⁆, f'⁆ = - α h • f' := lie_eq_smul_of_mem_rootSpace hfα 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
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_1 :
  ⁅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'⁆ ⋯
hh : Ne.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (0 : K)
f : L := HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • f'
hef : ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
this : ⁅⁅e, f'⁆, f'⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) (-(α : (a : ↥H) → K) h : K) f'
⊢ ⁅⁅e, f⁆, f⁆ = -HSMul.hSMul (α := ℕ) 2 f
have refine_2 : HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) •
    HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) •
      HSMul.hSMul.{u_2, u_3, u_3} (α := K) (-(α : (a : ↥H) → K) h : K) f' =
  -HSMul.hSMul (α := ℕ) 2 f
Tactic: rw [lie_smul, lie_smul, smul_lie, 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
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ h = (↑(coroot α) : L)
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
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → 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 = (↑(coroot α) : L)
have lift : ∀ (h : ↥H) (ht : IsSl2Triple (↑h : L) e f), (↑h : L) = (↑(coroot α) : L)
Tactic: lift h to H using by simpa only [← ht.lie_e_f, hef] using H.smul_mem _ (Submodule.coe_mem _)
Cleared hypotheses: h, ht
-- 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))
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
ht : IsSl2Triple (↑h : L) e f
⊢ (↑h : L) = (↑(coroot α) : L)
have e_self : h = coroot α
Tactic: congr 1
-- 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))
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
ht : IsSl2Triple (↑h : L) e f
⊢ Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
have this : ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
Tactic: have := lie_eq_smul_of_mem_rootSpace heα h
-- 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))
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
ht : IsSl2Triple (↑h : L) e f
this : ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
⊢ Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
have this₁ : HSMul.hSMul.{u_2, u_3, u_3} (α := K) 2 e = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
Tactic: rw [LieSubalgebra.coe_bracket_of_module, ht.lie_h_e_smul K] at 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))
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
ht : IsSl2Triple (↑h : L) e f
⊢ h = coroot α
have key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
Tactic: have key : α h = 2 := by
    have := lie_eq_smul_of_mem_rootSpace heα h
    rw [LieSubalgebra.coe_bracket_of_module, ht.lie_h_e_smul K] at this
    exact smul_left_injective K ht.e_ne_zero this.symm
-- 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))
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
ht : IsSl2Triple (↑h : L) e f
key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
this : ∃ (s : K), s • h = coroot α
⊢ h = coroot α
have obtain : ∀ (s : K) (hs : s • h = coroot α), h = coroot α
Tactic: obtain ⟨s, hs⟩ := 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))
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
ht : IsSl2Triple (↑h : L) e f
key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
s : K
hs : s • h = coroot α
⊢ h = coroot α
have this : s = 1
Tactic: replace this : s = 1 := by simpa [root_apply_coroot hα, key] using congr_arg α hs
-- 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))
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
ht : IsSl2Triple (↑h : L) e f
key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
s : K
hs : s • h = coroot α
this : s = 1
⊢ h = coroot α
have rwa : ∀ (hs : HSMul.hSMul.{u_2, u_3, u_3} (α := K) 1 h = coroot α) (this : s = 1), h = coroot α
Tactic: rwa [this, one_smul] at hs
Cleared hypotheses: hs, 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
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → 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
ht : IsSl2Triple (↑h : L) e f
key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
s : K
hs : s • h = coroot α
this : s = 1
rwa : ∀ (hs : HSMul.hSMul.{u_2, u_3, u_3} (α := K) 1 h = coroot α) (this : s = 1), h = coroot α
⊢ h = coroot α
have rwa₁ : ∀ (hs : h = coroot α) (this : s = 1), h = coroot α
Tactic: rwa [this, one_smul] at hs
Cleared hypotheses: hs, 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
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → 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
ht : IsSl2Triple (↑h : L) e f
key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
⊢ h = coroot α
have e_self : ∃ (s : K), s • h = coroot α
Tactic: suffices ∃ s : K, s • h = coroot α by
    obtain ⟨s, hs⟩ := this
    replace this : s = 1 := by simpa [root_apply_coroot hα, key] using congr_arg α hs
    rwa [this, one_smul] at hs
-- 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))
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
ht : IsSl2Triple (↑h : L) e f
key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
hef₁ :
  let α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α);
  ⁅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)
⊢ ∃ (s : K), s • h = coroot α
have hα' : let α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α);
α' = ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
Tactic: set α' := (cartanEquivDual H).symm α with hα'
Cleared hypotheses: hef