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
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)
mem₅ : Eq.{u_2 + 1} (α := K) (((traceForm K L L : (a : L) → L →ₗ[K] K) 0 : (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) ((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]
-- 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)
mem₅ : Eq.{u_2 + 1} (α := K) (((traceForm K L L : (a : L) → L →ₗ[K] K) 0 : (a : L) → K) v : K) (0 : K)
mem₆ : Eq.{u_2 + 1} (α := K) ((0 : (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) 0 0
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 : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
hy :
  Membership.mem (γ := Submodule K ↥H)
    (span K
      {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)})
    y
⊢ 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)
        y :
      K)
    (0 : K)
have mem : ∀ (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)
Tactic: induction hy using Submodule.span_induction with
  | mem z hz =>
    obtain ⟨u, hu, v, -, huv⟩ := hz
    change killingForm K L (x : L) (z : L) = 0
    replace hx : α x = 0 := by simpa using hx
    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]
  | zero => simp
  | add _ _ _ _ hx hy => simp [hx, hy]
  | smul _ _ _ hz => simp [hz]
Cleared hypotheses: hy
-- 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
hy :
  Membership.mem (γ := Submodule K ↥H)
    (span K
      {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)})
    y
mem :
  ∀ (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)
⊢ 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)
        y :
      K)
    (0 : K)
have zero : 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)
      0 :
    K)
  (0 : K)
Tactic: induction hy using Submodule.span_induction with
  | mem z hz =>
    obtain ⟨u, hu, v, -, huv⟩ := hz
    change killingForm K L (x : L) (z : L) = 0
    replace hx : α x = 0 := by simpa using hx
    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]
  | zero => simp
  | add _ _ _ _ hx hy => simp [hx, hy]
  | smul _ _ _ hz => simp [hz]
Cleared hypotheses: hy
-- 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
hy :
  Membership.mem (γ := Submodule K ↥H)
    (span K
      {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)})
    y
mem :
  ∀ (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)
zero :
  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)
        0 :
      K)
    (0 : K)
⊢ 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)
        y :
      K)
    (0 : K)
have add : ∀ (x_1 y : ↥H),
  Membership.mem (γ := Submodule K ↥H)
      (span K
        {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)})
      x_1 →
    Membership.mem (γ := Submodule K ↥H)
        (span K
          {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)})
        y →
      ∀
        (hx :
          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)
                x_1 :
              K)
            (0 : K))
        (hy :
          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)
                y :
              K)
            (0 : K)),
        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)
              (x_1 + y) :
            K)
          (0 : K)
Tactic: induction hy using Submodule.span_induction with
  | mem z hz =>
    obtain ⟨u, hu, v, -, huv⟩ := hz
    change killingForm K L (x : L) (z : L) = 0
    replace hx : α x = 0 := by simpa using hx
    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]
  | zero => simp
  | add _ _ _ _ hx hy => simp [hx, hy]
  | smul _ _ _ hz => simp [hz]
Cleared hypotheses: hy
-- 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
⊢ Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := α))
have hα' : coroot α = 0
Tactic: have hα' : coroot α = 0 := by simpa
-- 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α' : coroot α = 0
⊢ Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) ⊤
have h : ∀ (x : ↥H),
  Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x ↔ Membership.mem (γ := Submodule K ↥H) ⊤ x
Tactic: ext
-- 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α' : coroot α = 0
⊢ Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := α))
have hα₁ : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) ⊤
Tactic: replace hα : α.ker = ⊤ := by ext; simp [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α : ¬α.IsZero
⊢ Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := α))
have refine_1 : ∀ (x : ↥H)
  (hx : Membership.mem (γ := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α)) x),
  Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
Tactic: refine le_antisymm (fun x hx ↦ ?_) (fun x hx y hy ↦ ?_)
-- 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
refine_1 :
  ∀ (x : ↥H)
    (hx : Membership.mem (γ := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α)) x),
    Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
⊢ Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := α))
have refine_2 : ∀ (x : ↥H) (hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x) (y : ↥H)
  (hy : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) y), LinearMap.IsOrtho (traceForm K (↥H) L) y x
Tactic: refine le_antisymm (fun x hx ↦ ?_) (fun x hx y hy ↦ ?_)
-- 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
x : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α)) x
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
have hx₁ : ∀ (n : ↥H), Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) n → LinearMap.BilinForm.IsOrtho (traceForm K (↥H) L) n x
Tactic: simp only [LinearMap.BilinForm.mem_orthogonal_iff] 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 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
x : ↥H
hx :
  ∀ (n : ↥H),
    Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) n → LinearMap.BilinForm.IsOrtho (traceForm K (↥H) L) n x
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
have hx₁ : LinearMap.BilinForm.IsOrtho (traceForm K (↥H) L) (coroot α) x
Tactic: specialize hx (coroot α) (Submodule.mem_span_singleton_self _)
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 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
x : ↥H
hx : LinearMap.BilinForm.IsOrtho (traceForm K (↥H) L) (coroot α) x
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
have hx₁ : 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) ∨
  Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
