awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
this :
  Eq.{u_4 + 1} (α := LieSubmodule K L M)
    (⨆ (x : Weight K L M),
      genWeightSpace M
        (↑((Weight.equivSetOf K L M : (a : Weight K L M) → (↑{χ : L → K | genWeightSpace M χ ≠ ⊥} : Type (max u_1 u_3)))
              x) :
          L → K))
    ⊤
⊢ Eq.{u_4 + 1} (α := LieSubmodule K L M) (⨆ (χ : Weight K L M), genWeightSpace M (⇑χ : (a : L) → K)) ⊤

Tactic:
exact this
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
⊢ N = ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)

Tactic:
le_antisymm ?_ (iSup_le fun χ ↦ inf_le_left)

Premises used: le_antisymm, iSup_le, inf_le_left
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
refine : N ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
⊢ N = ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)

Tactic:
refine le_antisymm ?_ (iSup_le fun χ ↦ inf_le_left)

Premises used: le_antisymm, iSup_le
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
rw : ⨆ (i : Weight.{u_1, u_3, u_4} K L ↥N), LieSubmodule.map N.incl (genWeightSpace ↥N (⇑i : (a : L) → K))
| N

Tactic:
rw [← N.map_incl_top, ← iSup_genWeightSpace_eq_top' K L N, LieSubmodule.map_iSup]

Premises used: LieSubmodule.map_iSup, LieModule.iSup_genWeightSpace_eq_top', LieSubmodule.map_incl_top, Membership.mem, Subtype
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
conv_lhs :
  LE.le.{u_4} (α := LieSubmodule K L M)
    (⨆ (i : Weight.{u_1, u_3, u_4} K L ↥N), LieSubmodule.map N.incl (genWeightSpace ↥N (⇑i : (a : L) → K)))
    (⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K))
⊢ N ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)

Tactic:
conv_lhs => rw [← N.map_incl_top, ← iSup_genWeightSpace_eq_top' K L N, LieSubmodule.map_iSup]

Premises used: LieSubmodule.map_iSup, LieModule.iSup_genWeightSpace_eq_top', LieSubmodule.map_incl_top, Membership.mem, Subtype
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
⊢ LE.le.{u_4} (α := LieSubmodule K L M)
    (⨆ (i : Weight.{u_1, u_3, u_4} K L ↥N), LieSubmodule.map N.incl (genWeightSpace ↥N (⇑i : (a : L) → K)))
    (⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K))

Tactic:
iSup_le fun χ_N ↦ ?_

Premises used: Set.Mem, iSup_le
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
refine :
  ∀ (χ_N : Weight.{u_1, u_3, u_4} K L ↥N),
    LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤
      ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
⊢ LE.le.{u_4} (α := LieSubmodule K L M)
    (⨆ (i : Weight.{u_1, u_3, u_4} K L ↥N), LieSubmodule.map N.incl (genWeightSpace ↥N (⇑i : (a : L) → K)))
    (⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K))

Tactic:
refine iSup_le fun χ_N ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
χ_N : Weight.{u_1, u_3, u_4} K L ↥N
⊢ LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤ N

Tactic:
have hN := (LieSubmodule.map_mono (le_top : genWeightSpace N χ_N ≤ ⊤)).trans N.map_incl_top.le
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
χ_N : Weight.{u_1, u_3, u_4} K L ↥N
hN : LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤ N
pos :
  ∀ (h : Eq (α := LieSubmodule K L M) (genWeightSpace M (⇑χ_N : (a : L) → K)) ⊥),
    N ⊓ genWeightSpace M (⇑χ_N : (a : L) → K) ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
neg :
  ∀ (h : ¬Eq (α := LieSubmodule K L M) (genWeightSpace M (⇑χ_N : (a : L) → K)) ⊥),
    N ⊓ genWeightSpace M (⇑χ_N : (a : L) → K) ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)
⊢ N ⊓ genWeightSpace M (⇑χ_N : (a : L) → K) ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)

Tactic:
by_cases h : genWeightSpace M (χ_N : L → K) = ⊥

Premises used: LieModule.genWeightSpace, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
χ_N : Weight.{u_1, u_3, u_4} K L ↥N
hN : LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤ N
h : Eq (α := LieSubmodule K L M) (genWeightSpace M (⇑χ_N : (a : L) → K)) ⊥
⊢ N ⊓ genWeightSpace M (⇑χ_N : (a : L) → K) ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
χ_N : Weight.{u_1, u_3, u_4} K L ↥N
hN : LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤ N
h : ¬Eq (α := LieSubmodule K L M) (genWeightSpace M (⇑χ_N : (a : L) → K)) ⊥
⊢ N ⊓ genWeightSpace M (⇑χ_N : (a : L) → K) ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)

Tactic:
le_iSup_of_le ⟨_, h⟩ le_rfl

