awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
hI : IsLieAbelian.{u_2} ↥⊤
⊢ IsLieAbelian L

Tactic:
rw [lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv] at hI

Premises used: LieIdeal.topEquiv, lie_abelian_iff_equiv_lie_abelian
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
hI : IsLieAbelian L
⊢ False

Tactic:
IsSimple.non_abelian R (L := L) hI

Premises used: LieAlgebra.IsSimple.non_abelian
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
hI : IsLieAbelian L
⊢ False

Tactic:
exact IsSimple.non_abelian R (L := L) hI

Premises used: LieAlgebra.IsSimple.non_abelian
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
hL : ¬IsLieAbelian L
⊢ IsSimpleOrder.{u_2} (LieIdeal R L) ↔ IsSimple R L

Tactic:
⟨fun _ ↦ ⟨IsSimpleOrder.eq_bot_or_eq_top, hL⟩, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, LieAlgebra.IsSimple.mk, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Subsingleton L
⊢ ¬IsSimple R L

Tactic:
fun contra ↦ contra.non_abelian inferInstance

Premises used: inferInstance, Not, LieAlgebra.IsSimple.non_abelian
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
nth_rewrite : Membership.mem (γ := LieIdeal R L) (sSup {I} ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) x
⊢ x ∈ I ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})

Tactic:
nth_rewrite 1 [← sSup_singleton (a := I)]

Premises used: sSup_singleton
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
rw : Membership.mem (γ := LieIdeal R L) ⊤ x
rw₁ : Subset (α := Set (LieIdeal R L)) {I} {I' : LieIdeal R L | IsAtom I'}
⊢ Membership.mem (γ := LieIdeal R L) (sSup {I} ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) x

Tactic:
rw [← sSup_union, Set.union_diff_self, Set.union_eq_self_of_subset_left,
            IsSemisimple.sSup_atoms_eq_top]

Premises used: sSup_union, LieAlgebra.IsSemisimple.sSup_atoms_eq_top, Set.union_eq_self_of_subset_left, Set.union_diff_self
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
⊢ Membership.mem (γ := LieIdeal R L) ⊤ x

Tactic:
apply LieSubmodule.mem_top

Premises used: LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
⊢ Subset (α := Set (LieIdeal R L)) {I} {I' : LieIdeal R L | IsAtom I'}

Tactic:
simp only [Set.singleton_subset_iff, Set.mem_setOf_eq, hI]

Premises used: Set.singleton_subset_iff, Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
⊢ x ∈ I ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})

Tactic:
have hx : x ∈ I ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I}) := by
          nth_rewrite 1 [← sSup_singleton (a := I)]
          rw [← sSup_union, Set.union_diff_self, Set.union_eq_self_of_subset_left,
            IsSemisimple.sSup_atoms_eq_top]
          · apply LieSubmodule.mem_top
          · simp only [Set.singleton_subset_iff, Set.mem_setOf_eq, hI]
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
hx : x ∈ I ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})
⊢ ∃ y ∈ I,
    ∃ (z : L), Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) z ∧ y + z = x

Tactic:
rw [LieSubmodule.mem_sup] at hx

Premises used: LieSubmodule.mem_sup
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
hx :
  ∃ y ∈ I,
    ∃ (z : L), Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) z ∧ y + z = x
obtain :
  ∀ (a : L) (ha : a ∈ I) (b : L)
    (hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b),
    Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)).carrier
      (⁅a + b, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
⊢ Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)).carrier
    (⁅x, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)

Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
simp :
  HAdd.hAdd (α := L) (β := L) (⁅a, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
      (⁅b, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L) ∈
    Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)
⊢ Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)).carrier
    (⁅a + b, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)

Tactic:
simp only [Submodule.carrier_eq_coe, add_lie, SetLike.mem_coe]

Premises used: SetLike.mem_coe, Submodule.carrier_eq_coe, add_lie
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
a₁ :
  Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I))
    (⁅a, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
a₂ :
  Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I))
    (⁅b, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
⊢ HAdd.hAdd (α := L) (β := L) (⁅a, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
      (⁅b, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L) ∈
    Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)

Tactic:
apply add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
a₁ :
  ∃ (a_1 : L) (b : a_1 ∈ I),
    Subtype.mk (p := fun (a : L) ↦ a ∈ I) a_1 b ∈ J ∧
      Eq (α := L) (((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (a : L) ↦ a ∈ I) a_1 b) : L)
        (⁅a, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
⊢ Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I))
    (⁅a, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)

Tactic:
simp only [Submodule.mem_map, LieSubmodule.mem_toSubmodule, Subtype.exists]

