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 : PerfectField K
α : Weight K (↥H) L
refine_1 :
  LE.le (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
⊢ Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
have refine_2 : LE.le (α := Submodule K ↥H)
  (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
  (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
Tactic: refine le_antisymm ?_ ?_
-- 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 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
e : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
f : L
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ ⁅e, f⁆ ∈ (↑(K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) : Set L)
have rw : ∃ (a : K),
  HSMul.hSMul (β := L) a (↑(((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)
Tactic: rw [lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα, SetLike.mem_coe,
        Submodule.mem_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 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
⊢ Membership.mem (γ := Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
have this : {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x} ⊆
  (↑(K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) : Set L)
Tactic: have : {⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))} ⊆
        K ∙ ((cartanEquivDual H).symm α : L) := by
      rintro - ⟨e, heα, f, hfα, rfl⟩
      rw [lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα, SetLike.mem_coe,
        Submodule.mem_span_singleton]
      exact ⟨killingForm K L e f, rfl⟩
-- 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 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
this :
  {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x} ⊆
    (↑(K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) : Set L)
⊢ Membership.mem (γ := Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
have hx'₁ : Membership.mem (γ := Submodule K L)
  (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x}) x
Tactic: simp only [LieSubmodule.mem_toSubmodule, mem_corootSpace] at hx'
Cleared hypotheses: hx'
-- 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 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
this :
  {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x} ⊆
    (↑(K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) : Set L)
hx' :
  Membership.mem (γ := Submodule K L)
    (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x}) x
⊢ Membership.mem (γ := Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
have this₁ : Membership.mem (γ := Submodule K L)
  (span K (↑(K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) : Set L)) x
Tactic: replace this := Submodule.span_mono this hx'
Cleared hypotheses: this
-- 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 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K L)
    (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x}) x
this :
  Membership.mem (γ := Submodule K L)
    (span K (↑(K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) : Set L)) x
⊢ Membership.mem (γ := Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
have this₁ : Membership.mem (γ := Submodule K L)
  (K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) x
Tactic: rw [Submodule.span_span] at this
Cleared hypotheses: 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 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K L)
    (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x}) x
this :
  Membership.mem (γ := Submodule K L)
    (K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) x
⊢ Membership.mem (γ := Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
have refine_1 : ∀
  (this :
    ∃ (a : K),
      HSMul.hSMul (β := L) a (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) =
        x),
  ∃ (a : K),
    HSMul.hSMul (β := ↥H) a (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) =
      Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
Tactic: rw [Submodule.mem_span_singleton] at this ⊢
Cleared hypotheses: 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 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K L)
    (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x}) x
this :
  ∃ (a : K),
    HSMul.hSMul (β := L) a (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) = x
⊢ ∃ (a : K),
    HSMul.hSMul (β := ↥H) a (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) =
      Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
have refine_1 : ∀ (t : K)
  (hx :
    HSMul.hSMul (β := L) t (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) ∈ H)
  (hx' :
    Membership.mem (γ := Submodule K L)
      (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x})
      (HSMul.hSMul (β := L) t (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L))),
  ∃ (a : K),
    HSMul.hSMul (β := ↥H) a (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) =
      Subtype.mk (p := fun (x : L) ↦ x ∈ H)
        (HSMul.hSMul (β := L) t (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L))
        hx
Tactic: obtain ⟨t, rfl⟩ := this
Cleared hypotheses: x, hx, hx', 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 : PerfectField K
α : Weight K (↥H) L
⊢ LE.le (α := Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
    (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
have refine_2 : Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieSubmodule K ↥H ↥H) (corootSpace (⇑α : (a : ↥H) → K))
  (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
Tactic: simp only [Submodule.span_singleton_le_iff_mem, LieSubmodule.mem_toSubmodule]
-- 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
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
⊢ x = 0
have inl : ∀ (hαx : Eq.{u_2 + 1} (α := K) (0 x) 0) (hx : Membership.mem (γ := LieIdeal K ↥H) (corootSpace 0) x), x = 0
Tactic: rcases eq_or_ne α 0 with rfl | hα
Cleared hypotheses: α, hαx, 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
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
inl : ∀ (hαx : Eq.{u_2 + 1} (α := K) (0 x) 0) (hx : Membership.mem (γ := LieIdeal K ↥H) (corootSpace 0) x), x = 0
⊢ x = 0
have inr : ∀ (hα : α ≠ 0), x = 0
Tactic: rcases eq_or_ne α 0 with rfl | 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
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
⊢ Membership.mem (γ := Submodule K ↥H) (⨅ (β : Weight K (↥H) L), Weight.ker (M := L) (χ := β)) x
have refine : ∀ (β : Weight K (↥H) L), Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := β)) x
Tactic: refine (Submodule.mem_iInf _).mpr fun β ↦ ?_
-- 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
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
β : Weight K (↥H) L
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := β)) x
have obtain : ∀ (a b : ℤ) (hb : 0 < b) (hab : ∀ x ∈ corootSpace α, (a • α + HSMul.hSMul (β := ↥H → K) b (⇑β : (a : ↥H) → K)) x = 0),
  Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := β)) x
