awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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 (α := L) (LieSubmodule.restr I H) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)
have this : Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) (↑a : L) sorry)
Tactic: have : (⟨a.val, a.property⟩ : H) ∈ corootSpace α := ha
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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 (α := L) (LieSubmodule.restr I H) ((H.toLieSubmodule.incl : (a : ↥H.toLieSubmodule) → L) a : L)
have 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) sorry) : L)
Tactic: rw [mem_corootSpace] at this
Cleared hypotheses: this
-- 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 : 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)
have 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)
Tactic: refine (Submodule.span_le.mpr ?_) this
-- 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 : 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)
have rw : ⁅coroot α, y⁆ ∈ (↑I : Submodule K L)
Tactic: rw [← lie_eq_smul_of_mem_rootSpace hy (coroot α)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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 γ
⊢ y ∈ LieSubmodule.restr I H
have this : γ (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 α))
-- 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 : 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
⊢ 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 α
have 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)))
Tactic: suffices h : ∀ γ δ : H.root, δ ∈ I.rootSet → S.reflectionPerm γ δ ∈ I.rootSet by
    exact ⟨fun hα => S.reflectionPerm_self β α ▸ h β _ hα, h β α⟩
-- 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 : 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 δ
⊢ 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)))
have 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
Tactic: simp only [mem_rootSet] at hδ ⊢
Cleared hypotheses: hδ
-- 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 : 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
⊢ rootSpace H
      (⇑(↑((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) : Weight K (↥H) L) :
        (a : ↥H) → K) ≤
    LieSubmodule.restr I H
have 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
Tactic: by_cases hp : S.pairing δ γ = 0
-- 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 : 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
⊢ rootSpace H
      (⇑(↑((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) : Weight K (↥H) L) :
        (a : ↥H) → K) ≤
    LieSubmodule.restr I H
have 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
Tactic: by_cases hp : S.pairing δ γ = 0
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) : Weight K (↥H) L) :
        (a : ↥H) → K) ≤
    LieSubmodule.restr I H
have hγ : 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)
-- 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 : 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
have rwa : S.pairing δ ((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) γ) ≠ 0
Tactic: rwa [← S.pairing_reflectionPerm γ δ γ, S.pairing_reflectionPerm_self_right, neg_ne_zero]
-- 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 : 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
⊢ S.pairing ((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) γ ≠ 0
have rwa₁ : -S.pairing δ γ ≠ 0
Tactic: rwa [← S.pairing_reflectionPerm γ δ γ, S.pairing_reflectionPerm_self_right, neg_ne_zero]
-- 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 : 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
⊢ S.pairing ((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) γ ≠ 0
have rwa₂ : S.pairing δ γ ≠ 0
Tactic: rwa [← S.pairing_reflectionPerm γ δ γ, S.pairing_reflectionPerm_self_right, neg_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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
⊢ rootSpace H
      (⇑(↑((S.reflectionPerm γ : (a : ↥LieSubalgebra.root) → ↥LieSubalgebra.root) δ) : Weight K (↥H) L) :
        (a : ↥H) → K) ≤
    LieSubmodule.restr I H
have h_neg : 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]
-- 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 : 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
⊢ I.rootSpan ∈ RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)
have 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)
Tactic: rw [RootPairing.mem_invtRootSubmodule_iff]
-- 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 : 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))
⊢ I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) β) : Dual K ↥H →ₗ[K] Dual K ↥H)
have 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))
Tactic: rw [Module.End.mem_invtSubmodule, rootSpan, Submodule.span_le]
-- 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 : 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.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)
have 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)
Tactic: rw [SetLike.mem_coe, Submodule.mem_comap, LinearEquiv.coe_coe, ← RootPairing.root_reflectionPerm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) h : K) (0 : K)
have hβ₁ : ¬rootSpace H (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H
Tactic: simp only [LieIdeal.mem_rootSet] at hβ
Cleared hypotheses: hβ
-- 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 : 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
⊢ Eq.{u_1 + 1} (α := K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) h : K) (0 : K)
have 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
Tactic: contrapose! hβ
Cleared hypotheses: hβ
-- 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 : 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)
have rw : ⁅h, y⁆ ∈ (↑I : Submodule K L)
Tactic: rw [← lie_eq_smul_of_mem_rootSpace hy h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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)
⊢ y ∈ LieSubmodule.restr I H
have 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)
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
-- 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 : 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)
⊢ y ∈ LieSubmodule.restr I H
have rwa : ∀ (h_smul : y ∈ (↑I : Submodule K L)), y ∈ LieSubmodule.restr I H
Tactic: rwa [I.toSubmodule.smul_mem_iff hβ] at h_smul
Cleared hypotheses: h_smul
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := K) (((↑α : Weight K (↥H) L) : (a : ↥H) → K) (coroot (↑β : Weight K (↥H) L)) : K) (0 : K)
have h_ker : 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β