Premises used: LieSubmodule.mem_toSubmodule, Submodule.mem_map, Subtype.exists
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
a₁ :
  ∃ (a_1 : L) (b : a_1 ∈ I),
    Subtype.mk (p := fun (a : L) ↦ a ∈ I) a_1 b ∈ J ∧
      (↑(Subtype.mk (p := fun (a : L) ↦ a ∈ I) a_1 b) : L) = ⁅a, (↑y : L)⁆
⊢ ∃ (a_1 : L) (b : a_1 ∈ I),
    Subtype.mk (p := fun (a : L) ↦ a ∈ I) a_1 b ∈ J ∧
      Eq (α := L) (((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (a : L) ↦ a ∈ I) a_1 b) : L)
        (⁅a, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)

Tactic:
erw [Submodule.coe_subtype]

Premises used: Submodule.coe_subtype
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
a₁ : Subtype.mk (p := fun (a : L) ↦ a ∈ I) ⁅a, (↑y : L)⁆ ⋯ ∈ J
⊢ ∃ (a_1 : L) (b : a_1 ∈ I),
    Subtype.mk (p := fun (a : L) ↦ a ∈ I) a_1 b ∈ J ∧
      (↑(Subtype.mk (p := fun (a : L) ↦ a ∈ I) a_1 b) : L) = ⁅a, (↑y : L)⁆

Tactic:
simp only [exists_and_right, exists_eq_right, ha, lie_mem_left, exists_true_left]

Premises used: exists_true_left, exists_eq_right, exists_and_right, lie_mem_left
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
⊢ Subtype.mk (p := fun (a : L) ↦ a ∈ I) ⁅a, (↑y : L)⁆ ⋯ ∈ J

Tactic:
lie_mem_right R I J ⟨a, ha⟩ y hy

Premises used: Set.Mem, Membership.mem, Subtype, Subtype.mk, lie_mem_right
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
⊢ Subtype.mk (p := fun (a : L) ↦ a ∈ I) ⁅a, (↑y : L)⁆ ⋯ ∈ J

Tactic:
exact lie_mem_right R I J ⟨a, ha⟩ y hy

Premises used: Membership.mem, Subtype, Subtype.mk, lie_mem_right
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
this : ⁅b, (↑y : L)⁆ = 0
erw : 0 ∈ Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)
⊢ Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I))
    (⁅b, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)

Tactic:
erw [this]
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
this : ⁅b, (↑y : L)⁆ = 0
⊢ 0 ∈ Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)

Tactic:
simp only [zero_mem]

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
a₁ : ⁅b, (↑y : L)⁆ = 0
⊢ Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I))
    (⁅b, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)

Tactic:
suffices ⁅b, y.val⁆ = 0 by erw [this]; simp only [zero_mem]
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
a₁ : ⁅b, (↑y : L)⁆ ∈ I ⊓ sSup ({I : LieIdeal R L | IsAtom I} \ {I})
⊢ ⁅b, (↑y : L)⁆ = 0

Tactic:
rw [← LieSubmodule.mem_bot (R := R) (L := L),
              ← (IsSemisimple.sSupIndep_isAtom hI).eq_bot]

Premises used: LieSubmodule.mem_bot, LieAlgebra.IsSemisimple.sSupIndep_isAtom, Disjoint.eq_bot
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
⊢ ⁅b, (↑y : L)⁆ ∈ I ⊓ sSup ({I : LieIdeal R L | IsAtom I} \ {I})

Tactic:
⟨lie_mem_right R L I b y y.2, lie_mem_left _ _ _ _ _ hb⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro, lie_mem_right, Subtype.val, lie_mem_left, Subtype.property
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
⊢ ⁅b, (↑y : L)⁆ ∈ I ⊓ sSup ({I : LieIdeal R L | IsAtom I} \ {I})

Tactic:
exact ⟨lie_mem_right R L I b y y.2, lie_mem_left _ _ _ _ _ hb⟩
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
rw : ¬J = ⊤ → J = ⊥
⊢ J = ⊥ ∨ J = ⊤

