awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: apply add_mem
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ 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)
have 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)
Tactic: simp only [Submodule.mem_map, LieSubmodule.mem_toSubmodule, Subtype.exists]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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_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)
have 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)⁆
Tactic: erw [Submodule.coe_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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_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)⁆
have a₁ : Subtype.mk (p := fun (a : L) ↦ a ∈ I) ⁅a, (↑y : L)⁆ sorry ∈ J
Tactic: simp only [exists_and_right, exists_eq_right, ha, lie_mem_left, exists_true_left]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ 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)
have erw : 0 ∈ Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)
Tactic: erw [this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ 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)
have a₁ : ⁅b, (↑y : L)⁆ = 0
Tactic: suffices ⁅b, y.val⁆ = 0 by erw [this]; simp only [zero_mem]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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)⁆ = 0
have a₁ : ⁅b, (↑y : L)⁆ ∈ I ⊓ sSup ({I : LieIdeal R L | IsAtom I} \ {I})
Tactic: rw [← LieSubmodule.mem_bot (R := R) (L := L),
              ← (IsSemisimple.sSupIndep_isAtom hI).eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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 := ⋯ }
⊢ J = ⊥ ∨ J = ⊤
have rw : ¬J = ⊤ → J = ⊥
Tactic: rw [or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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' = ⊥
⊢ J = ⊥
have rw : ∀ (this : J' ≤ ⊥), J ≤ ⊥
Tactic: rw [eq_bot_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ Membership.mem (γ := LieSubmodule R ↥I ↥I) ⊥ x
have suffices : x ∈ J → x = 0
Tactic: suffices x ∈ J → x = 0 from this hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
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 ∈ J → x = 0
have this₁ : (↑x : L) ∈ J' → Membership.mem (γ := LieSubmodule R L L) ⊥ (↑x : L)
Tactic: have := @this x.1
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
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 ∈ J → x = 0
have 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
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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 = ⊤
⊢ J = ⊥
have suffices : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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 = ⊤
⊢ J' = ⊥
have a : J' < I
Tactic: apply hI.2
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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 = ⊤
⊢ J' < I
have a : J' ≤ I ∧ J' ≠ I
Tactic: rw [lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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 = ⊤
⊢ J' ≤ I ∧ J' ≠ I
have a : J' ≤ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
have a₁ : J' ≠ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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 = ⊤
⊢ J' ≠ I
have a : ∀ (hJ : J' = I), J = ⊤
Tactic: contrapose hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
⊢ J = ⊤
have a : ⊤ ≤ J
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
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
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx ∈ J
have hx₁ : x ∈ J'
Tactic: rw [← hJ] at hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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_1 : x ∈ I
hx : x ∈ J'
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx_1 ∈ J
have a : ∀ (y : ↥I) (hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I))
  (hx : Membership.mem (α := L) I (((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y : L)),
  Membership.mem (α := ↥I) J (Subtype.mk (p := fun (x : L) ↦ x ∈ I) (((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y) hx : ↥I)
Tactic: rcases hx with ⟨y, hy, rfl⟩
Cleared hypotheses: x, hx_1, hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
⊢ ∃ t ⊆ s, I = t.sup id
have inl : ∀ (hI : s.sup id ≤ s.sup id), ∃ t ⊆ s, s.sup id = t.sup id
Tactic: obtain rfl | hI := hI.eq_or_lt
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
inl : ∀ (hI : s.sup id ≤ s.sup id), ∃ t ⊆ s, s.sup id = t.sup id
⊢ ∃ t ⊆ s, I = t.sup id
have inr : ∀ (hI : I < s.sup id), ∃ t ⊆ s, I = t.sup id
Tactic: obtain rfl | hI := hI.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
⊢ ∃ J ∈ s, ¬J ≤ I
have by_contra! : ∀ (H : ∀ (J : LieIdeal R L) (_ : J ∈ s), J ≤ I), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
⊢ ∃ t ⊆ s, I = t.sup id
have inr : ∀ (J : LieIdeal R L) (hJs : J ∈ s) (hJI : ¬J ≤ I), ∃ t ⊆ s, I = t.sup id
Tactic: obtain ⟨J, hJs, hJI⟩ : ∃ J ∈ s, ¬ J ≤ I := by
    by_contra! H
    exact hI.ne (le_antisymm hI.le (s.sup_le H))
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
⊢ ∃ t ⊆ s, I = t.sup id
have hs' : s' ⊂ s
Tactic: have hs' : s' ⊂ s := Finset.erase_ssubset hJs
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
⊢ ∃ t ⊆ s, I = t.sup id
have hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
Tactic: have hs'S : ↑s' ⊆ S := Set.Subset.trans (Finset.coe_subset.mpr hs'.subset) hs
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
this : I ≤ K
⊢ ∃ t ⊆ s, I = t.sup id
have obtain : ∀ (t : Finset (LieIdeal R L)) (hts' : t ⊆ s') (htI : I = t.sup id), ∃ t ⊆ s, I = t.sup id
Tactic: obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
⊢ ∃ t ⊆ s, I = t.sup id
have inr : I ≤ K
Tactic: suffices I ≤ K by
    obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this
    exact ⟨t, hts'.trans hs'.subset, htI⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
x : L
hx : x ∈ I
⊢ ∃ y ∈ id J, ∃ z ∈ K, y + z = x
have rw : x ∈ s.sup id
Tactic: rw [← LieSubmodule.mem_sup, ← Finset.sup_insert, Finset.insert_erase hJs]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
x : L
hx : x ∈ I
⊢ x ∈ K
have inr : ∀ (y : L) (hy : y ∈ id J) (z : L) (hz : z ∈ K) (hx : y + z ∈ I), y + z ∈ K
Tactic: obtain ⟨y, hy, z, hz, rfl⟩ : ∃ y ∈ id J, ∃ z ∈ K, y + z = x := by
    rw [← LieSubmodule.mem_sup, ← Finset.sup_insert, Finset.insert_erase hJs]
    exact hI.le hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
this : Membership.mem (γ := LieIdeal R ↥J) (center R ↥J) (Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy)
⊢ y + z ∈ K
have _inst : IsSimple.{u_1, u_2} R ↥J
Tactic: have _inst := isSimple_of_isAtom J (hs hJs)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
⊢ y + z ∈ K
have inr : Membership.mem (γ := LieIdeal R ↥J) (center R ↥J) (Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy)
Tactic: suffices ⟨y, hy⟩ ∈ LieAlgebra.center R J by
    have _inst := isSimple_of_isAtom J (hs hJs)
    simp_all
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
this : ⁅(↑j : L), z⁆ = 0 ∧ ⁅(↑j : L), y + z⁆ = 0
⊢ ⁅j, Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy⁆ = 0
have this₁ : Eq.{u_2 + 1} (α := L) 0 0 ∧ ⁅(↑j : L), y⁆ = 0
Tactic: rw [lie_add, this.1, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
this : Eq.{u_2 + 1} (α := L) 0 0 ∧ ⁅(↑j : L), y⁆ = 0
⊢ ⁅j, Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy⁆ = 0
have a : (↑⁅j, Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy⁆ : L) = (↑0 : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
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
s : Finset (LieIdeal R L)
hs : (↑s : Set (LieIdeal R L)) ⊆ {I : LieIdeal R L | IsAtom I}
I : LieIdeal R L
hI_1 : I ≤ s.sup id
S : Set (LieIdeal R L) := {I : LieIdeal R L | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : (↑s' : Set (LieIdeal R L)) ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
⊢ ⁅j, Subtype.mk (p := fun (x : L) ↦ x ∈ J) y hy⁆ = 0
have inr : ⁅(↑j : L), z⁆ = 0 ∧ ⁅(↑j : L), y + z⁆ = 0
Tactic: suffices ⁅(j : L), z⁆ = 0 ∧ ⁅(j : L), y + z⁆ = 0 by
    rw [lie_add, this.1, add_zero] at this
    ext
    exact this.2