awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
⊢ Ne (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
have pos : ∀ (hα : α.IsZero), Ne (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
Tactic: by_cases hα : α.IsZero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
pos : ∀ (hα : α.IsZero), Ne (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
⊢ Ne (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
have neg : ∀ (hα : ¬α.IsZero), Ne (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
Tactic: by_cases hα : α.IsZero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : α.IsZero
⊢ Ne (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
have h : Eq (α := ↥H → K) (-(⇑α : (a : ↥H) → K)) (⇑α : (a : ↥H) → K)
Tactic: convert! α.genWeightSpace_ne_bot
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : α.IsZero
⊢ Eq (α := ↥H → K) (-(⇑α : (a : ↥H) → K)) (⇑α : (a : ↥H) → K)
have h : Eq (α := ↥H → K) (-0) 0
Tactic: rw [hα, neg_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : α.IsZero
h : Eq (α := ↥H → K) (-0) 0
⊢ Eq (α := ↥H → K) (-(⇑α : (a : ↥H) → K)) (⇑α : (a : ↥H) → K)
have h₁ : Eq (α := ↥H → K) 0 0
Tactic: rw [hα, neg_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
⊢ False
have neg : ∀ (x : L) (hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x) (x_ne0 : x ≠ 0),
  False
Tactic: obtain ⟨x, hx, x_ne0⟩ := α.exists_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
y : L
hy : y ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
have hy₁ : Membership.mem (γ := LieSubmodule K (↥H) L) ⊥ y
Tactic: rw [rootSpace, e] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
y : L
hy : Membership.mem (γ := LieSubmodule K (↥H) L) ⊥ y
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
have rw : Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) 0 : K) (0 : K)
Tactic: rw [hy, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
y : L
hy : Membership.mem (γ := LieSubmodule K (↥H) L) ⊥ y
rw : Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) 0 : K) (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K) (0 : K)
have rw₁ : Eq.{u_2 + 1} (α := K) 0 0
Tactic: rw [hy, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
⊢ False
have this : Membership.mem (γ := Submodule K L) (LinearMap.ker (killingForm K L)) x
Tactic: have := mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg K L H hx
        (fun y hy ↦ by rw [rootSpace, e] at hy; rw [hy, map_zero])
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (hypothesis)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
this : Membership.mem (γ := Submodule K L) (LinearMap.ker (killingForm K L)) x
⊢ False
have this₁ : Membership.mem (γ := Submodule K L) ⊥ x
Tactic: rw [ker_killingForm_eq_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
⊢ { toFun := -(⇑({ toFun := -(⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := ⋯ } : Weight K (↥H) L) : (a : ↥H) → K),
      genWeightSpace_ne_bot' := ⋯ } =
    α
have h : ∀ (x : ↥H),
  Eq.{u_2 + 1} (α := K)
    ((({ toFun := -(⇑({ toFun := -(⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := sorry } : Weight K (↥H) L) : (a : ↥H) → K),
              genWeightSpace_ne_bot' := sorry } :
            Weight K (↥H) L) :
          (a : ↥H) → K)
        x :
      K)
    ((α : (a : ↥H) → K) x : K)
Tactic: ext
-- 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
inst_4 : IsKilling K L
H : LieSubalgebra K L
inst_5 : H.IsCartanSubalgebra
inst_6 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
⊢ (-α).IsZero
have h₁ : ∀ (x : ↥H), Eq.{u_2 + 1} (α := K) ((-α : (a : ↥H) → K) x : K) (0 x : K)
Tactic: ext
-- 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
inst_4 : IsKilling K L
H : LieSubalgebra K L
inst_5 : H.IsCartanSubalgebra
inst_6 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
x : ↥H
⊢ Eq.{u_2 + 1} (α := K) ((-α : (a : ↥H) → K) x : K) (0 x : K)
have h₁ : Eq.{u_2 + 1} (α := K) ((-(⇑α : (a : ↥H) → K)) x : K) (0 x : K)
Tactic: rw [coe_neg, h, neg_zero]
-- 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
inst_4 : IsKilling K L
H : LieSubalgebra K L
inst_5 : H.IsCartanSubalgebra
inst_6 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
x : ↥H
h₁ : Eq.{u_2 + 1} (α := K) ((-(⇑α : (a : ↥H) → K)) x : K) (0 x : K)
⊢ Eq.{u_2 + 1} (α := K) ((-α : (a : ↥H) → K) x : K) (0 x : K)
have h₂ : Eq.{u_2 + 1} (α := K) ((-0) x) (0 x)
Tactic: rw [coe_neg, h, neg_zero]
-- 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
inst_4 : IsKilling K L
H : LieSubalgebra K L
inst_5 : H.IsCartanSubalgebra
inst_6 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
x : ↥H
h₁ : Eq.{u_2 + 1} (α := K) ((-(⇑α : (a : ↥H) → K)) x : K) (0 x : K)
h₂ : Eq.{u_2 + 1} (α := K) ((-0) x) (0 x)
⊢ Eq.{u_2 + 1} (α := K) ((-α : (a : ↥H) → K) x : K) (0 x : K)
have h₃ : Eq.{u_2 + 1} (α := K) (0 x) (0 x)
Tactic: rw [coe_neg, h, neg_zero]
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
this :
  Membership.mem (γ := Submodule K ↥H) (LinearMap.ker (traceForm K (↥H) L)) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
⊢ x = 0
have this₁ : Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx = 0
Tactic: simp only [ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.mem_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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
⊢ x = 0
have suffices : Membership.mem (γ := Submodule K ↥H) (LinearMap.ker (traceForm K (↥H) L)) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
Tactic: suffices ⟨x, hx⟩ ∈ LinearMap.ker (traceForm K H L) by
    simp only [ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.mem_bot] at this
    exact (AddSubmonoid.mk_eq_zero H.toAddSubmonoid).mp 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
⊢ Eq (α := LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)
    ((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) :
      LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)
    (0 : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)
have h : ∀ (y : ↥H),
  Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        y :
      K)
    ((0 : (a : ↥H) → K) y : K)
Tactic: ext y
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
y : ↥H
⊢ Commute (S := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
    ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)
have rw : Eq (α := End K L)
  (Bracket.bracket (L := End K L)
      ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
      ((toEnd K (↥H) L : (a : ↥H) → End K L) y) :
    End K L)
  (0 : End K L)
Tactic: rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
y : ↥H
rw :
  Eq (α := End K L)
    (Bracket.bracket (L := End K L)
        ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
        ((toEnd K (↥H) L : (a : ↥H) → End K L) y) :
      End K L)
    (0 : End K L)
⊢ Commute (S := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
    ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)
have rw₁ : Eq (α := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx, y⁆ : End K L)
  (0 : End K L)
Tactic: rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
y : ↥H
rw :
  Eq (α := End K L)
    (Bracket.bracket (L := End K L)
        ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
        ((toEnd K (↥H) L : (a : ↥H) → End K L) y) :
      End K L)
    (0 : End K L)
rw₁ :
  Eq (α := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx, y⁆ : End K L)
    (0 : End K L)
⊢ Commute (S := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
    ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)
have rw₂ : Eq (α := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) 0 : End K L) (0 : End K L)
Tactic: rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
y : ↥H
rw :
  Eq (α := End K L)
    (Bracket.bracket (L := End K L)
        ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
        ((toEnd K (↥H) L : (a : ↥H) → End K L) y) :
      End K L)
    (0 : End K L)
rw₁ :
  Eq (α := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx, y⁆ : End K L)
    (0 : End K L)
rw₂ : Eq (α := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) 0 : End K L) (0 : End K L)
⊢ Commute (S := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
    ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)
have rw₃ : Eq.{u_3 + 1} (α := End K L) 0 0
Tactic: rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
y : ↥H
⊢ Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        y :
      K)
    ((0 : (a : ↥H) → K) y : K)
have comm : Commute (S := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
  ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)
Tactic: have comm : Commute (toEnd K H L ⟨x, hx⟩) (toEnd K H L y) := by
    rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
y : ↥H
comm :
  Commute (S := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
    ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)
⊢ Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        y :
      K)
    ((0 : (a : ↥H) → K) y : K)
have h : Eq.{u_2 + 1} (α := K)
  ((LinearMap.trace K L : (a : L →ₗ[K] L) → K)
      (HMul.hMul (α := End K L) (β := End K L)
        ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
        ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)) :
    K)
  (0 : K)
Tactic: rw [traceForm_apply_apply, ← Module.End.mul_eq_comp, 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
⊢ Eq.{u_3 + 1} (α := LieIdeal K ↥H) (corootSpace 0) ⊥
have refine : ∀ (x : ↥H) (hx : Membership.mem (γ := LieSubmodule K ↥H ↥H) (corootSpace 0) x),
  Membership.mem (γ := LieSubmodule K ↥H ↥H) ⊥ x
Tactic: refine eq_bot_iff.mpr fun 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
x : ↥H
hx : Membership.mem (γ := LieSubmodule K ↥H ↥H) (corootSpace 0) x
⊢ Membership.mem (γ := LieSubmodule K ↥H ↥H) ⊥ x
have suffices : Eq (α := Set L) {x : L | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} {0}
Tactic: suffices {x | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} = {0} by simpa [mem_corootSpace, this] using 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
x : ↥H
hx : Membership.mem (γ := LieSubmodule K ↥H ↥H) (corootSpace 0) x
⊢ Eq (α := Set L) {x : L | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} {0}
have refine : ∀ (x : L), Membership.mem (γ := Set L) {x : L | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} x → x = 0
Tactic: refine eq_singleton_iff_unique_mem.mpr ⟨⟨0, H.zero_mem, 0, H.zero_mem, zero_lie 0⟩, ?_⟩
-- 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
x : ↥H
hx : Membership.mem (γ := LieSubmodule K ↥H ↥H) (corootSpace 0) x
y : L
hy : y ∈ H
z : L
hz : z ∈ H
⊢ ⁅y, z⁆ = 0
have suffices : ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy, Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz⁆ = 0
Tactic: suffices ⁅(⟨y, hy⟩ : H), (⟨z, hz⟩ : H)⁆ = 0 by
    simpa only [Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero] 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
α : Weight K (↥H) L
x : ↥H
⊢ 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)
have rw : Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) x : K) ((α : (a : ↥H) → K) x : K)
Tactic: 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
rw : Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) x : K) ((α : (a : ↥H) → K) x : K)
⊢ 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)
have rw₁ : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) ((α : (a : ↥H) → K) x : K)
Tactic: rw [LinearEquiv.apply_symm_apply, Weight.toLinear_apply]