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α : ¬α.IsZero
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
this : IsUnit (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) α')⁻¹ : K))
⊢ Eq (α := Submodule K ↥H) (K ∙ coroot α) (K ∙ α')
have change : Eq (α := Submodule K ↥H)
  (K ∙ HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul.{u_2, u_3, u_3} (α := K) (((α : (a : ↥H) → K) α')⁻¹ : K) α')) (K ∙ α')
Tactic: change (K ∙ (2 • (α α')⁻¹ • α')) = _
-- 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
⊢ Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)
have if : ∀ (hα : α.IsZero), Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)
Tactic: if hα : α.IsZero then
    simp [hα.eq, coroot_eq_zero_iff.mpr hα]
  else
    set α' := (cartanEquivDual H).symm α
    suffices (K ∙ coroot α) = K ∙ α' by rw [coe_corootSpace_eq_span_singleton']; exact this.symm
    have : IsUnit (2 * (α α')⁻¹) := by simpa using root_apply_cartanEquivDual_symm_ne_zero hα
    change (K ∙ (2 • (α α')⁻¹ • α')) = _
    simpa [← Nat.cast_smul_eq_nsmul K, smul_smul] using Submodule.span_singleton_smul_eq 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
if : ∀ (hα : α.IsZero), Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)
⊢ Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)
have if₁ : ∀ (hα : ¬α.IsZero), Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)
Tactic: if hα : α.IsZero then
    simp [hα.eq, coroot_eq_zero_iff.mpr hα]
  else
    set α' := (cartanEquivDual H).symm α
    suffices (K ∙ coroot α) = K ∙ α' by rw [coe_corootSpace_eq_span_singleton']; exact this.symm
    have : IsUnit (2 * (α α')⁻¹) := by simpa using root_apply_cartanEquivDual_symm_ne_zero hα
    change (K ∙ (2 • (α α')⁻¹ • α')) = _
    simpa [← Nat.cast_smul_eq_nsmul K, smul_smul] using Submodule.span_singleton_smul_eq 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
x : ↥H
h_mem : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) x
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (2 : K)
⊢ x = coroot α
have pos : ∀ (h₀ : α.IsZero), x = coroot α
Tactic: by_cases h₀ : α.IsZero
-- 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
x : ↥H
h_mem : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) x
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (2 : K)
pos : ∀ (h₀ : α.IsZero), x = coroot α
⊢ x = coroot α
have neg : ∀ (h₀ : ¬α.IsZero), x = coroot α
Tactic: by_cases h₀ : α.IsZero
-- 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
x : ↥H
h_mem : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) x
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (2 : K)
h₀ : ¬α.IsZero
⊢ Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) x
have rwa : Membership.mem (γ := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) x
Tactic: rwa [← coe_corootSpace_eq_span_singleton]
-- 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
x : ↥H
h_mem : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) x
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (2 : K)
h₀ : ¬α.IsZero
⊢ x = coroot α
have h_mem₁ : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) x
Tactic: replace h_mem : x ∈ K ∙ coroot α := by rwa [← coe_corootSpace_eq_span_singleton]
Cleared hypotheses: h_mem
-- 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
x : ↥H
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (2 : K)
h₀ : ¬α.IsZero
h_mem : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) x
⊢ x = coroot α
have neg : ∀ (t : K) (h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (t • coroot α) : K) (2 : K))
  (h_mem : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) (t • coroot α)), t • coroot α = coroot α
Tactic: obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp h_mem
Cleared hypotheses: x, h_two, h_mem
-- 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₀ : ¬α.IsZero
t : K
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (t • coroot α) : K) (2 : K)
h_mem : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) (t • coroot α)
⊢ t • coroot α = coroot α
have neg : t = 1
Tactic: suffices t = 1 by simp [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α : ¬α.IsZero
⊢ IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)
have rw : IsCompl.{u_3} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
Tactic: rw [← coe_corootSpace_eq_span_singleton]
-- 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α : ¬α.IsZero
⊢ IsCompl.{u_3} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α))
    (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
have apply : Ne.{u_3 + 1} (α := Submodule K ↥H)
  (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) ⊥
Tactic: apply Module.Dual.isCompl_ker_of_disjoint_of_ne_bot (by simp_all)
      (disjoint_ker_weight_corootSpace α)
-- 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α : ¬α.IsZero
⊢ Ne.{u_3 + 1} (α := Submodule K ↥H)
    (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) ⊥
have hα₁ : Ne.{u_3 + 1} (α := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) ⊥
Tactic: replace hα : corootSpace α ≠ ⊥ := by simpa using hα
Cleared hypotheses: 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α : Ne.{u_3 + 1} (α := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) ⊥
⊢ Ne.{u_3 + 1} (α := Submodule K ↥H)
    (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) ⊥
have rwa : ∀ (hα : ¬Eq.{u_3 + 1} (α := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) ⊥),
  Ne.{u_3 + 1} (α := Submodule K ↥H)
    (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) ⊥
Tactic: rwa [ne_eq, ← LieSubmodule.toSubmodule_inj] at hα
Cleared hypotheses: 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α : Ne.{u_3 + 1} (α := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) ⊥
rwa :
  ∀ (hα : ¬Eq.{u_3 + 1} (α := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) ⊥),
    Ne.{u_3 + 1} (α := Submodule K ↥H)
      (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) ⊥
⊢ Ne.{u_3 + 1} (α := Submodule K ↥H)
    (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) ⊥
have rwa₁ : ∀
  (hα :
    ¬Eq.{u_3 + 1} (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (↑⊥ : Submodule K ↥H)),
  Ne.{u_3 + 1} (α := Submodule K ↥H)
    (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) ⊥
Tactic: rwa [ne_eq, ← LieSubmodule.toSubmodule_inj] at hα
Cleared hypotheses: 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
⊢ IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)
have if : ∀ (hα : α.IsZero), IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)
Tactic: if hα : α.IsZero then
    simpa [Weight.coe_toLinear_eq_zero_iff.mpr hα, coroot_eq_zero_iff.mpr hα, Weight.ker]
      using isCompl_top_bot
  else
    rw [← coe_corootSpace_eq_span_singleton]
    apply Module.Dual.isCompl_ker_of_disjoint_of_ne_bot (by simp_all)
      (disjoint_ker_weight_corootSpace α)
    replace hα : corootSpace α ≠ ⊥ := by simpa using hα
    rwa [ne_eq, ← LieSubmodule.toSubmodule_inj] at 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
