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

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

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

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