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 : 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)
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)}))
⊢ 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:
conv_rhs => rw [RootPairing.invtRootSubmodule.eq_span_root q]

Premises used: RootPairing.invtRootSubmodule.eq_span_root
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)
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)}
⊢ 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:
congr 2
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)
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)}
        α
⊢ 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:
ext α
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)
α : ↥(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:
mem_rootSet_invtSubmoduleToLieIdeal _ _

Premises used: Set.Mem, setOf, LieIdeal.rootSet, LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)
α : ↥(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:
exact mem_rootSet_invtSubmoduleToLieIdeal _ _

Premises used: LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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

Tactic:
⟨fun h ↦ ?_, LieIdeal.toInvtRootSubmodule_mono⟩

Premises used: LieIdeal.toInvtRootSubmodule_mono, Iff.intro
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
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)) ⋯,
                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
⊢ 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

Tactic:
refine ⟨fun h ↦ ?_, LieIdeal.toInvtRootSubmodule_mono⟩
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)))
rw : invtSubmoduleToLieIdeal I.rootSpan ⋯ ≤ invtSubmoduleToLieIdeal J.rootSpan ⋯
⊢ I ≤ J

Tactic:
rw [← lieIdealOrderIso_left_inv (H := H) I, ← lieIdealOrderIso_left_inv (H := H) J]

Premises used: LieAlgebra.IsKilling.rootSystem, RootPairing.mem_invtRootSubmodule_iff, LieIdeal.rootSpan_mem_invtRootSubmodule, LieAlgebra.IsKilling.lieIdealOrderIso_left_inv, Iff.mp
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)))
⊢ invtSubmoduleToLieIdeal I.rootSpan ⋯ ≤ invtSubmoduleToLieIdeal J.rootSpan ⋯

Tactic:
invtSubmoduleToLieIdeal_mono _ _ h

Premises used: LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_mono
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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)))
⊢ invtSubmoduleToLieIdeal I.rootSpan ⋯ ≤ invtSubmoduleToLieIdeal J.rootSpan ⋯

Tactic:
exact invtSubmoduleToLieIdeal_mono _ _ h

Premises used: LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_mono
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
⊢ Nontrivial L

Tactic:
nontriviality L
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
h : Nontrivial L
⊢ ¬IsLieAbelian L

Tactic:
have hL : ¬ IsLieAbelian L :=
    (isLieAbelian_iff_subsingleton K (L := L)).not.mpr (not_subsingleton L)
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
h : Nontrivial L
hL : ¬IsLieAbelian L
rw :
  IsSimpleOrder
      ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)) ↔
    IsSimple K L
rw₁ :
  IsSimpleOrder
      ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)) ↔
    IsSimpleOrder.{u_2} (LieIdeal K L)
rw₂ rw₃ :
  IsSimpleOrder
      ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H)) ↔
    IsSimpleOrder
      ↥(RootPairing.invtRootSubmodule (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H))
⊢ RootPairing.IsIrreducible (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H) ↔ IsSimple K L

Tactic:
rw [RootPairing.isIrreducible_iff_invtRootSubmodule, ← isSimple_iff_of_not_isLieAbelian K L hL,
    (lieIdealOrderIso H).isSimpleOrder_iff]

Premises used: LieAlgebra.IsKilling.lieIdealOrderIso, OrderIso.isSimpleOrder_iff, RootPairing.isIrreducible_iff_invtRootSubmodule, LieAlgebra.isSimple_iff_of_not_isLieAbelian
-- Module: Mathlib.Algebra.Lie.Weights.IsSimple
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
H : LieSubalgebra K L
inst_5 : H.IsCartanSubalgebra
inst_6 : IsTriangularizable K (↥H) L
inst_7 : IsSimple K L
⊢ RootPairing.IsIrreducible (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (IsKilling.rootSystem H)

Tactic:
LieAlgebra.IsKilling.isSimple_iff_isIrreducible.mpr ‹_›

Premises used: Iff.mpr, LieAlgebra.IsKilling.isSimple_iff_isIrreducible
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
x : M
⊢ (r + s) • x = r • x + s • x

Tactic:
Module.add_smul r s x

Premises used: Module.add_smul
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : R
h : a + b = 1
x : M
rw : (a + b) • x = x
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x = x
rw₂ rw₃ : x = x
⊢ a • x + b • x = x

Tactic:
rw [← add_smul, h, one_smul]

Premises used: one_smul, add_smul
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
rw : HAdd.hAdd (α := R) 1 1 • x = x + x
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 x = x + x
rw₂ rw₃ : x + x = x + x
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) 2 x = x + x

Tactic:
rw [← one_add_one_eq_two, add_smul, one_smul]

Premises used: one_add_one_eq_two, one_smul, add_smul
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
x_1 : M
inst_3 : AddCommMonoid M₂
inst_4 : SMul R M₂
f : M₂ →+ M
hf : Injective.{u_4 + 1, u_3 + 1} (α := M₂) (β := M) (⇑f : (a : M₂) → M)
smul : ∀ (c : R) (x : M₂), (f : (a : M₂) → M) (c • x) = HSMul.hSMul (β := M) c ((f : (a : M₂) → M) x : M)
c₁ c₂ : R
x : M₂
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : M₂) → M) ((c₁ + c₂) • x) : M) ((f : (a : M₂) → M) (c₁ • x + c₂ • x) : M)

Tactic:
simp only [smul, f.map_add, add_smul]

Premises used: add_smul, AddMonoidHom.map_add
-- Module: Mathlib.Algebra.Module.Defs
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : R
x_1 : M
inst_3 : AddCommMonoid M₂
inst_4 : SMul R M₂
f : M₂ →+ M
hf : Injective.{u_4 + 1, u_3 + 1} (α := M₂) (β := M) (⇑f : (a : M₂) → M)
smul : ∀ (c : R) (x : M₂), (f : (a : M₂) → M) (c • x) = HSMul.hSMul (β := M) c ((f : (a : M₂) → M) x : M)
x : M₂
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : M₂) → M) (HSMul.hSMul.{u_1, u_4, u_4} (α := R) 0 x) : M) ((f : (a : M₂) → M) 0 : M)

Tactic:
simp only [smul, zero_smul, f.map_zero]

Premises used: AddMonoidHom.map_zero, zero_smul