if : ∀ (hα : α.IsZero), IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)
⊢ IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)
have if₁ : ∀ (hα : ¬α.IsZero), IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)
Tactic: if hα : α.IsZero then
    simpa [Weight.coe_toLinear_eq_zero_iff.mpr hα, coroot_eq_zero_iff.mpr hα, Weight.ker]
      using isCompl_top_bot
  else
    rw [← coe_corootSpace_eq_span_singleton]
    apply Module.Dual.isCompl_ker_of_disjoint_of_ne_bot (by simp_all)
      (disjoint_ker_weight_corootSpace α)
    replace hα : corootSpace α ≠ ⊥ := by simpa using hα
    rwa [ne_eq, ← LieSubmodule.toSubmodule_inj] at 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
x y : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
z : ↥H
hz :
  Membership.mem (γ := Set ↥H)
    {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)} z
⊢ Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        z :
      K)
    (0 : K)
have mem : ∀ (u : L) (hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)) (v : L) (huv : ⁅u, v⁆ = (↑z : L)),
  Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        z :
      K)
    (0 : K)
Tactic: obtain ⟨u, hu, v, -, huv⟩ := hz
Cleared hypotheses: hz
-- 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
x y : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
z : ↥H
u : L
hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)
v : L
huv : ⁅u, v⁆ = (↑z : L)
⊢ Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        z :
      K)
    (0 : K)
have mem : Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) (↑z : L) : K)
  (0 : K)
Tactic: change killingForm K L (x : L) (z : L) = 0
-- 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
x y : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
z : ↥H
u : L
hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)
v : L
huv : ⁅u, v⁆ = (↑z : L)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) (↑z : L) : K)
    (0 : K)
have hx₁ : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
Tactic: replace hx : α x = 0 := by simpa using hx
Cleared hypotheses: hx
-- 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
x y z : ↥H
u : L
hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)
v : L
huv : ⁅u, v⁆ = (↑z : L)
hx : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) (↑z : L) : K)
    (0 : K)
have mem : Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) ⁅u, v⁆ : K)
  (0 : K)
Tactic: rw [← huv, ← traceForm_apply_lie_apply, ← LieSubalgebra.coe_bracket_of_module,
      lie_eq_smul_of_mem_rootSpace hu, hx, zero_smul, map_zero, LinearMap.zero_apply]
-- 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
x y z : ↥H
u : L
hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)
v : L
huv : ⁅u, v⁆ = (↑z : L)
hx : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
mem :
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) ⁅u, v⁆ : K)
    (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) (↑z : L) : K)
    (0 : K)
have mem₁ : Eq.{u_2 + 1} (α := K) ((((traceForm K L L : (a : L) → L →ₗ[K] K) ⁅(↑x : L), u⁆ : L →ₗ[K] K) : (a : L) → K) v : K)
  (0 : K)
Tactic: rw [← huv, ← traceForm_apply_lie_apply, ← LieSubalgebra.coe_bracket_of_module,
      lie_eq_smul_of_mem_rootSpace hu, hx, zero_smul, map_zero, LinearMap.zero_apply]
-- 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
x y z : ↥H
u : L
hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)
v : L
huv : ⁅u, v⁆ = (↑z : L)
hx : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
mem :
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) ⁅u, v⁆ : K)
    (0 : K)
mem₁ :
  Eq.{u_2 + 1} (α := K) ((((traceForm K L L : (a : L) → L →ₗ[K] K) ⁅(↑x : L), u⁆ : L →ₗ[K] K) : (a : L) → K) v : K)
    (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) (↑z : L) : K)
    (0 : K)
