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
α : Weight K (↥H) L
x : ↥H
⊢ (((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) (coroot α) : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
        (a : ↥H) → K)
      x =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := K) (β := K)
        (((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H))⁻¹ :
          K)
        ((α : (a : ↥H) → K) x : K))
have this : Eq.{u_2 + 1} (α := K)
  ((((cartanEquivDual H : (a : ↥H) → Dual K ↥H)
            (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) :
          Dual.{u_2, u_3} K ↥H) :
        (a : ↥H) → K)
      x :
    K)
  ((α : (a : ↥H) → K) x : K)
Tactic: have : cartanEquivDual H ((cartanEquivDual H).symm α) x = α x := by
    rw [LinearEquiv.apply_symm_apply, Weight.toLinear_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
α : Weight K (↥H) L
x : ↥H
this :
  Eq.{u_2 + 1} (α := K)
    ((((cartanEquivDual H : (a : ↥H) → Dual K ↥H)
              (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) :
            Dual.{u_2, u_3} K ↥H) :
          (a : ↥H) → K)
        x :
      K)
    ((α : (a : ↥H) → K) x : K)
⊢ (((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) (coroot α) : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
        (a : ↥H) → K)
      x =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := K) (β := K)
        (((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H))⁻¹ :
          K)
        ((α : (a : ↥H) → K) x : K))
have rw : HSMul.hSMul (α := ℕ) 2
    (HSMul.hSMul (α := K) (β := K)
      (((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H))⁻¹ : K)
      ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K)
                (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) :
              LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
            (a : ↥H) → K)
          x :
        K)) =
  HSMul.hSMul (α := ℕ) 2
    (HSMul.hSMul (α := K) (β := K)
      (((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H))⁻¹ : K)
      ((α : (a : ↥H) → K) x : K))
Tactic: rw [coroot, map_nsmul, map_smul, LinearMap.smul_apply, LinearMap.smul_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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥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)
have rw : Membership.mem (γ := Submodule K L) (LinearMap.ker (killingForm K 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))
Tactic: rw [← sub_eq_zero, ← Submodule.mem_bot (R := K), ← ker_killingForm_eq_bot]
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
⊢ Membership.mem (γ := Submodule K L) (LinearMap.ker (killingForm K 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))
have hx : ⁅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) ∈
  rootSpace H 0
Tactic: apply mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg (α := (0 : H → K))
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
hx :
  ⁅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) ∈
    rootSpace H 0
⊢ Membership.mem (γ := Submodule K L) (LinearMap.ker (killingForm K 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))
have hx' : ∀ y ∈ rootSpace H (-0),
  Eq.{u_2 + 1} (α := K)
    ((((killingForm K L : (a : L) → L →ₗ[K] K)
              (⁅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)) :
            L →ₗ[K] K) :
          (a : L) → K)
        y :
      K)
    (0 : K)
Tactic: apply mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg (α := (0 : H → K))
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥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) ∈
    rootSpace H 0
have hx : ⁅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
Tactic: simp only [rootSpace_zero_eq, LieSubalgebra.mem_toLieSubmodule]
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥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) ∈
    H
have hx : ⁅e, f⁆ ∈ H
Tactic: refine sub_mem ?_ (H.smul_mem _ α'.property)
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
z : L
hz : z ∈ rootSpace H (-0)
⊢ Eq.{u_2 + 1} (α := K)
    ((((killingForm K L : (a : L) → L →ₗ[K] K)
              (⁅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)) :
            L →ₗ[K] K) :
          (a : L) → K)
        z :
      K)
    (0 : K)
have hz₁ : z ∈ H
Tactic: replace hz : z ∈ H := by simpa using hz
Cleared hypotheses: hz
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
z : L
hz : z ∈ H
⊢ Eq.{u_2 + 1} (α := K)
    ((((killingForm K L : (a : L) → L →ₗ[K] K)
              (⁅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)) :
            L →ₗ[K] K) :
          (a : L) → K)
        z :
      K)
    (0 : K)
have he : ⁅z, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz) : K) e
Tactic: have he : ⁅z, e⁆ = α ⟨z, hz⟩ • e := aux ⟨z, hz⟩
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
z : L
hz : z ∈ H
he :
  ⁅z, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz) : K) e
⊢ Eq.{u_2 + 1} (α := K)
    ((((killingForm K L : (a : L) → L →ₗ[K] K)
              (⁅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)) :
            L →ₗ[K] K) :
          (a : L) → K)
        z :
      K)
    (0 : K)
have hαz : Eq.{u_2 + 1} (α := K)
  ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑α' : L) : L →ₗ[K] K) : (a : L) → K)
      (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz) : L) :
    K)
  ((α : (a : ↥H) → K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz) : K)
