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

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)
c c' : C
f g : c ⟶ c'
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
obtain ⟨c₀, ⟨f₀⟩⟩ := h (IsFiltered.coeq (F.map f) (F.map g))

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)
c c' : C
f g : c ⟶ c'
c₀ : C
f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀
⊢ ∃ Z h, f ≫ h = g ≫ h

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)
c c' c₀ : C
f : IsFiltered.max (F.obj c) (F.obj c') ⟶ F.obj c₀
⊢ ∃ Z x x, True

Tactic:
exact ⟨c₀, F.preimage (IsFiltered.leftToMax _ _ ≫ f),
  F.preimage (IsFiltered.rightToMax _ _ ≫ f), trivial⟩

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)
c c' : C
⊢ ∃ Z x x, True

Tactic:
obtain ⟨c₀, ⟨f⟩⟩ := h (IsFiltered.max (F.obj c) (F.obj c'))

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)
c c' c₀ : C
f : IsFiltered.max (F.obj c) (F.obj c') ⟶ F.obj c₀
⊢ ∃ Z x x, True

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)
c c' : C
f g : c ⟶ c'
c₀ : C
f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀
⊢ F.map (f ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀)) =
    F.map (g ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀))

Tactic:
simp [reassoc_of% (IsFiltered.coeq_condition (F.map f) (F.map g))]

Result:
no goals

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)
c c' : C
f g : c ⟶ c'
c₀ : C
f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
refine ⟨_, F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀), F.map_injective ?_⟩

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)
c c' : C
f g : c ⟶ c'
c₀ : C
f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀
⊢ F.map (f ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀)) =
    F.map (g ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀))