-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem inf_objs_exists (O : Finset C) : ∃ S : C, ∀ {X}, X ∈ O → Nonempty (S ⟶ X)

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (S' ⟶ X)
⊢ ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (min X S' ⟶ X_1)

Tactic:
rintro Y mY

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
⊢ Nonempty (min X S' ⟶ Y)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
⊢ ∀ {X : C}, X ∈ ∅ → Nonempty (Classical.choice ⋯ ⟶ X)

Tactic:
intro

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X✝ : C
⊢ X✝ ∈ ∅ → Nonempty (Classical.choice ⋯ ⟶ X✝)

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

Tactic:
exact ⟨Classical.choice IsCofiltered.nonempty, by intro; simp⟩

Result:
no goals

Proof state:
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : X ∉ O'
h : ∃ S, ∀ {X : C}, X ∈ O' → Nonempty (S ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (S ⟶ X_1)

Tactic:
obtain ⟨S', w'⟩ := h

Result:
case insert.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (S' ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (S ⟶ X_1)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X✝ : C
⊢ X✝ ∈ ∅ → Nonempty (Classical.choice ⋯ ⟶ X✝)

Tactic:
simp

Result:
no goals

Proof state:
case insert.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (S' ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (S ⟶ X_1)

Tactic:
use min X S'

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (S' ⟶ X)
⊢ ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (min X S' ⟶ X_1)

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
⊢ Nonempty (min X S' ⟶ Y)

Tactic:
obtain rfl | h := eq_or_ne Y X

Result:
case h.inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O' : Finset C
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (S' ⟶ X)
Y : C
nm : Y ∉ O'
mY : Y ∈ insert Y O'
⊢ Nonempty (min Y S' ⟶ Y)

case h.inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
h : Y ≠ X
⊢ Nonempty (min X S' ⟶ Y)

Proof state:
case h.inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
h : Y ≠ X
⊢ Nonempty (min X S' ⟶ Y)

Tactic:
exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
⊢ ∃ S, ∀ {X : C}, X ∈ O → Nonempty (S ⟶ X)

Tactic:
induction' O using Finset.induction with X O' nm h

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

case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
X : C
O' : Finset C
nm : X ∉ O'
h : ∃ S, ∀ {X : C}, X ∈ O' → Nonempty (S ⟶ X)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (S ⟶ X_1)

Proof state:
case h.inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O' : Finset C
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (S' ⟶ X)
Y : C
nm : Y ∉ O'
mY : Y ∈ insert Y O'
⊢ Nonempty (min Y S' ⟶ Y)

Tactic:
exact ⟨minToLeft _ _⟩

Result:
no goals