-- Mathlib/CategoryTheory/Filtered/Final.lean
theorem Functor.Final.exists_coeq_of_locally_small [IsFilteredOrEmpty C] [Final F] {d : D} {c : C}
    (s s' : d ⟶ F.obj c) : ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Proof state:
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
⊢ colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s'

Tactic:
apply (Final.colimitCompCoyonedaIso F d).toEquiv.injective

Result:
case a
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
⊢ (colimitCompCoyonedaIso F d).toEquiv (colimit.ι (F ⋙ coyoneda.obj (op d)) c s) =
    (colimitCompCoyonedaIso F d).toEquiv (colimit.ι (F ⋙ coyoneda.obj (op d)) c s')

Proof state:
case intro.intro.intro
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s'
c' : C
t₁ t₂ : c ⟶ c'
h : (F ⋙ coyoneda.obj (op d)).map t₁ s = (F ⋙ coyoneda.obj (op d)).map t₂ s'
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
refine ⟨IsFiltered.coeq t₁ t₂, t₁ ≫ IsFiltered.coeqHom t₁ t₂, ?_⟩

Result:
case intro.intro.intro
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s'
c' : C
t₁ t₂ : c ⟶ c'
h : (F ⋙ coyoneda.obj (op d)).map t₁ s = (F ⋙ coyoneda.obj (op d)).map t₂ s'
⊢ s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂) = s' ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂)

Proof state:
case intro.intro.intro
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s'
c' : C
t₁ t₂ : c ⟶ c'
h : (F ⋙ coyoneda.obj (op d)).map t₁ s = (F ⋙ coyoneda.obj (op d)).map t₂ s'
⊢ s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂) = s' ≫ F.map (t₂ ≫ IsFiltered.coeqHom t₁ t₂)

Tactic:
dsimp only [comp_obj, coyoneda_obj_obj, unop_op, Functor.comp_map, coyoneda_obj_map] at h

Result:
case intro.intro.intro
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s'
c' : C
t₁ t₂ : c ⟶ c'
h : s ≫ F.map t₁ = s' ≫ F.map t₂
⊢ s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂) = s' ≫ F.map (t₂ ≫ IsFiltered.coeqHom t₁ t₂)

Proof state:
case a
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
⊢ (colimitCompCoyonedaIso F d).toEquiv (colimit.ι (F ⋙ coyoneda.obj (op d)) c s) =
    (colimitCompCoyonedaIso F d).toEquiv (colimit.ι (F ⋙ coyoneda.obj (op d)) c s')

Tactic:
subsingleton

Result:
no goals

Proof state:
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
have : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s' := by
  apply (Final.colimitCompCoyonedaIso F d).toEquiv.injective
  subsingleton

Result:
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s'
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Proof state:
case intro.intro.intro
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s'
c' : C
t₁ t₂ : c ⟶ c'
h : s ≫ F.map t₁ = s' ≫ F.map t₂
⊢ s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂) = s' ≫ F.map (t₂ ≫ IsFiltered.coeqHom t₁ t₂)

Tactic:
simp [reassoc_of% h]

Result:
no goals

Proof state:
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s'
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
obtain ⟨c', t₁, t₂, h⟩ := (Types.FilteredColimit.colimit_eq_iff.{v₁, v₁, v₁} _).mp this

Result:
case intro.intro.intro
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s'
c' : C
t₁ t₂ : c ⟶ c'
h : (F ⋙ coyoneda.obj (op d)).map t₁ s = (F ⋙ coyoneda.obj (op d)).map t₂ s'
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Proof state:
case intro.intro.intro
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s'
c' : C
t₁ t₂ : c ⟶ c'
h : (F ⋙ coyoneda.obj (op d)).map t₁ s = (F ⋙ coyoneda.obj (op d)).map t₂ s'
⊢ s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂) = s' ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂)

Tactic:
conv_rhs => rw [IsFiltered.coeq_condition t₁ t₂]

Result:
case intro.intro.intro
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s'
c' : C
t₁ t₂ : c ⟶ c'
h : (F ⋙ coyoneda.obj (op d)).map t₁ s = (F ⋙ coyoneda.obj (op d)).map t₂ s'
⊢ s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂) = s' ≫ F.map (t₂ ≫ IsFiltered.coeqHom t₁ t₂)