C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : Simple X
⊢ IsSimpleOrder (Subobject X)
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
⊢ Simple X → IsSimpleOrder (Subobject X)
intro h
no goals
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : Simple X
⊢ IsSimpleOrder (Subobject X)
infer_instance
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : IsSimpleOrder (Subobject X)
⊢ Simple X
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
⊢ IsSimpleOrder (Subobject X) → Simple X
intro h
no goals
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : IsSimpleOrder (Subobject X)
⊢ Simple X
exact simple_of_isSimpleOrder_subobject X