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))
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))
rw :
  Eq.{u_1 + 1} (α := K)
    ((LinearMap.BilinForm.toLinHomAux₁ (traceForm K (↥H) L) (coroot (↑α : Weight K (↥H) L)) : (a : ↥H) → K)
        (coroot (↑β : Weight K (↥H) L)) :
      K)
    (0 : K)
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := (↑α : Weight K (↥H) L)))
    (coroot (↑β : Weight K (↥H) L))

Tactic:
rw [← orthogonal_span_coroot_eq_ker,
    LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker, LinearMap.mem_ker]

Premises used: LinearMap.mem_ker, LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker
-- 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))
⊢ Eq.{u_1 + 1} (α := K)
    ((LinearMap.BilinForm.toLinHomAux₁ (traceForm K (↥H) L) (coroot (↑α : Weight K (↥H) L)) : (a : ↥H) → K)
        (coroot (↑β : Weight K (↥H) L)) :
      K)
    (0 : K)

Tactic:
traceForm_eq_zero_of_mem_ker_of_mem_span_coroot h_ker (Submodule.mem_span_singleton_self _)

Premises used: Submodule.mem_span_singleton_self, LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot
-- 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))
⊢ Eq.{u_1 + 1} (α := K)
    ((LinearMap.BilinForm.toLinHomAux₁ (traceForm K (↥H) L) (coroot (↑α : Weight K (↥H) L)) : (a : ↥H) → K)
        (coroot (↑β : Weight K (↥H) L)) :
      K)
    (0 : K)

Tactic:
exact traceForm_eq_zero_of_mem_ker_of_mem_span_coroot h_ker (Submodule.mem_span_singleton_self _)

Premises used: Submodule.mem_span_singleton_self, LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot
-- 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
⊢ LieSubmodule.restr I H ⊓ H.toLieSubmodule =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)

Tactic:
le_antisymm ?_ (iSup₂_le fun _ hα ↦
    le_inf (I.corootSubmodule_le hα) LieSubmodule.map_incl_le)

Premises used: iSup₂_le, le_inf, LieSubmodule.map_incl_le, le_antisymm, LieIdeal.corootSubmodule_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
refine :
  LieSubmodule.restr I H ⊓ H.toLieSubmodule ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)
⊢ LieSubmodule.restr I H ⊓ H.toLieSubmodule =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)

Tactic:
refine le_antisymm ?_ (iSup₂_le fun _ hα ↦
    le_inf (I.corootSubmodule_le hα) LieSubmodule.map_incl_le)

Premises used: iSup₂_le, le_inf, LieSubmodule.map_incl_le, le_antisymm, LieIdeal.corootSubmodule_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
x : L
this :
  ∀ (hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L))
    (hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)),
    Membership.mem (γ := LieSubmodule K (↥H) L)
      (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
          corootSubmodule (↑α : Weight K (↥H) L))
      x
⊢ x ∈ LieSubmodule.restr I H ⊓ H.toLieSubmodule →
    Membership.mem (γ := LieSubmodule K (↥H) L)
      (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
          corootSubmodule (↑α : Weight K (↥H) L))
      x

Tactic:
⟨hxI, hxH⟩
-- 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
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
⊢ span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α

Tactic:
have h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α :=
    (iSup_split f (· ∈ I.rootSet)).symm
-- 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
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
rw :
  LE.le.{u_2} (α := LieIdeal K ↥H) (⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), corootSpace (⇑α : (a : ↥H) → K))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α)
⊢ span_I_roots ⊔ span_compl_roots = ⊤

Tactic:
rw [h_split, eq_top_iff, ← biSup_corootSpace_eq_top]

Premises used: eq_top_iff, LieAlgebra.IsKilling.biSup_corootSpace_eq_top
-- 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
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α

Tactic:
simpa [LieSubalgebra.root] using hα