Premises used: le_rfl, Set.Mem, LieModule.Weight.mk, le_iSup_of_le
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
χ_N : Weight.{u_1, u_3, u_4} K L ↥N
hN : LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤ N
h : ¬Eq (α := LieSubmodule K L M) (genWeightSpace M (⇑χ_N : (a : L) → K)) ⊥
⊢ N ⊓ genWeightSpace M (⇑χ_N : (a : L) → K) ≤ ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)

Tactic:
exact le_iSup_of_le ⟨_, h⟩ le_rfl

Premises used: le_rfl, le_iSup_of_le
-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
K : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field K
inst_5 : LieAlgebra K L
inst_6 : Module K M
inst_7 : LieModule K L M
inst_8 : FiniteDimensional K M
inst_9 : IsTriangularizable K L M
N : LieSubmodule K L M
χ_N : Weight.{u_1, u_3, u_4} K L ↥N
hN : LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤ N
⊢ LieSubmodule.map N.incl (genWeightSpace ↥N (⇑χ_N : (a : L) → K)) ≤
    ⨆ (χ : Weight K L M), N ⊓ genWeightSpace M (⇑χ : (a : L) → K)

Tactic:
exact (le_inf hN (map_genWeightSpace_le _)).trans <| by
    by_cases h : genWeightSpace M (χ_N : L → K) = ⊥
    · simp [h]
    · exact le_iSup_of_le ⟨_, h⟩ le_rfl

Premises used: LieModule.map_genWeightSpace_le, le_inf, LE.le.trans
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
x : L
hx : x ∈ corootSubmodule α
obtain :
  ∀ (a : ↥H.toLieSubmodule)
    (ha : Membership.mem (γ := LieSubmodule K ↥H ↥H.toLieSubmodule) (corootSpace (⇑α : (a : ↥H) → K)) a)
    (hx : Membership.mem (α := L) (corootSubmodule α) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)),
    Membership.mem (α := L) (LieSubmodule.restr I H) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)
⊢ x ∈ LieSubmodule.restr I H

Tactic:
obtain ⟨a, ha, rfl⟩ := (LieSubmodule.mem_map _).mp hx

Premises used: Iff.mp, rfl, LieSubmodule.mem_map
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
a : ↥H.toLieSubmodule
ha : Membership.mem (γ := LieSubmodule K ↥H ↥H.toLieSubmodule) (corootSpace (⇑α : (a : ↥H) → K)) a
hx : Membership.mem (α := L) (corootSubmodule α) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)
⊢ Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) (↑a : L) ⋯)

Tactic:
have : (⟨a.val, a.property⟩ : H) ∈ corootSpace α := ha
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
a : ↥H.toLieSubmodule
ha : Membership.mem (γ := LieSubmodule K ↥H ↥H.toLieSubmodule) (corootSpace (⇑α : (a : ↥H) → K)) a
hx : Membership.mem (α := L) (corootSubmodule α) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)
this :
  Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) (↑a : L) ⋯)
⊢ Membership.mem (γ := Submodule K L)
    (Submodule.span K
      {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x})
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ H) (↑a : L) ⋯) : L)

Tactic:
rw [mem_corootSpace] at this

Premises used: LieAlgebra.mem_corootSpace
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
a : ↥H.toLieSubmodule
ha : Membership.mem (γ := LieSubmodule K ↥H ↥H.toLieSubmodule) (corootSpace (⇑α : (a : ↥H) → K)) a
hx : Membership.mem (α := L) (corootSubmodule α) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)
this :
  Membership.mem (γ := Submodule K L)
    (Submodule.span K
      {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x})
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ H) (↑a : L) ⋯) : L)
⊢ Membership.mem (α := L) (LieSubmodule.restr I H) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)

Tactic:
(Submodule.span_le.mpr ?_) this

Premises used: Iff.mpr, Set.Mem, Submodule.span_le
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
a : ↥H.toLieSubmodule
ha : Membership.mem (γ := LieSubmodule K ↥H ↥H.toLieSubmodule) (corootSpace (⇑α : (a : ↥H) → K)) a
hx : Membership.mem (α := L) (corootSubmodule α) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)
this :
  Membership.mem (γ := Submodule K L)
    (Submodule.span K
      {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x})
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ H) (↑a : L) ⋯) : L)
refine :
  {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x} ⊆
    (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
⊢ Membership.mem (α := L) (LieSubmodule.restr I H) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)

Tactic:
refine (Submodule.span_le.mpr ?_) this

