awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : Submodule K (Dual.{u_1, u_2} K ↥H)
hq :
  ∀ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    q ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) i) : Dual K ↥H →ₗ[K] Dual K ↥H)
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα :
  Membership.mem (α := Dual.{u_1, u_2} K ↥H) q
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α : Dual.{u_1, u_2} K ↥H)
⊢ Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α
have calc : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ sl2SubmoduleOfRoot sorry
Tactic: calc rootSpace H (α : Weight K H L)
        ≤ sl2SubmoduleOfRoot (H.isNonZero_coe_root α) := by
          rw [sl2SubmoduleOfRoot_eq_sup]; exact le_sup_of_le_left le_sup_left
      _ ≤ ⨆ x : {β : Weight K H L // ↑β ∈ q ∧ β.IsNonZero}, sl2SubmoduleOfRoot x.2.2 :=
          le_iSup_of_le ⟨↑α, hα, H.isNonZero_coe_root α⟩ le_rfl
      _ = J.restr H := (restr_invtSubmoduleToLieIdeal_eq_iSup q hq).symm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
⊢ Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
have rw : Membership.mem (γ := Submodule K (Dual.{u_1, u_2} K ↥H)) I.rootSpan (Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L)) ↔
  Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
Tactic: rw [mem_rootSet_invtSubmoduleToLieIdeal, rootSystem_root_apply]
-- 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 : 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
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
⊢ J = I
have h_eq : ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
  Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
Tactic: have h_eq : ∀ α : H.root, α ∈ J.rootSet ↔ α ∈ I.rootSet := fun α ↦ by
    rw [mem_rootSet_invtSubmoduleToLieIdeal, rootSystem_root_apply]
    exact ⟨I.mem_rootSet_of_mem_rootSpan, fun h ↦ Submodule.subset_span ⟨α, h, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
⊢ LieSubmodule.restr J H = LieSubmodule.restr I H
have rw : Eq.{u_2 + 1} (α := LieSubmodule K (↥H) L)
  (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α),
      sl2SubmoduleOfRoot sorry)
  (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
      sl2SubmoduleOfRoot sorry)
Tactic: rw [J.restr_eq_iSup_sl2SubmoduleOfRoot, I.restr_eq_iSup_sl2SubmoduleOfRoot]
-- 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 : 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
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
⊢ J = I
have h_restr : LieSubmodule.restr J H = LieSubmodule.restr I H
Tactic: have h_restr : J.restr H = I.restr H := by
    rw [J.restr_eq_iSup_sl2SubmoduleOfRoot, I.restr_eq_iSup_sl2SubmoduleOfRoot]
    exact le_antisymm
      (iSup₂_le fun α hα ↦ le_iSup₂_of_le α ((h_eq α).1 hα) le_rfl)
      (iSup₂_le fun α hα ↦ le_iSup₂_of_le α ((h_eq α).2 hα) le_rfl)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
h_restr : LieSubmodule.restr J H = LieSubmodule.restr I H
⊢ J = I
have rw : (↑J : Submodule K L) = (↑I : Submodule K L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, ← LieSubmodule.restr_toSubmodule J H,
    ← LieSubmodule.restr_toSubmodule I H, h_restr]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
h_restr : LieSubmodule.restr J H = LieSubmodule.restr I H
rw : (↑J : Submodule K L) = (↑I : Submodule K L)
⊢ J = I
have rw₁ : (↑(LieSubmodule.restr J H) : Submodule K L) = (↑I : Submodule K L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, ← LieSubmodule.restr_toSubmodule J H,
    ← LieSubmodule.restr_toSubmodule I H, h_restr]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
h_restr : LieSubmodule.restr J H = LieSubmodule.restr I H
rw : (↑J : Submodule K L) = (↑I : Submodule K L)
rw₁ : (↑(LieSubmodule.restr J H) : Submodule K L) = (↑I : Submodule K L)
⊢ J = I
have rw₂ : (↑(LieSubmodule.restr J H) : Submodule K L) = (↑(LieSubmodule.restr I H) : Submodule K L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, ← LieSubmodule.restr_toSubmodule J H,
    ← LieSubmodule.restr_toSubmodule I H, h_restr]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
I : LieIdeal K L
hI :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    I.rootSpan ∈ End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) J.rootSet α ↔
      Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α
h_restr : LieSubmodule.restr J H = LieSubmodule.restr I H
rw : (↑J : Submodule K L) = (↑I : Submodule K L)
rw₁ : (↑(LieSubmodule.restr J H) : Submodule K L) = (↑I : Submodule K L)
rw₂ : (↑(LieSubmodule.restr J H) : Submodule K L) = (↑(LieSubmodule.restr I H) : Submodule K L)
⊢ J = I
have rw₃ : (↑(LieSubmodule.restr I H) : Submodule K L) = (↑(LieSubmodule.restr I H) : Submodule K L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, ← LieSubmodule.restr_toSubmodule J H,
    ← LieSubmodule.restr_toSubmodule I H, h_restr]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H))
hq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    (↑q : Submodule K (Dual K ↥H)) ∈
      End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
⊢ (invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) hq).toInvtRootSubmodule = q
have simp : Submodule.span K
    (Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
      (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
      {α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤
          LieSubmodule.restr (invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) hq) H}) =
  (↑q : Submodule K (Dual K ↥H))
Tactic: simp only [Subtype.ext_iff, LieIdeal.toInvtRootSubmodule, LieIdeal.rootSpan, LieIdeal.rootSet]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H))
hq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    (↑q : Submodule K (Dual K ↥H)) ∈
      End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
