awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
x m : L
χ : Weight K (↥H) L
x_χ : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
m₁ m₂ : L
hx :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (⨆ (i : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) m₁
hy :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (⨆ (i : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) m₂
ih₁ :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    ⁅x_χ, m₁⁆
ih₂ :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    ⁅x_χ, m₂⁆
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    ⁅x_χ, m₁ + m₂⁆
have mem : ∀
  (ih₁ :
    Membership.mem (γ := Submodule K L)
      (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
        Submodule K L)
      ⁅x_χ, m₁⁆)
  (ih₂ :
    Membership.mem (γ := Submodule K L)
      (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
        Submodule K L)
      ⁅x_χ, m₂⁆),
  Membership.mem (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
      Submodule K L)
    (⁅x_χ, m₁⁆ + ⁅x_χ, m₂⁆)
Tactic: simp only [lie_add, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
Cleared hypotheses: ih₁, ih₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
x m : L
hm :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    m
χ : Weight K (↥H) L
x_χ : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    ⁅x_χ, m⁆
have mem : ∀ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }) (m_α : L)
  (hm_α : m_α ∈ sl2SubmoduleOfRoot sorry),
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
            Submodule K L))))
    ⁅x_χ, m_α⁆
Tactic: induction hm using LieSubmodule.iSup_induction' with
      | mem α m_α hm_α => exact invtSubmoduleToLieIdeal_aux q hq χ x_χ m_α hx_χ α.1 α.2.1 α.2.2 hm_α
      | zero =>
        simp only [Submodule.carrier_eq_coe, lie_zero, SetLike.mem_coe, zero_mem]
      | add m₁ m₂ _ _ ih₁ ih₂ =>
        simp only [lie_add, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
        exact add_mem ih₁ ih₂
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
x m : L
hm :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    m
χ : Weight K (↥H) L
x_χ : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
mem :
  ∀ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }) (m_α : L)
    (hm_α : m_α ∈ sl2SubmoduleOfRoot ⋯),
    Membership.mem (γ := Set L)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
            (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
              Submodule K L))))
      ⁅x_χ, m_α⁆
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    ⁅x_χ, m⁆
have mem₁ : Membership.mem (γ := Set L)
  (AddSubsemigroup.carrier
    (AddSubmonoid.toAddSubsemigroup
      (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
        (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
          Submodule K L))))
  ⁅x_χ, 0⁆
Tactic: induction hm using LieSubmodule.iSup_induction' with
      | mem α m_α hm_α => exact invtSubmoduleToLieIdeal_aux q hq χ x_χ m_α hx_χ α.1 α.2.1 α.2.2 hm_α
      | zero =>
        simp only [Submodule.carrier_eq_coe, lie_zero, SetLike.mem_coe, zero_mem]
      | add m₁ m₂ _ _ ih₁ ih₂ =>
        simp only [lie_add, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
        exact add_mem ih₁ ih₂
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
x m : L
hm :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    m
x₁ x₂ : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : Weight K (↥H) L), genWeightSpace L (⇑i : (a : ↥H) → K)) x₁
hy : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (i : Weight K (↥H) L), genWeightSpace L (⇑i : (a : ↥H) → K)) x₂
ih₁ :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    ⁅x₁, m⁆
ih₂ :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    ⁅x₂, m⁆
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    ⁅x₁ + x₂, m⁆
have add : ∀
  (ih₁ :
    Membership.mem (γ := Submodule K L)
      (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
        Submodule K L)
      ⁅x₁, m⁆)
  (ih₂ :
    Membership.mem (γ := Submodule K L)
      (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
        Submodule K L)
      ⁅x₂, m⁆),
  Membership.mem (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
      Submodule K L)
    (⁅x₁, m⁆ + ⁅x₂, m⁆)
Tactic: simp only [add_lie, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
Cleared hypotheses: ih₁, ih₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
x m : L
hm :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    m
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (χ : Weight K (↥H) L), genWeightSpace L (⇑χ : (a : ↥H) → K)) x
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    ⁅x, m⁆
have mem : ∀ (χ : Weight K (↥H) L) (x_χ : L)
  (hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ),
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
            Submodule K L))))
    ⁅x_χ, m⁆