Premises used: LieSubalgebra.root
-- 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
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
⊢ LE.le.{u_2} (α := LieIdeal K ↥H) (⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), corootSpace (⇑α : (a : ↥H) → K))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α)

Tactic:
exact iSup₂_le fun α hα ↦ le_iSup_of_le ⟨α, by simpa [LieSubalgebra.root] using hα⟩ le_rfl

Premises used: iSup₂_le, le_iSup_of_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
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
⊢ span_I_roots ⊔ span_compl_roots = ⊤

Tactic:
have h_top : span_I_roots ⊔ span_compl_roots = ⊤ := by
    rw [h_split, eq_top_iff, ← biSup_corootSpace_eq_top]
    exact iSup₂_le fun α hα ↦ le_iSup_of_le ⟨α, by simpa [LieSubalgebra.root] using hα⟩ le_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
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
change :
  LieSubmodule.map H.toLieSubmodule.incl
      (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α) =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)
⊢ LieSubmodule.map H.toLieSubmodule.incl span_I_roots =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)

Tactic:
change LieSubmodule.map _ (⨆ α ∈ I.rootSet, f α) = ⨆ α ∈ I.rootSet, _

Premises used: LieSubmodule.map, iSup, 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
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
simp_rw :
  Eq.{u_2 + 1} (α := LieSubmodule K (↥H) L)
    (⨆ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet i),
        LieSubmodule.map H.toLieSubmodule.incl (f i))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L))
⊢ LieSubmodule.map H.toLieSubmodule.incl
      (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α) =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)

Tactic:
simp_rw [LieSubmodule.map_iSup]

Premises used: LieSubmodule.map_iSup
-- 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
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
⊢ Eq.{u_2 + 1} (α := LieSubmodule K (↥H) L)
    (⨆ (i : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet i),
        LieSubmodule.map H.toLieSubmodule.incl (f i))
    (⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L))

Tactic:
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
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
⊢ LieSubmodule.map H.toLieSubmodule.incl span_I_roots =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)

Tactic:
have hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots =
      ⨆ α ∈ I.rootSet, corootSubmodule α.1 := by
    change LieSubmodule.map _ (⨆ α ∈ I.rootSet, f α) = ⨆ α ∈ I.rootSet, _
    simp_rw [LieSubmodule.map_iSup]; 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
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl :
  LieSubmodule.map H.toLieSubmodule.incl span_I_roots =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)
μ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hμ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet μ
simp_rw :
  Eq.{u_2 + 1} (α := Submodule K ↥H)
    (↑(⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β) : Submodule K ↥H)
    (⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), (↑(f β) : Submodule K ↥H))
⊢ (↑span_compl_roots : Submodule K ↥H) =
    ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), (↑(f β) : Submodule K ↥H)

Tactic:
simp_rw [span_compl_roots, LieSubmodule.iSup_toSubmodule]

Premises used: LieSubmodule.iSup_toSubmodule
-- 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
x : L
hxI : x ∈ (↑(↑(LieSubmodule.restr I H) : Submodule K L) : Set L)
hxH : x ∈ (↑(↑H.toLieSubmodule : Submodule K L) : Set L)
f : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) → LieIdeal K ↥H :=
  fun (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ corootSpace (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
span_I_roots : LieIdeal K ↥H :=
  ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
    ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α), f α
span_compl_roots : LieIdeal K ↥H := ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl :
  LieSubmodule.map H.toLieSubmodule.incl span_I_roots =
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet α),
        corootSubmodule (↑α : Weight K (↥H) L)
μ : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
hμ : Membership.mem (γ := Set ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) I.rootSet μ
⊢ (↑span_compl_roots : Submodule K ↥H) =
    ⨆ (β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))), ⨆ (_ : β ∉ I.rootSet), (↑(f β) : Submodule K ↥H)

Tactic:
have : span_compl_roots.toSubmodule = ⨆ β ∉ I.rootSet, (f β).toSubmodule := by
      simp_rw [span_compl_roots, LieSubmodule.iSup_toSubmodule]