awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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'⁆ ⋯
rw 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)
⊢ 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:
rw [Submodule.coe_smul_of_tower]

Premises used: Submodule.coe_smul_of_tower
-- 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 : 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)

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]
-- 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 : 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)
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)
⊢ Ne.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) h : K) (0 : K)

Tactic:
rw [this, map_smul, smul_eq_mul, ne_eq, mul_eq_zero, not_or]

Premises used: mul_eq_zero, ne_eq, not_or, smul_eq_mul, map_smul
-- 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 : 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)
⊢ ¬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:
⟨hf, root_apply_cartanEquivDual_symm_ne_zero hα⟩

Premises used: LieAlgebra.IsKilling.root_apply_cartanEquivDual_symm_ne_zero, And.intro
-- 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 : 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)
⊢ ¬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:
exact ⟨hf, root_apply_cartanEquivDual_symm_ne_zero hα⟩
-- 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 : 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)

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α⟩
-- 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 : 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.{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
-- 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 : 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
rw₉ rw₁₀ : e + e = e + e
⊢ ⁅⁅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]

Premises used: smul_assoc, lie_smul, mul_assoc, two_smul, smul_lie, smul_eq_mul, mul_one, inv_mul_cancel₀
-- 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 : 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

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]
-- 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 : 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))

Tactic:
⟨⁅e, f⁆, e, f, ⟨fun contra ↦ ?_, rfl, hef, ?_⟩, heα, Submodule.smul_mem _ _ hfα⟩

Premises used: Bracket.bracket, IsSl2Triple.mk, And.intro, Exists.intro, rfl, Submodule.smul_mem
-- 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 : 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
refine_2 : ⁅⁅e, f⁆, f⁆ = -HSMul.hSMul (α := ℕ) 2 f
⊢ ∃ (h : L) (e : L) (f : L),
    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))

Tactic:
refine ⟨⁅e, f⁆, e, f, ⟨fun contra ↦ ?_, rfl, hef, ?_⟩, heα, Submodule.smul_mem _ _ hfα⟩
-- 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 : 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
⊢ Bracket.bracket (L := L) 0 e = HSMul.hSMul (α := ℕ) 2 e

Tactic:
rw [contra] at hef
-- 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 : 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
hef₁ : Bracket.bracket (L := L) 0 e = HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅e, f⁆ = 0

Tactic:
rw [contra] at hef
-- 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 : 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
⊢ IsAddTorsionFree L

Tactic:
have : IsAddTorsionFree L := .of_isTorsionFree K L
-- 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 : 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
⊢ e = 0

Tactic:
simp only [zero_lie, eq_comm (a := (0 : L)), smul_eq_zero, OfNat.ofNat_ne_zero, false_or] at hef

Premises used: OfNat.ofNat_ne_zero, false_or, eq_comm, zero_lie, smul_eq_zero
-- 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 : 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'
contra : ⁅e, f⁆ = 0
this : IsAddTorsionFree L
hef : e = 0
⊢ False

Tactic:
contradiction
-- 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 : 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.{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