Tactic:
rw [or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
this : J' = ⊥
rw : ∀ (this : J' ≤ ⊥), J ≤ ⊥
⊢ J = ⊥

Tactic:
rw [eq_bot_iff] at this ⊢

Premises used: eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
this : J' ≤ ⊥
x : ↥I
hx : x ∈ J
suffices : x ∈ J → x = 0
⊢ Membership.mem (γ := LieSubmodule R ↥I ↥I) ⊥ x

Tactic:
suffices x ∈ J → x = 0 from this hx
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
this : J' ≤ ⊥
x : ↥I
hx : x ∈ J
⊢ (↑x : L) ∈ J' → Membership.mem (γ := LieSubmodule R L L) ⊥ (↑x : L)

Tactic:
have := @this x.1
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
this_1 : J' ≤ ⊥
x : ↥I
hx : x ∈ J
this : (↑x : L) ∈ J' → Membership.mem (γ := LieSubmodule R L L) ⊥ (↑x : L)
⊢ ∀ (x_1 : L) (x_2 : x_1 ∈ I),
    Subtype.mk (p := fun (a : L) ↦ a ∈ I) x_1 x_2 ∈ J →
      ((↑I : Submodule R L).subtype : (a : ↥I) → L) (Subtype.mk (p := fun (a : L) ↦ a ∈ I) x_1 x_2) = (↑x : L) → x = 0

Tactic:
simp only [LieIdeal.incl_coe, LieIdeal.toLieSubalgebra_toSubmodule,
        LieSubmodule.mem_mk_iff', Submodule.mem_map, LieSubmodule.mem_toSubmodule, Subtype.exists,
        LieSubmodule.mem_bot, ZeroMemClass.coe_eq_zero, forall_exists_index, and_imp, J'] at this

Premises used: ZeroMemClass.coe_eq_zero, LieSubmodule.mem_mk_iff', LieSubmodule.mem_toSubmodule, Submodule.mem_map, and_imp, LieIdeal.incl_coe, Subtype.exists, forall_exists_index, LieIdeal.toLieSubalgebra_toSubmodule, LieSubmodule.mem_bot
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
this_1 : J' ≤ ⊥
x : ↥I
hx : x ∈ J
this :
  ∀ (x_1 : L) (x_2 : x_1 ∈ I),
    Subtype.mk (p := fun (a : L) ↦ a ∈ I) x_1 x_2 ∈ J →
      ((↑I : Submodule R L).subtype : (a : ↥I) → L) (Subtype.mk (p := fun (a : L) ↦ a ∈ I) x_1 x_2) = (↑x : L) → x = 0
⊢ x ∈ J → x = 0

Tactic:
fun _ ↦ this (↑x) x.property hx rfl

Premises used: Subtype.val, rfl, Subtype.property
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
this_1 : J' ≤ ⊥
x : ↥I
hx : x ∈ J
this :
  ∀ (x_1 : L) (x_2 : x_1 ∈ I),
    Subtype.mk (p := fun (a : L) ↦ a ∈ I) x_1 x_2 ∈ J →
      ((↑I : Submodule R L).subtype : (a : ↥I) → L) (Subtype.mk (p := fun (a : L) ↦ a ∈ I) x_1 x_2) = (↑x : L) → x = 0
⊢ x ∈ J → x = 0

Tactic:
exact fun _ ↦ this (↑x) x.property hx rfl

Premises used: Subtype.val, rfl, Subtype.property
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
suffices : J' = ⊥
⊢ J = ⊥

Tactic:
suffices J' = ⊥ by
      rw [eq_bot_iff] at this ⊢
      intro x hx
      suffices x ∈ J → x = 0 from this hx
      have := @this x.1
      simp only [LieIdeal.incl_coe, LieIdeal.toLieSubalgebra_toSubmodule,
        LieSubmodule.mem_mk_iff', Submodule.mem_map, LieSubmodule.mem_toSubmodule, Subtype.exists,
        LieSubmodule.mem_bot, ZeroMemClass.coe_eq_zero, forall_exists_index, and_imp, J'] at this
      exact fun _ ↦ this (↑x) x.property hx rfl
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
a : J' < I
⊢ J' = ⊥

Tactic:
apply hI.2

Premises used: And.right
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
a : J' ≤ I ∧ J' ≠ I
⊢ J' < I

Tactic:
rw [lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
a : J' ≤ I
a₁ : J' ≠ I
⊢ J' ≤ I ∧ J' ≠ I

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
x : ↥I
⊢ Membership.mem (α := L) I (((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) x : L)

Tactic:
x.2

Premises used: Set.Mem, Subtype.property
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
x : ↥I
⊢ Membership.mem (α := L) I (((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) x : L)

Tactic:
exact x.2

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
a : ∀ (hJ : J' = I), J = ⊤
⊢ J' ≠ I

Tactic:
contrapose hJ
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : J' = I
a : ⊤ ≤ J
⊢ J = ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I);
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : J' = I
x : L
hx : x ∈ I
⊢ x ∈ J'

Tactic:
rw [← hJ] at hx