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 : 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'⁆ ⋯
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)
⊢ Ne.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (0 : K)
have rw : ¬Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f' : K) (0 : K) ∧
  ¬Eq.{u_2 + 1} (α := K)
      ((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) : K)
      (0 : K)
Tactic: rw [this, map_smul, smul_eq_mul, ne_eq, mul_eq_zero, not_or]
-- 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'⁆ ⋯
⊢ ∃ (h : L) (e : L) (f : L),
    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
have hh : Ne.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (0 : K)
Tactic: have hh : α h ≠ 0 := by
    have : h = killingForm K L e f' • (cartanEquivDual H).symm α := by
      simp only [h, Subtype.ext_iff, hef]
      rw [Submodule.coe_smul_of_tower]
    rw [this, map_smul, smul_eq_mul, ne_eq, mul_eq_zero, not_or]
    exact ⟨hf, root_apply_cartanEquivDual_symm_ne_zero 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 : 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'
⊢ ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
have this : ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
Tactic: have : ⁅⁅e, f'⁆, e⁆ = α h • e := lie_eq_smul_of_mem_rootSpace heα 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 :
  ⁅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'
this : ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
⊢ ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
have rw : ⁅HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
Tactic: 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 :
  ⁅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'
this : ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
rw : ⁅HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
have rw₁ : HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
Tactic: 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 :
  ⁅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'
this : ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
rw : ⁅HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₁ : HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
have rw₂ : 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) e =
  HSMul.hSMul (α := ℕ) 2 e
Tactic: 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 :
  ⁅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'
this : ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
rw : ⁅HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₁ : HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₂ :
  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) e =
    HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
have rw₃ : HSMul.hSMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) •
    e =
  HSMul.hSMul (α := ℕ) 2 e
Tactic: 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 :
  ⁅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'
this : ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
rw : ⁅HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₁ : HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₂ :
  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) e =
    HSMul.hSMul (α := ℕ) 2 e
rw₃ :
  HSMul.hSMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) •
      e =
    HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
have rw₄ : HMul.hMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) • e =
  HSMul.hSMul (α := ℕ) 2 e
Tactic: 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 :
  ⁅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'
this : ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
rw : ⁅HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₁ : HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₂ :
  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) e =
    HSMul.hSMul (α := ℕ) 2 e
rw₃ :
  HSMul.hSMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) •
      e =
    HSMul.hSMul (α := ℕ) 2 e
rw₄ :
  HMul.hMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) •
      e =
    HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
have rw₅ : (2 * HMul.hMul (α := K) (β := K) (((α : (a : ↥H) → K) h)⁻¹ : K) ((α : (a : ↥H) → K) h : K)) • e =
  HSMul.hSMul (α := ℕ) 2 e
Tactic: 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 :
  ⁅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'
this : ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
rw : ⁅HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₁ : HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₂ :
  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) e =
    HSMul.hSMul (α := ℕ) 2 e
rw₃ :
  HSMul.hSMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) •
      e =
    HSMul.hSMul (α := ℕ) 2 e
rw₄ :
  HMul.hMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) •
      e =
    HSMul.hSMul (α := ℕ) 2 e
rw₅ :
  (2 * HMul.hMul (α := K) (β := K) (((α : (a : ↥H) → K) h)⁻¹ : K) ((α : (a : ↥H) → K) h : K)) • e =
    HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
have rw₆ : HMul.hMul (α := K) 2 1 • e = HSMul.hSMul (α := ℕ) 2 e
Tactic: 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 :
  ⁅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'
this : ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
rw : ⁅HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₁ : HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₂ :
  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) e =
    HSMul.hSMul (α := ℕ) 2 e
rw₃ :
  HSMul.hSMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) •
      e =
    HSMul.hSMul (α := ℕ) 2 e
rw₄ :
  HMul.hMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) •
      e =
    HSMul.hSMul (α := ℕ) 2 e
rw₅ :
  (2 * HMul.hMul (α := K) (β := K) (((α : (a : ↥H) → K) h)⁻¹ : K) ((α : (a : ↥H) → K) h : K)) • e =
    HSMul.hSMul (α := ℕ) 2 e
rw₆ : HMul.hMul (α := K) 2 1 • e = HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
have rw₇ : HSMul.hSMul.{u_2, u_3, u_3} (α := K) 2 e = HSMul.hSMul (α := ℕ) 2 e
Tactic: 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 :
  ⁅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'
this : ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
rw : ⁅HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₁ : HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₂ :
  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) e =
    HSMul.hSMul (α := ℕ) 2 e
rw₃ :
  HSMul.hSMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) •
      e =
    HSMul.hSMul (α := ℕ) 2 e
rw₄ :
  HMul.hMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) •
      e =
    HSMul.hSMul (α := ℕ) 2 e
rw₅ :
  (2 * HMul.hMul (α := K) (β := K) (((α : (a : ↥H) → K) h)⁻¹ : K) ((α : (a : ↥H) → K) h : K)) • e =
    HSMul.hSMul (α := ℕ) 2 e
rw₆ : HMul.hMul (α := K) 2 1 • e = HSMul.hSMul (α := ℕ) 2 e
rw₇ : HSMul.hSMul.{u_2, u_3, u_3} (α := K) 2 e = HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
have rw₈ : e + e = HSMul.hSMul (α := ℕ) 2 e
Tactic: 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 :
  ⁅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'
this : ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
rw : ⁅HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₁ : HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K) • ⁅⁅e, f'⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₂ :
  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) e =
    HSMul.hSMul (α := ℕ) 2 e
rw₃ :
  HSMul.hSMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) •
      e =
    HSMul.hSMul (α := ℕ) 2 e
rw₄ :
  HMul.hMul (β := K) (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) h)⁻¹ : K)) ((α : (a : ↥H) → K) h : K) •
      e =
    HSMul.hSMul (α := ℕ) 2 e
rw₅ :
  (2 * HMul.hMul (α := K) (β := K) (((α : (a : ↥H) → K) h)⁻¹ : K) ((α : (a : ↥H) → K) h : K)) • e =
    HSMul.hSMul (α := ℕ) 2 e
rw₆ : HMul.hMul (α := K) 2 1 • e = HSMul.hSMul (α := ℕ) 2 e
rw₇ : HSMul.hSMul.{u_2, u_3, u_3} (α := K) 2 e = HSMul.hSMul (α := ℕ) 2 e
rw₈ : e + e = HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅⁅e, f⁆, e⁆ = HSMul.hSMul (α := ℕ) 2 e
have rw₉ : e + e = e + e
Tactic: rw [lie_smul, smul_lie, this, ← smul_assoc, smul_eq_mul, mul_assoc, inv_mul_cancel₀ hh,
      mul_one, two_smul, two_smul]