C : Type u_1
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this : Nontrivial (Subobject X)
⊢ ∃ Y, Simple (underlying.obj Y)
C : Type u_1
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
⊢ ∃ Y, Simple (underlying.obj Y)
haveI : Nontrivial (Subobject X) := nontrivial_of_not_isZero h
C : Type u_1
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this✝ : Nontrivial (Subobject X)
this : IsAtomic (Subobject X)
⊢ ∃ Y, Simple (underlying.obj Y)
C : Type u_1
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this : Nontrivial (Subobject X)
⊢ ∃ Y, Simple (underlying.obj Y)
haveI := isAtomic_of_orderBot_wellFounded_lt (ArtinianObject.subobject_lt_wellFounded X)
case intro
C : Type u_1
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this✝ : Nontrivial (Subobject X)
this : IsAtomic (Subobject X)
Y : Subobject X
s : IsAtom Y ∧ Y ≤ ⊤
⊢ ∃ Y, Simple (underlying.obj Y)
C : Type u_1
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this✝ : Nontrivial (Subobject X)
this : IsAtomic (Subobject X)
⊢ ∃ Y, Simple (underlying.obj Y)
obtain ⟨Y, s⟩ := (IsAtomic.eq_bot_or_exists_atom_le (⊤ : Subobject X)).resolve_left top_ne_bot
no goals
case intro
C : Type u_1
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this✝ : Nontrivial (Subobject X)
this : IsAtomic (Subobject X)
Y : Subobject X
s : IsAtom Y ∧ Y ≤ ⊤
⊢ ∃ Y, Simple (underlying.obj Y)
exact ⟨Y, (subobject_simple_iff_isAtom _).mpr s.1⟩