awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_pairing_zero : S.pairing i j = 0
h_pos_zero : ⁅x_χ, m_pos⁆ = 0
h_neg_zero : ⁅x_χ, m_neg⁆ = 0
h_chi_coroot_zero : Eq.{u_1 + 1} (α := K) ((χ : (a : ↥H) → K) (coroot α) : K) (0 : K)
h_lie_eq_smul : ⁅(↑y : L), x_χ⁆ = HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((χ : (a : ↥H) → K) y : K) x_χ
h_chi_h_zero : Eq.{u_1 + 1} (α := K) ((χ : (a : ↥H) → K) y : K) (0 : K)
h_bracket_elem : ⁅x_χ, (↑y : L)⁆ = 0
⊢ ⁅x_χ, (↑y : L)⁆ = 0

Tactic:
exact h_bracket_elem
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_pairing_zero : S.pairing i j = 0
h_pos_zero : ⁅x_χ, m_pos⁆ = 0
h_neg_zero : ⁅x_χ, m_neg⁆ = 0
h_bracket_zero : ⁅x_χ, (↑y : L)⁆ = 0
rw :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯)
    (HAdd.hAdd (α := L) 0 0 + 0)
⊢ Membership.mem (γ := LieSubmodule K (↥H) L)
    (⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) ⁅x_χ, m_α⁆

Tactic:
rw [h_bracket_sum, h_pos_zero, h_neg_zero, h_bracket_zero]
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑χ : (a : ↥H) → K)) x_χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, (↑y : L)⁆
h_pos_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_pos⁆
h_neg_containment :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HSub.hSub (α := (a : ↥H) → K) (⇑χ : (a : ↥H) → K) (⇑α : (a : ↥H) → K))) ⁅x_χ, m_neg⁆
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
exists_root_index :
  ∀ (γ : Weight K (↥H) L) (hγ : γ.IsNonZero),
    ∃ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L γ
h_plus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
h_minus_bot :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) : (a : ↥H) → K)) ⊥
i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hi : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) i = Weight.toLinear K (↥H) L χ
j : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hj : (S.root : (a : ↥LieSubalgebra.root) → Dual K ↥H) j = Weight.toLinear K (↥H) L α
h_pairing_zero : S.pairing i j = 0
h_pos_zero : ⁅x_χ, m_pos⁆ = 0
h_neg_zero : ⁅x_χ, m_neg⁆ = 0
h_bracket_zero : ⁅x_χ, (↑y : L)⁆ = 0
⊢ Membership.mem (γ := LieSubmodule K (↥H) L)
    (⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯)
    (HAdd.hAdd (α := L) 0 0 + 0)

Tactic:
simp only [add_zero, zero_mem]

Premises used: ZeroMemClass.zero_mem, add_zero
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (χ : Weight K (↥H) L), genWeightSpace L (⇑χ : (a : ↥H) → K)) x

Tactic:
simp [LieModule.iSup_genWeightSpace_eq_top']

Premises used: LieModule.iSup_genWeightSpace_eq_top'
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
⊢ Membership.mem (γ := LieSubmodule K (↥H) L) (⨆ (χ : Weight K (↥H) L), genWeightSpace L (⇑χ : (a : ↥H) → K)) x

Tactic:
have hx : x ∈ ⨆ χ : Weight K H L, genWeightSpace L χ := by
      simp [LieModule.iSup_genWeightSpace_eq_top']
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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_χ
α : { α : 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_α⁆

Tactic:
invtSubmoduleToLieIdeal_aux q hq χ x_χ m_α hx_χ α.1 α.2.1 α.2.2 hm_α

Premises used: Set.Mem, And.right, And.left, Subtype.val, _private.0.LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_aux, Subtype.property
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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_χ
α : { α : 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_α⁆

Tactic:
exact invtSubmoduleToLieIdeal_aux q hq χ x_χ m_α hx_χ α.1 α.2.1 α.2.2 hm_α

Premises used: And.right, And.left, Subtype.val, _private.0.LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_aux, Subtype.property
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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_χ
⊢ 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_χ, 0⁆

Tactic:
simp only [Submodule.carrier_eq_coe, lie_zero, SetLike.mem_coe, zero_mem]

Premises used: SetLike.mem_coe, lie_zero, ZeroMemClass.zero_mem, Submodule.carrier_eq_coe
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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₂⁆
mem :
  ∀
    (ih₁ :
      Membership.mem (γ := Submodule K L)
        (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
          Submodule K L)
        ⁅x_χ, m₁⁆)
    (ih₂ :
      Membership.mem (γ := Submodule K L)
        (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
          Submodule K L)
        ⁅x_χ, m₂⁆),
    Membership.mem (γ := Submodule K L)
      (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
        Submodule K L)
      (⁅x_χ, m₁⁆ + ⁅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₂⁆

Tactic:
simp only [lie_add, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢

Premises used: SetLike.mem_coe, Submodule.carrier_eq_coe, lie_add
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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 (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    ⁅x_χ, m₁⁆
ih₂ :
  Membership.mem (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    ⁅x_χ, m₂⁆
⊢ Membership.mem (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    (⁅x_χ, m₁⁆ + ⁅x_χ, m₂⁆)

Tactic:
add_mem ih₁ ih₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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 (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    ⁅x_χ, m₁⁆
ih₂ :
  Membership.mem (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    ⁅x_χ, m₂⁆
⊢ Membership.mem (γ := Submodule K L)
    (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
      Submodule K L)
    (⁅x_χ, m₁⁆ + ⁅x_χ, m₂⁆)

Tactic:
exact add_mem ih₁ ih₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
⊢ 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))))
    (Bracket.bracket (L := L) 0 m)

Tactic:
simp only [Submodule.carrier_eq_coe, zero_lie, SetLike.mem_coe, zero_mem]

Premises used: SetLike.mem_coe, zero_lie, ZeroMemClass.zero_mem, Submodule.carrier_eq_coe
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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⁆
add :
  ∀
    (ih₁ :
      Membership.mem (γ := Submodule K L)
        (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
          Submodule K L)
        ⁅x₁, m⁆)
    (ih₂ :
      Membership.mem (γ := Submodule K L)
        (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
          Submodule K L)
        ⁅x₂, m⁆),
    Membership.mem (γ := Submodule K L)
      (↑(⨆ (α : { α : Weight K (↥H) L // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯) :
        Submodule K L)
      (⁅x₁, m⁆ + ⁅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⁆

Tactic:
simp only [add_lie, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢

Premises used: SetLike.mem_coe, Submodule.carrier_eq_coe, add_lie