case empty
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
⊢ ∃ S, ∀ {X : C}, X ∈ ∅ → _root_.Nonempty (S ⟶ X)

case insert
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
h : ∃ S, ∀ {X : C}, X ∈ O' → _root_.Nonempty (S ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (S ⟶ X_1)
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
O : Finset C
⊢ ∃ S, ∀ {X : C}, X ∈ O → _root_.Nonempty (S ⟶ X)
induction' O using Finset.induction with X O' nm h
case insert
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
h : ∃ S, ∀ {X : C}, X ∈ O' → _root_.Nonempty (S ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (S ⟶ X_1)
case empty
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
⊢ ∃ S, ∀ {X : C}, X ∈ ∅ → _root_.Nonempty (S ⟶ X)

case insert
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
h : ∃ S, ∀ {X : C}, X ∈ O' → _root_.Nonempty (S ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (S ⟶ X_1)
. exact ⟨Classical.choice IsCofiltered.Nonempty, by intro; simp⟩
no goals
case empty
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
⊢ ∃ S, ∀ {X : C}, X ∈ ∅ → _root_.Nonempty (S ⟶ X)
exact ⟨Classical.choice IsCofiltered.Nonempty, by intro; simp⟩
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X✝ : C
⊢ X✝ ∈ ∅ → _root_.Nonempty (Classical.choice (_ : _root_.Nonempty C) ⟶ X✝)
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
⊢ ∀ {X : C}, X ∈ ∅ → _root_.Nonempty (Classical.choice (_ : _root_.Nonempty C) ⟶ X)
intro
no goals
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X✝ : C
⊢ X✝ ∈ ∅ → _root_.Nonempty (Classical.choice (_ : _root_.Nonempty C) ⟶ X✝)
simp
case insert.intro
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (S ⟶ X_1)
case insert
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
h : ∃ S, ∀ {X : C}, X ∈ O' → _root_.Nonempty (S ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (S ⟶ X_1)
obtain ⟨S', w'⟩ := h
case insert.intro
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
⊢ ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (min X S' ⟶ X_1)
case insert.intro
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (S ⟶ X_1)
use min X S'
case insert.intro
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
⊢ _root_.Nonempty (min X S' ⟶ Y)
case insert.intro
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
⊢ ∀ {X_1 : C}, X_1 ∈ insert X O' → _root_.Nonempty (min X S' ⟶ X_1)
rintro Y mY
case insert.intro.inl
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
O' : Finset C
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
Y : C
nm : ¬Y ∈ O'
mY : Y ∈ insert Y O'
⊢ _root_.Nonempty (min Y S' ⟶ Y)

case insert.intro.inr
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
h : Y ≠ X
⊢ _root_.Nonempty (min X S' ⟶ Y)
case insert.intro
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
⊢ _root_.Nonempty (min X S' ⟶ Y)
obtain rfl | h := eq_or_ne Y X
no goals
case insert.intro.inl
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
O' : Finset C
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
Y : C
nm : ¬Y ∈ O'
mY : Y ∈ insert Y O'
⊢ _root_.Nonempty (min Y S' ⟶ Y)
exact ⟨minToLeft _ _⟩
no goals
case insert.intro.inr
C : Type u
inst✝¹ : Category C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : ¬X ∈ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → _root_.Nonempty (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
h : Y ≠ X
⊢ _root_.Nonempty (min X S' ⟶ Y)
exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