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

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

Tactic:
intro

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

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

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

Result:
no goals

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

Tactic:
obtain rfl | h := eq_or_ne Y X

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

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

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

Tactic:
rintro Y mY

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

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

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

Result:
no goals

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

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

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

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

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

Tactic:
use max X S'

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

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

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

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

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

Tactic:
simp

Result:
no goals

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

Tactic:
exact ⟨leftToMax _ _⟩

Result:
no goals