have mem₂ : Eq.{u_2 + 1} (α := K) ((((traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, u⁆ : L →ₗ[K] K) : (a : L) → K) v : K) (0 : K)
Tactic: rw [← huv, ← traceForm_apply_lie_apply, ← LieSubalgebra.coe_bracket_of_module,
      lie_eq_smul_of_mem_rootSpace hu, hx, zero_smul, map_zero, LinearMap.zero_apply]
-- 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
x y z : ↥H
u : L
hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)
v : L
huv : ⁅u, v⁆ = (↑z : L)
hx : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
mem :
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) ⁅u, v⁆ : K)
    (0 : K)
mem₁ :
  Eq.{u_2 + 1} (α := K) ((((traceForm K L L : (a : L) → L →ₗ[K] K) ⁅(↑x : L), u⁆ : L →ₗ[K] K) : (a : L) → K) v : K)
    (0 : K)
mem₂ :
  Eq.{u_2 + 1} (α := K) ((((traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, u⁆ : L →ₗ[K] K) : (a : L) → K) v : K) (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) (↑z : L) : K)
    (0 : K)
have mem₃ : Eq.{u_2 + 1} (α := K)
  ((((traceForm K L L : (a : L) → L →ₗ[K] K) (HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) u) :
          L →ₗ[K] K) :
        (a : L) → K)
      v :
    K)
  (0 : K)
Tactic: rw [← huv, ← traceForm_apply_lie_apply, ← LieSubalgebra.coe_bracket_of_module,
      lie_eq_smul_of_mem_rootSpace hu, hx, zero_smul, map_zero, LinearMap.zero_apply]
-- 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
x y z : ↥H
u : L
hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)
v : L
huv : ⁅u, v⁆ = (↑z : L)
hx : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
mem :
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) ⁅u, v⁆ : K)
    (0 : K)
mem₁ :
  Eq.{u_2 + 1} (α := K) ((((traceForm K L L : (a : L) → L →ₗ[K] K) ⁅(↑x : L), u⁆ : L →ₗ[K] K) : (a : L) → K) v : K)
    (0 : K)
mem₂ :
  Eq.{u_2 + 1} (α := K) ((((traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, u⁆ : L →ₗ[K] K) : (a : L) → K) v : K) (0 : K)
mem₃ :
  Eq.{u_2 + 1} (α := K)
    ((((traceForm K L L : (a : L) → L →ₗ[K] K) (HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) u) :
            L →ₗ[K] K) :
          (a : L) → K)
        v :
      K)
    (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) (↑z : L) : K)
    (0 : K)
have mem₄ : Eq.{u_2 + 1} (α := K)
  ((((traceForm K L L : (a : L) → L →ₗ[K] K) (HSMul.hSMul.{u_2, u_3, u_3} (α := K) 0 u) : L →ₗ[K] K) : (a : L) → K) v :
    K)
  (0 : K)
Tactic: rw [← huv, ← traceForm_apply_lie_apply, ← LieSubalgebra.coe_bracket_of_module,
      lie_eq_smul_of_mem_rootSpace hu, hx, zero_smul, map_zero, LinearMap.zero_apply]
-- 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
x y z : ↥H
u : L
hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)
v : L
huv : ⁅u, v⁆ = (↑z : L)
hx : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
mem :
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) ⁅u, v⁆ : K)
    (0 : K)
mem₁ :
  Eq.{u_2 + 1} (α := K) ((((traceForm K L L : (a : L) → L →ₗ[K] K) ⁅(↑x : L), u⁆ : L →ₗ[K] K) : (a : L) → K) v : K)
    (0 : K)
mem₂ :
  Eq.{u_2 + 1} (α := K) ((((traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, u⁆ : L →ₗ[K] K) : (a : L) → K) v : K) (0 : K)
mem₃ :
  Eq.{u_2 + 1} (α := K)
    ((((traceForm K L L : (a : L) → L →ₗ[K] K) (HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) u) :
            L →ₗ[K] K) :
          (a : L) → K)
        v :
      K)
    (0 : K)
mem₄ :
  Eq.{u_2 + 1} (α := K)
    ((((traceForm K L L : (a : L) → L →ₗ[K] K) (HSMul.hSMul.{u_2, u_3, u_3} (α := K) 0 u) : L →ₗ[K] K) : (a : L) → K)
        v :
      K)
    (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) (↑z : L) : K)
    (0 : K)
have mem₅ : Eq.{u_2 + 1} (α := K) (((traceForm K L L : (a : L) → L →ₗ[K] K) 0 : (a : L) → K) v : K) (0 : K)
Tactic: rw [← huv, ← traceForm_apply_lie_apply, ← LieSubalgebra.coe_bracket_of_module,
      lie_eq_smul_of_mem_rootSpace hu, hx, zero_smul, map_zero, LinearMap.zero_apply]