Tactic: obtain ⟨a, b, hb, hab⟩ :=
      exists_forall_mem_corootSpace_smul_add_eq_zero L α β hα β.genWeightSpace_ne_bot
-- 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
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
⊢ x = 0
have hx₁ : Membership.mem (γ := Submodule K ↥H) (⨅ (β : Weight K (↥H) L), Weight.ker (M := L) (χ := β)) x
Tactic: replace hx : x ∈ ⨅ β : Weight K H L, β.ker := by
    refine (Submodule.mem_iInf _).mpr fun β ↦ ?_
    obtain ⟨a, b, hb, hab⟩ :=
      exists_forall_mem_corootSpace_smul_add_eq_zero L α β hα β.genWeightSpace_ne_bot
    simpa [hαx, hb.ne'] using hab _ 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
⊢ Disjoint.{u_3} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α))
    (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
have rw : Eq.{u_3 + 1} (α := Submodule K ↥H)
  (Weight.ker (M := L) (χ := α) ⊓
    LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
  ⊥
Tactic: rw [disjoint_iff]
-- 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.{u_3 + 1} (α := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    ⊥
have refine : ∀ (x : ↥H),
  Membership.mem (γ := Submodule K ↥H)
      (Weight.ker (M := L) (χ := α) ⊓
        LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
      x →
    ∀ (hαx : x ∈ (↑(Weight.ker (M := L) (χ := α)) : Set ↥H))
      (hx :
        x ∈
          (↑(LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) : Set ↥H)),
      x = 0
Tactic: refine (Submodule.eq_bot_iff _).mpr fun x ⟨hαx, hx⟩ ↦ ?_
-- 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 :
  Membership.mem (γ := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    x
hαx : x ∈ (↑(Weight.ker (M := L) (χ := α)) : Set ↥H)
hx : x ∈ (↑(LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) : Set ↥H)
⊢ x = 0
have hαx₁ : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
Tactic: replace hαx : α x = 0 := by simpa using hαx
Cleared hypotheses: hα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
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ Ne.{u_2 + 1} (α := K)
    ((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) : K)
    (0 : K)
have contrapose : ∀
  (hα :
    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)),
  α.IsZero
Tactic: contrapose hα
Cleared hypotheses: 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α :
  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)
this :
  Membership.mem.{u_3, u_3} (α := ↥H) (γ := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
⊢ α.IsZero
have this₁ : Membership.mem.{u_3, u_3} (α := ↥H) (γ := Submodule K ↥H) ⊥
  (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
Tactic: rw [(disjoint_ker_weight_corootSpace α).eq_bot] at this
Cleared hypotheses: 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α :
  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)
⊢ α.IsZero
have suffices : Membership.mem.{u_3, u_3} (α := ↥H) (γ := Submodule K ↥H)
  (Weight.ker (M := L) (χ := α) ⊓
    LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
  (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
Tactic: suffices (cartanEquivDual H).symm α ∈ α.ker ⊓ corootSpace α by
    rw [(disjoint_ker_weight_corootSpace α).eq_bot] at this
    simpa using 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α : α.IsNonZero
⊢ Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (coroot α) : K) (2 : K)
have rw : Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) (coroot α) : K) (2 : K)
Tactic: rw [← Weight.coe_coe]
-- 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
⊢ coroot α = 0 ↔ α.IsZero
have refine_1 : ∀ (hα : coroot α = 0), α.IsZero
Tactic: refine ⟨fun hα ↦ ?_, fun 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
refine_1 : ∀ (hα : coroot α = 0), α.IsZero
⊢ coroot α = 0 ↔ α.IsZero
have refine_2 : ∀ (hα : α.IsZero), coroot α = 0
Tactic: refine ⟨fun hα ↦ ?_, fun 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α : coroot α = 0
⊢ α.IsZero
have refine_1 : ∀ (contra : ¬α.IsZero), False
Tactic: by_contra contra
-- 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 : Eq (α := Submodule K ↥H) (K ∙ coroot α) (K ∙ α')
⊢ Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)
have rw : Eq (α := Submodule K ↥H)
  (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
  (K ∙ coroot α)
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
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
⊢ Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (K ∙ coroot α)
have suffices : Eq (α := Submodule K ↥H) (K ∙ coroot α) (K ∙ α')
Tactic: suffices (K ∙ coroot α) = K ∙ α' by rw [coe_corootSpace_eq_span_singleton']; exact this.symm
-- 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
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
⊢ Eq (α := Submodule K ↥H) (K ∙ coroot α) (K ∙ α')
have this : IsUnit (HMul.hMul (α := K) (β := K) (2 : K) (((α : (a : ↥H) → K) α')⁻¹ : K))
Tactic: have : IsUnit (2 * (α α')⁻¹) := by simpa using root_apply_cartanEquivDual_symm_ne_zero hα