Tactic: induction hx using LieSubmodule.iSup_induction' with
    | mem χ x_χ hx_χ =>
      induction hm using LieSubmodule.iSup_induction' with
      | mem α m_α hm_α => exact invtSubmoduleToLieIdeal_aux q hq χ x_χ m_α hx_χ α.1 α.2.1 α.2.2 hm_α
      | zero =>
        simp only [Submodule.carrier_eq_coe, lie_zero, SetLike.mem_coe, zero_mem]
      | add m₁ m₂ _ _ ih₁ ih₂ =>
        simp only [lie_add, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
        exact add_mem ih₁ ih₂
    | zero =>
      simp only [Submodule.carrier_eq_coe, zero_lie, SetLike.mem_coe, zero_mem]
    | add x₁ x₂ _ _ ih₁ ih₂ =>
      simp only [add_lie, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
      exact add_mem ih₁ ih₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
x m : L
hm :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    m
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (χ : Weight K (↥H) L), genWeightSpace L (⇑χ : (a : ↥H) → K)) x
mem :
  ∀ (χ : Weight K (↥H) L) (x_χ : L)
    (hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ),
    Membership.mem (γ := Set L)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
            (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
              Submodule K L))))
      ⁅x_χ, m⁆
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
          (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
            Submodule K L))))
    ⁅x, m⁆
have zero : Membership.mem (γ := Set L)
  (AddSubsemigroup.carrier
    (AddSubmonoid.toAddSubsemigroup
      (Submodule.toAddSubmonoid.{u_1, u_2} (R := K)
        (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
          Submodule K L))))
  (Bracket.bracket (L := L) 0 m)
Tactic: induction hx using LieSubmodule.iSup_induction' with
    | mem χ x_χ hx_χ =>
      induction hm using LieSubmodule.iSup_induction' with
      | mem α m_α hm_α => exact invtSubmoduleToLieIdeal_aux q hq χ x_χ m_α hx_χ α.1 α.2.1 α.2.2 hm_α
      | zero =>
        simp only [Submodule.carrier_eq_coe, lie_zero, SetLike.mem_coe, zero_mem]
      | add m₁ m₂ _ _ ih₁ ih₂ =>
        simp only [lie_add, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
        exact add_mem ih₁ ih₂
    | zero =>
      simp only [Submodule.carrier_eq_coe, zero_lie, SetLike.mem_coe, zero_mem]
    | add x₁ x₂ _ _ ih₁ ih₂ =>
      simp only [add_lie, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
      exact add_mem ih₁ ih₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
⊢ LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H =
    ⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯
have rw : (↑(LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H) : Submodule K L) =
  (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
    Submodule K L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.restr_toSubmodule,
    coe_invtSubmoduleToLieIdeal_eq_iSup, LieSubmodule.iSup_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
rw :
  (↑(LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H) : Submodule K L) =
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
⊢ LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H =
    ⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯
have rw₁ : (↑(invtSubmoduleToLieIdeal q hq) : Submodule K L) =
  (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
    Submodule K L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.restr_toSubmodule,
    coe_invtSubmoduleToLieIdeal_eq_iSup, LieSubmodule.iSup_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
rw :
  (↑(LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H) : Submodule K L) =
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
rw₁ :
  (↑(invtSubmoduleToLieIdeal q hq) : Submodule K L) =
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
⊢ LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H =
    ⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯
have rw₂ : Eq.{u_2 + 1} (α := Submodule K L)
  (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
    Submodule K L)
  (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot sorry) :
    Submodule K L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.restr_toSubmodule,
    coe_invtSubmoduleToLieIdeal_eq_iSup, LieSubmodule.iSup_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
rw :
  (↑(LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H) : Submodule K L) =
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
rw₁ :
  (↑(invtSubmoduleToLieIdeal q hq) : Submodule K L) =
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
rw₂ :
  Eq.{u_2 + 1} (α := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
⊢ LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H =
    ⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯
have rw₃ : Eq.{u_2 + 1} (α := Submodule K L)
  (⨆ (i : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }),
    (↑(sl2SubmoduleOfRoot sorry) : Submodule K L))
  (⨆ (i : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }),
    (↑(sl2SubmoduleOfRoot sorry) : Submodule K L))
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.restr_toSubmodule,
    coe_invtSubmoduleToLieIdeal_eq_iSup, LieSubmodule.iSup_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
⊢ Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
    Membership.mem (α := Dual.{u_1, u_2} K ↥H) q
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H)
have mp : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α →
  Membership.mem (α := Dual.{u_1, u_2} K ↥H) q
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
mp :
  Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α →
    Membership.mem (α := Dual.{u_1, u_2} K ↥H) q
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H)
⊢ Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
    Membership.mem (α := Dual.{u_1, u_2} K ↥H) q
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H)
have mpr : Membership.mem (α := Dual.{u_1, u_2} K ↥H) q
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H) →
  Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
Tactic: constructor