Tactic: simp only [LinearMap.BilinForm.isOrtho_def, traceForm_coroot, smul_eq_mul, nsmul_eq_mul,
        Nat.cast_ofNat, mul_eq_zero, OfNat.ofNat_ne_zero, inv_eq_zero, false_or] 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 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
x : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
y : ↥H
hy : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) y
⊢ LinearMap.IsOrtho (traceForm K (↥H) L) y x
have this : 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)
      y :
    K)
  (0 : K)
Tactic: have := traceForm_eq_zero_of_mem_ker_of_mem_span_coroot hx hy
-- 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
x : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
y : ↥H
hy : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) y
this :
  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)
        y :
      K)
    (0 : K)
⊢ LinearMap.IsOrtho (traceForm K (↥H) L) y x
have refine_2 : ∀
  (this :
    Eq.{u_2 + 1} (α := K)
      ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) y : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
            (a : ↥H) → K)
          x :
        K)
      (0 : K)),
  LinearMap.IsOrtho (traceForm K (↥H) L) y x
Tactic: rwa [traceForm_comm] 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
⊢ Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := α))
have if : ∀ (hα : α.IsZero),
  Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := α))
Tactic: if hα : α.IsZero then
    have hα' : coroot α = 0 := by simpa
    replace hα : α.ker = ⊤ := by ext; simp [hα]
    simp [hα, hα']
  else
    refine le_antisymm (fun x hx ↦ ?_) (fun x hx y hy ↦ ?_)
    · simp only [LinearMap.BilinForm.mem_orthogonal_iff] at hx
      specialize hx (coroot α) (Submodule.mem_span_singleton_self _)
      simp only [LinearMap.BilinForm.isOrtho_def, traceForm_coroot, smul_eq_mul, nsmul_eq_mul,
        Nat.cast_ofNat, mul_eq_zero, OfNat.ofNat_ne_zero, inv_eq_zero, false_or] at hx
      simpa using hx.resolve_left (root_apply_cartanEquivDual_symm_ne_zero hα)
    · have := traceForm_eq_zero_of_mem_ker_of_mem_span_coroot hx hy
      rwa [traceForm_comm] at 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) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
      (Weight.ker (M := L) (χ := α))
⊢ Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := α))
have if₁ : ∀ (hα : ¬α.IsZero),
  Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := α))
Tactic: if hα : α.IsZero then
    have hα' : coroot α = 0 := by simpa
    replace hα : α.ker = ⊤ := by ext; simp [hα]
    simp [hα, hα']
  else
    refine le_antisymm (fun x hx ↦ ?_) (fun x hx y hy ↦ ?_)
    · simp only [LinearMap.BilinForm.mem_orthogonal_iff] at hx
      specialize hx (coroot α) (Submodule.mem_span_singleton_self _)
      simp only [LinearMap.BilinForm.isOrtho_def, traceForm_coroot, smul_eq_mul, nsmul_eq_mul,
        Nat.cast_ofNat, mul_eq_zero, OfNat.ofNat_ne_zero, inv_eq_zero, false_or] at hx
      simpa using hx.resolve_left (root_apply_cartanEquivDual_symm_ne_zero hα)
    · have := traceForm_eq_zero_of_mem_ker_of_mem_span_coroot hx hy
      rwa [traceForm_comm] at 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 : α = β
⊢ coroot α = coroot β
have rw : coroot β = coroot β
Tactic: rw [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
⊢ coroot α = coroot β ↔ α = β
have refine : ∀ (hyp : coroot α = coroot β), α = β
Tactic: refine ⟨fun hyp ↦ ?_, fun h ↦ by rw [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
hyp : coroot α = coroot β
hα : α.IsZero
⊢ β.IsZero
have rw : ∀ (hα : coroot α = 0), coroot β = 0
Tactic: rw [← coroot_eq_zero_iff] at 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
hyp : coroot α = coroot β
hα : α.IsZero
⊢ α = β
have hβ : β.IsZero
Tactic: have hβ : β.IsZero := by
      rw [← coroot_eq_zero_iff] at hα ⊢
      rwa [← hyp]
-- 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
hyp : coroot α = coroot β
hα : α.IsZero
hβ : β.IsZero
⊢ α = β
have h : ∀ (x : ↥H), Eq.{u_2 + 1} (α := K) ((α : (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
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
⊢ β.IsNonZero
have contrapose : ∀ (hα : β.IsZero), α.IsZero
Tactic: contrapose 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
hyp : coroot α = coroot β
hα : β.IsZero
⊢ α.IsZero
have simp : ∀ (hα : coroot β = 0), coroot α = 0
Tactic: simp only [← coroot_eq_zero_iff] at hα ⊢
Cleared hypotheses: hα