Premises used: Iff.mpr, Submodule.span_le
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
a : ↥H.toLieSubmodule
ha : Membership.mem (γ := LieSubmodule K ↥H ↥H.toLieSubmodule) (corootSpace (⇑α : (a : ↥H) → K)) a
hx : Membership.mem (α := L) (corootSubmodule α) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)
this :
  Membership.mem (γ := Submodule K L)
    (Submodule.span K
      {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x})
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ H) (↑a : L) ⋯) : L)
y : L
hy : y ∈ rootSpace H (⇑α : (a : ↥H) → K)
w : L
⊢ ⁅y, w⁆ ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)

Tactic:
lie_mem_left K L I y _ (hα hy)

Premises used: Set.Mem, lie_mem_left
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
a : ↥H.toLieSubmodule
ha : Membership.mem (γ := LieSubmodule K ↥H ↥H.toLieSubmodule) (corootSpace (⇑α : (a : ↥H) → K)) a
hx : Membership.mem (α := L) (corootSubmodule α) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)
this :
  Membership.mem (γ := Submodule K L)
    (Submodule.span K
      {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x})
    (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ H) (↑a : L) ⋯) : L)
y : L
hy : y ∈ rootSpace H (⇑α : (a : ↥H) → K)
w : L
⊢ ⁅y, w⁆ ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)

Tactic:
exact lie_mem_left K L I y _ (hα hy)

Premises used: lie_mem_left
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
I : LieIdeal K L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
⊢ Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α ↔
    rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, LieIdeal.rootSet
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
y : L
hy : y ∈ rootSpace H γ
rw : ⁅coroot α, y⁆ ∈ (↑I : Submodule K L)
⊢ γ (coroot α) • y ∈ (↑I : Submodule K L)

Tactic:
rw [← lie_eq_smul_of_mem_rootSpace hy (coroot α)]

Premises used: LieAlgebra.IsKilling.coroot, LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
y : L
hy : y ∈ rootSpace H γ
⊢ ⁅coroot α, y⁆ ∈ (↑I : Submodule K L)

Tactic:
lie_mem_left K L I _ y
      (I.corootSubmodule_le hα (coe_coroot_mem_corootSubmodule α))

Premises used: Set.Mem, LieIdeal.corootSubmodule_le, lie_mem_left, LieAlgebra.IsKilling.coe_coroot_mem_corootSubmodule
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
y : L
hy : y ∈ rootSpace H γ
⊢ ⁅coroot α, y⁆ ∈ (↑I : Submodule K L)

Tactic:
exact lie_mem_left K L I _ y
      (I.corootSubmodule_le hα (coe_coroot_mem_corootSubmodule α))

Premises used: LieIdeal.corootSubmodule_le, lie_mem_left, LieAlgebra.IsKilling.coe_coroot_mem_corootSubmodule
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
y : L
hy : y ∈ rootSpace H γ
⊢ γ (coroot α) • y ∈ (↑I : Submodule K L)

Tactic:
have : γ (coroot α) • y ∈ I.toSubmodule := by
    rw [← lie_eq_smul_of_mem_rootSpace hy (coroot α)]
    exact lie_mem_left K L I _ y
      (I.corootSubmodule_le hα (coe_coroot_mem_corootSubmodule α))
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
y : L
hy : y ∈ rootSpace H γ
this : γ (coroot α) • y ∈ (↑I : Submodule K L)
⊢ y ∈ LieSubmodule.restr I H

Tactic:
I.toSubmodule.smul_mem_iff hγ_ne |>.mp this

Premises used: Set.Mem, LieSubmodule.toSubmodule, Submodule.smul_mem_iff, Iff.mp
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
y : L
hy : y ∈ rootSpace H γ
this : γ (coroot α) • y ∈ (↑I : Submodule K L)
⊢ y ∈ LieSubmodule.restr I H

Tactic:
exact I.toSubmodule.smul_mem_iff hγ_ne |>.mp this

Premises used: LieSubmodule.toSubmodule, Submodule.smul_mem_iff, Iff.mp
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
h :
  ∀ (γ δ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet δ →
      Membership.mem (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (γ :=
        Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet
        ((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ :
          ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
⊢ Membership.mem (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (γ :=
      Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet
      ((RootPairing.reflectionPerm (rootSystem H) β : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) α :
        ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↔
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α

Tactic:
⟨fun hα => S.reflectionPerm_self β α ▸ h β _ hα, h β α⟩

Premises used: RootPairing.reflectionPerm_self, Eq.rec, Iff.intro, RootPairing.reflectionPerm, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
α β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
S : RootPairing (↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) K (Dual.{u_1, u_2} K ↥H) ↥H := rootSystem H
h :
  ∀ (γ δ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet δ →
      Membership.mem (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (γ :=
        Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet
        ((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ :
          ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
⊢ Membership.mem (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (γ :=
      Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet
      ((RootPairing.reflectionPerm (rootSystem H) β : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) α :
        ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↔
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α

Tactic:
exact ⟨fun hα => S.reflectionPerm_self β α ▸ h β _ hα, h β α⟩