-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
h : ↥H
ht : IsSl2Triple (↑h : L) e f
key : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (2 : K)
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
hef :
  ⁅e, f⁆ =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      (↑α' : L)
hα' : α' = ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
h_eq :
  h =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      α'
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 α
h₆ : HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul.{u_2, u_3, u_3} (α := K) (((α : (a : ↥H) → K) α')⁻¹ : K) α') = coroot α
h₇ h₈ :
  HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul.{u_2, u_3, u_3} (α := K) (((α : (a : ↥H) → K) α')⁻¹ : K) α') =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := ↥H)
        (((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H))⁻¹ :
          K)
        (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥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:
rw [h_eq, smul_smul, mul_assoc, inv_mul_cancel₀ hef₀, mul_one, smul_assoc, coroot]

Premises used: smul_assoc, LieAlgebra.IsKilling.coroot, mul_assoc, smul_smul, mul_one, inv_mul_cancel₀