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 : 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
suffices :
  ∀ (γ δ : ↥(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:
suffices h : ∀ γ δ : H.root, δ ∈ I.rootSet → S.reflectionPerm γ δ ∈ I.rootSet by
    exact ⟨fun hα => S.reflectionPerm_self β α ▸ h β _ hα, h β α⟩
-- 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
γ δ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hδ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet δ
simp :
  ∀ (hδ : rootSpace H (⇑(↑δ : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
    rootSpace H
        (⇑(↑((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) : Weight K (↥H) L) :
          (a : ↥H) → K) ≤
      LieSubmodule.restr I H
⊢ 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)))

Tactic:
simp only [mem_rootSet] at hδ ⊢

Premises used: LieIdeal.mem_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
α β : ↥(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
γ δ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hδ : rootSpace H (⇑(↑δ : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
pos :
  ∀ (hp : S.pairing δ γ = 0),
    rootSpace H
        (⇑(↑((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) : Weight K (↥H) L) :
          (a : ↥H) → K) ≤
      LieSubmodule.restr I H
neg :
  ∀ (hp : ¬S.pairing δ γ = 0),
    rootSpace H
        (⇑(↑((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) : Weight K (↥H) L) :
          (a : ↥H) → K) ≤
      LieSubmodule.restr I H
⊢ rootSpace H
      (⇑(↑((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) : Weight K (↥H) L) :
        (a : ↥H) → K) ≤
    LieSubmodule.restr I H

Tactic:
by_cases hp : S.pairing δ γ = 0

Premises used: RootPairing.pairing
-- 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
γ δ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hδ : rootSpace H (⇑(↑δ : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
hp : S.pairing δ γ = 0
pos pos₁ pos₂ pos₃ : rootSpace H (⇑(↑δ : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
⊢ rootSpace H
      (⇑(↑((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) : Weight K (↥H) L) :
        (a : ↥H) → K) ≤
    LieSubmodule.restr I H

Tactic:
rwa [S.reflectionPerm_eq_of_pairing_eq_zero hp]

Premises used: RootPairing.reflectionPerm_eq_of_pairing_eq_zero
-- 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
γ δ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hδ : rootSpace H (⇑(↑δ : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
⊢ rootSpace H (⇑(S.root' γ) : (a : ↥H) → K) ≤ LieSubmodule.restr I H

Tactic:
have hγ := I.rootSpace_le_of_apply_coroot_ne_zero hδ
      (mt S.pairing_eq_zero_iff.mpr hp)
-- 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
γ δ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hδ : rootSpace H (⇑(↑δ : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
hγ : rootSpace H (⇑(S.root' γ) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
rwa : S.pairing δ ((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) γ) ≠ 0
rwa₁ : -S.pairing δ γ ≠ 0
rwa₂ rwa₃ rwa₄ rwa₅ : S.pairing δ γ ≠ 0
⊢ S.pairing ((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) γ ≠ 0

Tactic:
rwa [← S.pairing_reflectionPerm γ δ γ, S.pairing_reflectionPerm_self_right, neg_ne_zero]

Premises used: RootPairing.pairing_reflectionPerm_self_right, neg_ne_zero, RootPairing.pairing_reflectionPerm
-- 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
γ δ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hδ : rootSpace H (⇑(↑δ : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
hγ : rootSpace H (⇑(S.root' γ) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
⊢ S.pairing ((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) γ ≠ 0

Tactic:
have h_neg : S.pairing (S.reflectionPerm γ δ) γ ≠ 0 := by
      rwa [← S.pairing_reflectionPerm γ δ γ, S.pairing_reflectionPerm_self_right, neg_ne_zero]
-- 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
γ δ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hδ : rootSpace H (⇑(↑δ : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
hγ : rootSpace H (⇑(S.root' γ) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
h_neg : S.pairing ((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) γ ≠ 0
⊢ rootSpace H
      (⇑(↑((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) : Weight K (↥H) L) :
        (a : ↥H) → K) ≤
    LieSubmodule.restr I H

Tactic:
I.rootSpace_le_of_apply_coroot_ne_zero hγ h_neg

Premises used: LieIdeal.rootSpace_le_of_apply_coroot_ne_zero
-- 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
γ δ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hδ : rootSpace H (⇑(↑δ : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
hγ : rootSpace H (⇑(S.root' γ) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
h_neg : S.pairing ((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) γ ≠ 0
⊢ rootSpace H
      (⇑(↑((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) : Weight K (↥H) L) :
        (a : ↥H) → K) ≤
    LieSubmodule.restr I H

Tactic:
exact I.rootSpace_le_of_apply_coroot_ne_zero hγ h_neg

Premises used: LieIdeal.rootSpace_le_of_apply_coroot_ne_zero
-- 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
rw :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
⊢ I.rootSpan ∈ RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)

Tactic:
rw [RootPairing.mem_invtRootSubmodule_iff]

Premises used: RootPairing.mem_invtRootSubmodule_iff
-- 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))
rw :
  Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
      (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H) I.rootSet ⊆
    (↑(Submodule.comap (↑(RootPairing.reflection (rootSystem H) β) : Dual K ↥H →ₗ[K] Dual K ↥H)
          (Submodule.span K
            (Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
              (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H) I.rootSet))) :
      Set (Dual K ↥H))
⊢ I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) β) : Dual K ↥H →ₗ[K] Dual K ↥H)

Tactic:
rw [Module.End.mem_invtSubmodule, rootSpan, Submodule.span_le]

Premises used: Module.End.mem_invtSubmodule, LieIdeal.rootSpan, 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
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))
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
rw :
  Membership.mem (α := Dual.{u_1, u_2} K ↥H) (γ := Submodule K (Dual.{u_1, u_2} K ↥H))
    (Submodule.span K
      (Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
        (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H) I.rootSet))
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        ((RootPairing.reflectionPerm (rootSystem H) β : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) α) :
      Dual.{u_1, u_2} K ↥H)
⊢ Membership.mem (α := Dual.{u_1, u_2} K ↥H)
    (↑(Submodule.comap (↑(RootPairing.reflection (rootSystem H) β) : Dual K ↥H →ₗ[K] Dual K ↥H)
          (Submodule.span K
            (Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
              (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H) I.rootSet))) :
      Set (Dual K ↥H))
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H)

Tactic:
rw [SetLike.mem_coe, Submodule.mem_comap, LinearEquiv.coe_coe, ← RootPairing.root_reflectionPerm]

Premises used: Submodule.mem_comap, SetLike.mem_coe, LinearEquiv.coe_coe, RootPairing.root_reflectionPerm
-- 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))
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
⊢ Membership.mem (α := Dual.{u_1, u_2} K ↥H) (γ := Submodule K (Dual.{u_1, u_2} K ↥H))
    (Submodule.span K
      (Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
        (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H) I.rootSet))
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        ((RootPairing.reflectionPerm (rootSystem H) β : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) α) :
      Dual.{u_1, u_2} K ↥H)

Tactic:
Submodule.subset_span ⟨_, (I.reflectionPerm_mem_rootSet_iff α β).mpr hα, rfl⟩

Premises used: Iff.mpr, LieIdeal.reflectionPerm_mem_rootSet_iff, Set.Mem, setOf, And.intro, Exists.intro, Submodule.subset_span, rfl
-- 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))
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hα : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
⊢ Membership.mem (α := Dual.{u_1, u_2} K ↥H) (γ := Submodule K (Dual.{u_1, u_2} K ↥H))
    (Submodule.span K
      (Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
        (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H) I.rootSet))
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        ((RootPairing.reflectionPerm (rootSystem H) β : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) α) :
      Dual.{u_1, u_2} K ↥H)

Tactic:
exact Submodule.subset_span ⟨_, (I.reflectionPerm_mem_rootSet_iff α β).mpr hα, rfl⟩
-- 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 J : LieIdeal K L
h : I ≤ J
⊢ LE.le (α := ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)))
    I.toInvtRootSubmodule J.toInvtRootSubmodule

Tactic:
Submodule.span_mono (Set.image_mono
    fun α (hα : rootSpace H α.1 ≤ I.restr H) ↦ hα.trans (show I.restr H ≤ J.restr H from h))

Premises used: Set.Mem, Set.image_mono, setOf, Submodule.span_mono, 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
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
h : ↥H
hI : (↑h : L) ∈ I
β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hβ : β ∉ I.rootSet
⊢ ¬rootSpace H (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H

Tactic:
simp only [LieIdeal.mem_rootSet] at hβ

Premises used: LieIdeal.mem_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
h : ↥H
hI : (↑h : L) ∈ I
β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hβ : ¬rootSpace H (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
contrapose! :
  ∀ (hβ : Ne.{u_1 + 1} (α := K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) h : K) (0 : K)),
    rootSpace H (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
⊢ Eq.{u_1 + 1} (α := K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) h : K) (0 : K)

Tactic:
contrapose! hβ
-- 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
h : ↥H
hI : (↑h : L) ∈ I
β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hβ : Ne.{u_1 + 1} (α := K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) h : K) (0 : K)
y : L
hy : y ∈ rootSpace H (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K)
rw : ⁅h, y⁆ ∈ (↑I : Submodule K L)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) h : K) y ∈ (↑I : Submodule K L)

Tactic:
rw [← lie_eq_smul_of_mem_rootSpace hy h]

Premises used: 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
h : ↥H
hI : (↑h : L) ∈ I
β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hβ : Ne.{u_1 + 1} (α := K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) h : K) (0 : K)
y : L
hy : y ∈ rootSpace H (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K)
⊢ ⁅h, y⁆ ∈ (↑I : Submodule K L)

Tactic:
lie_mem_left K L I h y hI

Premises used: Set.Mem, Subtype.val, 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
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
h : ↥H
hI : (↑h : L) ∈ I
β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hβ : Ne.{u_1 + 1} (α := K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) h : K) (0 : K)
y : L
hy : y ∈ rootSpace H (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K)
⊢ ⁅h, y⁆ ∈ (↑I : Submodule K L)

Tactic:
exact lie_mem_left K L I h y hI

Premises used: Subtype.val, 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
inst_5 : CharZero K
inst_6 : IsKilling K L
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
h : ↥H
hI : (↑h : L) ∈ I
β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hβ : Ne.{u_1 + 1} (α := K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) h : K) (0 : K)
y : L
hy : y ∈ rootSpace H (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) h : K) y ∈ (↑I : Submodule K L)

Tactic:
have h_smul : (β : Weight K H L) h • y ∈ I.toSubmodule := by
    rw [← lie_eq_smul_of_mem_rootSpace hy h]
    exact lie_mem_left K L I h y hI
-- 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
h : ↥H
hI : (↑h : L) ∈ I
β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hβ : Ne.{u_1 + 1} (α := K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) h : K) (0 : K)
y : L
hy : y ∈ rootSpace H (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K)
h_smul : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) h : K) y ∈ (↑I : Submodule K L)
rwa rwa₁ rwa₂ rwa₃ : ∀ (h_smul : y ∈ (↑I : Submodule K L)), y ∈ LieSubmodule.restr I H
⊢ y ∈ LieSubmodule.restr I H

Tactic:
rwa [I.toSubmodule.smul_mem_iff hβ] at h_smul

Premises used: LieSubmodule.toSubmodule, Submodule.smul_mem_iff
-- 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))
hα : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hβ : β ∉ I.rootSet
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := (↑β : Weight K (↥H) L)))
    (coroot (↑α : Weight K (↥H) L))

Tactic:
have h_ker : coroot (α : Weight K H L) ∈ (β : Weight K H L).ker :=
    I.root_apply_eq_zero_of_notMem_rootSet
      (I.corootSubmodule_le hα (coe_coroot_mem_corootSubmodule _)) hβ
-- 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))
hα : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hβ : β ∉ I.rootSet
h_ker :
  Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := (↑β : Weight K (↥H) L)))
    (coroot (↑α : Weight K (↥H) L))
change :
  Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := (↑α : Weight K (↥H) L)))
    (coroot (↑β : Weight K (↥H) L))
⊢ Eq.{u_1 + 1} (α := K) (((↑α : Weight K (↥H) L) : (a : ↥H) → K) (coroot (↑β : Weight K (↥H) L)) : K) (0 : K)

Tactic:
change coroot (β : Weight K H L) ∈ (α : Weight K H L).ker

Premises used: LieAlgebra.IsKilling.coroot, LieModule.Weight.ker, Subtype.val