-- Mathlib/CategoryTheory/Filtered/Final.lean
theorem Functor.final_of_exists_of_isFiltered_of_fullyFaithful [IsFilteredOrEmpty D] [F.Full]
    [F.Faithful] (h : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) : Final F

Proof state:
case intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : IsFilteredOrEmpty C
d : D
c : C
s s' : d ⟶ F.obj c
c₀ : C
f : IsFiltered.coeq s s' ⟶ F.obj c₀
⊢ s ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f)) = s' ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f))

Tactic:
simp [reassoc_of% (IsFiltered.coeq_condition s s')]

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : IsFilteredOrEmpty C
d : D
c : C
s s' : d ⟶ F.obj c
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
obtain ⟨c₀, ⟨f⟩⟩ := h (IsFiltered.coeq s s')

Result:
case intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : IsFilteredOrEmpty C
d : D
c : C
s s' : d ⟶ F.obj c
c₀ : C
f : IsFiltered.coeq s s' ⟶ F.obj c₀
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : IsFilteredOrEmpty C
⊢ F.Final

Tactic:
refine Functor.final_of_exists_of_isFiltered F h (fun {d c} s s' => ?_)

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : IsFilteredOrEmpty C
d : D
c : C
s s' : d ⟶ F.obj c
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
⊢ F.Final

Tactic:
have := IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful F h

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : IsFilteredOrEmpty C
⊢ F.Final

Proof state:
case intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : IsFilteredOrEmpty C
d : D
c : C
s s' : d ⟶ F.obj c
c₀ : C
f : IsFiltered.coeq s s' ⟶ F.obj c₀
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
refine ⟨c₀, F.preimage (IsFiltered.coeqHom s s' ≫ f), ?_⟩

Result:
case intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : IsFilteredOrEmpty C
d : D
c : C
s s' : d ⟶ F.obj c
c₀ : C
f : IsFiltered.coeq s s' ⟶ F.obj c₀
⊢ s ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f)) = s' ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f))