Tactic: have hαz : killingForm K L α' (⟨z, hz⟩ : H) = α ⟨z, hz⟩ :=
      LinearMap.BilinForm.apply_toDual_symm_apply (hB := traceForm_cartan_nondegenerate K L 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
α : Weight K (↥H) L
⊢ Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
have obtain : ∀ (e : L) (he₀ : e ≠ 0) (he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e),
  Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
Tactic: obtain ⟨e : L, he₀ : e ≠ 0, he : ∀ x, ⁅x, e⁆ = α x • e⟩ := exists_forall_lie_eq_smul K H 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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
⊢ Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
have heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
Tactic: have heα : e ∈ rootSpace H α := (mem_genWeightSpace L α e).mpr fun x ↦ ⟨1, by simp [← he x]⟩
-- 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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
⊢ ∃ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)),
    Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)
have contrapose! : ∀
  (he₀ :
    ∀ (f : L) (_ : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))),
      Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)),
  e = 0
Tactic: contrapose! he₀
Cleared hypotheses: he₀
-- 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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
⊢ Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
have obtain : ∀ (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)),
  Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
Tactic: obtain ⟨f, hfα, hf⟩ : ∃ f ∈ rootSpace H (-α), killingForm K L e f ≠ 0 := by
    contrapose! he₀
    simpa using mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg K L H heα he₀
-- 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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
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)
⊢ Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
have suffices : ⁅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: suffices ⁅e, f⁆ = killingForm K L e f • ((cartanEquivDual H).symm α : L) from
    (mem_corootSpace α).mpr <| Submodule.subset_span ⟨(killingForm K L e f)⁻¹ • e,
      Submodule.smul_mem _ _ heα, f, hfα, by simpa [inv_smul_eq_iff₀ 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
⊢ Eq (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (span K (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L))) ⊤
have refine : LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤ (LinearMap.range (traceForm K (↥H) L))
Tactic: refine eq_top_iff.mpr (le_trans ?_ (LieModule.range_traceForm_le_span_weight K H L))
-- 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
⊢ LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (LinearMap.range (traceForm K (↥H) L))
have rw : LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
  (LinearMap.range (LinearMap.flip (traceForm K (↥H) L)))
Tactic: rw [← traceForm_flip K H L, ← LinearMap.dualAnnihilator_ker_eq_range_flip,
    ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.dualAnnihilator_bot]
-- 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
rw :
  LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (LinearMap.range (LinearMap.flip (traceForm K (↥H) L)))
⊢ LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (LinearMap.range (traceForm K (↥H) L))
have rw₁ : LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
  (Submodule.dualAnnihilator (LinearMap.ker (traceForm K (↥H) L)))
Tactic: rw [← traceForm_flip K H L, ← LinearMap.dualAnnihilator_ker_eq_range_flip,
    ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.dualAnnihilator_bot]
-- 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
rw :
  LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (LinearMap.range (LinearMap.flip (traceForm K (↥H) L)))
rw₁ :
  LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (Submodule.dualAnnihilator (LinearMap.ker (traceForm K (↥H) L)))
⊢ LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (LinearMap.range (traceForm K (↥H) L))
have rw₂ : LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤ (Submodule.dualAnnihilator ⊥)
Tactic: rw [← traceForm_flip K H L, ← LinearMap.dualAnnihilator_ker_eq_range_flip,
    ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.dualAnnihilator_bot]
-- 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
rw :
  LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (LinearMap.range (LinearMap.flip (traceForm K (↥H) L)))
rw₁ :
  LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (Submodule.dualAnnihilator (LinearMap.ker (traceForm K (↥H) L)))
rw₂ : LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤ (Submodule.dualAnnihilator ⊥)
⊢ LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (LinearMap.range (traceForm K (↥H) L))
have rw₃ : LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤ ⊤
Tactic: rw [← traceForm_flip K H L, ← LinearMap.dualAnnihilator_ker_eq_range_flip,
    ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.dualAnnihilator_bot]
-- 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
⊢ Eq (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (span K (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero})) ⊤
have rw : Eq (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
  (span K (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))
  (span K (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L)))
Tactic: rw [← span_weight_eq_top]
-- 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
⊢ Eq (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (span K (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))
    (span K (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L)))
have refine : LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
  (span K (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L)))
  (span K (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))
Tactic: refine le_antisymm (Submodule.span_mono <| by simp) ?_
-- 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
⊢ LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (span K (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L)))
    (span K (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))
have suffices : Subset (α := Set (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
  (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L))
  (insert 0 (image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}))
Tactic: suffices range (Weight.toLinear K H L) ⊆
    insert 0 ({α : Weight K H L | α.IsNonZero}.image (Weight.toLinear K H L)) by
    simpa only [Submodule.span_insert_zero] using Submodule.span_mono this