| (↑q : Submodule K (Dual K ↥H))
have rw : Submodule.span K
  (Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
    (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
    {i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
      Membership.mem (α := Dual.{u_1, u_2} K ↥H) (↑q : Submodule K (Dual K ↥H))
        ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) i : Dual.{u_1, u_2} K ↥H)})
Tactic: rw [RootPairing.invtRootSubmodule.eq_span_root q]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H))
hq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    (↑q : Submodule K (Dual K ↥H)) ∈
      End.invtSubmodule (↑(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)
        {α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤
            LieSubmodule.restr (invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) hq) H}) =
    (↑q : Submodule K (Dual K ↥H))
have conv_rhs : Eq (α := 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)
      {α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤
          LieSubmodule.restr (invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) hq) H}))
  (Submodule.span K
    (Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
      (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
      {i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
        Membership.mem (α := Dual.{u_1, u_2} K ↥H) (↑q : Submodule K (Dual K ↥H))
          ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) i : Dual.{u_1, u_2} K ↥H)}))
Tactic: conv_rhs => rw [RootPairing.invtRootSubmodule.eq_span_root q]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H))
hq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    (↑q : Submodule K (Dual K ↥H)) ∈
      End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
⊢ Eq (α := 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)
        {α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤
            LieSubmodule.restr (invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) hq) H}))
    (Submodule.span K
      (Set.image (α := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
        (⇑(RootPairing.root (rootSystem H)) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        {i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
          Membership.mem (α := Dual.{u_1, u_2} K ↥H) (↑q : Submodule K (Dual K ↥H))
            ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) i : Dual.{u_1, u_2} K ↥H)}))
have e_s : Eq (α := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
  {α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
    rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤
      LieSubmodule.restr (invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) hq) H}
  {i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
    Membership.mem (α := Dual.{u_1, u_2} K ↥H) (↑q : Submodule K (Dual K ↥H))
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) i : Dual.{u_1, u_2} K ↥H)}
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
q : ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H))
hq :
  ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    (↑q : Submodule K (Dual K ↥H)) ∈
      End.invtSubmodule (↑(RootPairing.reflection (rootSystem H) α) : Dual K ↥H →ₗ[K] Dual K ↥H)
⊢ Eq (α := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
    {α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
      rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤
        LieSubmodule.restr (invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) hq) H}
    {i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
      Membership.mem (α := Dual.{u_1, u_2} K ↥H) (↑q : Submodule K (Dual K ↥H))
        ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) i : Dual.{u_1, u_2} K ↥H)}
have e_s : ∀ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
  Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
      {α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤
          LieSubmodule.restr (invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) hq) H}
      α ↔
    Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
      {i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) |
        Membership.mem (α := Dual.{u_1, u_2} K ↥H) (↑q : Submodule K (Dual K ↥H))
          ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) i : Dual.{u_1, u_2} K ↥H)}
      α
Tactic: ext α
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
I J : LieIdeal K L
⊢ LE.le (α := ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)))
      (({ toFun := LieIdeal.toInvtRootSubmodule,
              invFun :=
                fun
                  (q :
                    ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
                        (rootSystem H))) ↦
                invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : LieIdeal K L) → ↥(rootSystem H).invtRootSubmodule)
          I :
        ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)))
      (({ toFun := LieIdeal.toInvtRootSubmodule,
              invFun :=
                fun
                  (q :
                    ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
                        (rootSystem H))) ↦
                invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : LieIdeal K L) → ↥(rootSystem H).invtRootSubmodule)
          J :
        ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H))) ↔
    I ≤ J
have refine : ∀
  (h :
    LE.le (α := ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)))
      (({ toFun := LieIdeal.toInvtRootSubmodule,
              invFun :=
                fun
                  (q :
                    ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
                        (rootSystem H))) ↦
                invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) sorry,
              left_inv := sorry, right_inv := sorry } :
            (a : LieIdeal K L) → ↥(rootSystem H).invtRootSubmodule)
          I :
        ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)))
      (({ toFun := LieIdeal.toInvtRootSubmodule,
              invFun :=
                fun
                  (q :
                    ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
                        (rootSystem H))) ↦
                invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) sorry,
              left_inv := sorry, right_inv := sorry } :
            (a : LieIdeal K L) → ↥(rootSystem H).invtRootSubmodule)
          J :
        ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)))),
  I ≤ J
Tactic: refine ⟨fun h ↦ ?_, LieIdeal.toInvtRootSubmodule_mono⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.IsSimple (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : FiniteDimensional K L
inst_5 : IsKilling K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
I J : LieIdeal K L
h :
  LE.le (α := ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)))
    (({ toFun := LieIdeal.toInvtRootSubmodule,
            invFun :=
              fun
                (q :
                  ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
                      (rootSystem H))) ↦
              invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : LieIdeal K L) → ↥(rootSystem H).invtRootSubmodule)
        I :
      ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)))
    (({ toFun := LieIdeal.toInvtRootSubmodule,
            invFun :=
              fun
                (q :
                  ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
                      (rootSystem H))) ↦
              invtSubmoduleToLieIdeal (↑q : Submodule K (Dual K ↥H)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : LieIdeal K L) → ↥(rootSystem H).invtRootSubmodule)
        J :
      ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)))
⊢ I ≤ J
have rw : invtSubmoduleToLieIdeal I.rootSpan sorry ≤ invtSubmoduleToLieIdeal J.rootSpan sorry
Tactic: rw [← lieIdealOrderIso_left_inv (H := H) I, ← lieIdealOrderIso_left_inv (H := H) J]