-- Mathlib/CategoryTheory/Limits/TypesFiltered.lean
theorem isColimit_eq_iff {t : Cocone F} (ht : IsColimit t) {i j : J} {xi : F.obj i} {xj : F.obj j} :
    t.ι.app i xi = t.ι.app j xj ↔ ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj

Proof state:
case h.e'_2.h.e'_2.h
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1✝ : ((Functor.const J).obj (colimitCocone F).pt).obj i = (colimitCocone F).pt
⊢ (colimitCocone F).ι.app i xi = (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv (t.ι.app i xi)

Tactic:
exact (congrFun
  (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xi).symm

Result:
no goals

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
⊢ t.ι.app i xi = t.ι.app j xj ↔ ∃ k f g, F.map f xi = F.map g xj

Tactic:
refine Iff.trans ?_ (colimit_eq_iff_aux F)

Result:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
⊢ t.ι.app i xi = t.ι.app j xj ↔ (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
⊢ t.ι.app i xi = t.ι.app j xj ↔ ∃ k f g, F.map f xi = F.map g xj

Tactic:
have : HasColimit F := ⟨_, ht⟩

Result:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
⊢ t.ι.app i xi = t.ι.app j xj ↔ ∃ k f g, F.map f xi = F.map g xj

Proof state:
case h.e'_2.h.e'_3.h
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1✝ : ((Functor.const J).obj (colimitCocone F).pt).obj i = (colimitCocone F).pt
⊢ (colimitCocone F).ι.app j xj = (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv (t.ι.app j xj)

Tactic:
exact (congrFun
  (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xj).symm

Result:
no goals

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
⊢ t.ι.app i xi = t.ι.app j xj ↔ (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj

Tactic:
rw [← (IsColimit.coconePointUniqueUpToIso ht (colimitCoconeIsColimit F)).toEquiv.injective.eq_iff]

Result:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
⊢ (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv (t.ι.app i xi) =
      (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv (t.ι.app j xj) ↔
    (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
⊢ (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv (t.ι.app i xi) =
      (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv (t.ι.app j xj) ↔
    (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj

Tactic:
convert Iff.rfl

Result:
case h.e'_2.h.e'_2.h
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1✝ : ((Functor.const J).obj (colimitCocone F).pt).obj i = (colimitCocone F).pt
⊢ (colimitCocone F).ι.app i xi = (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv (t.ι.app i xi)

case h.e'_2.h.e'_3.h
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1✝ : ((Functor.const J).obj (colimitCocone F).pt).obj i = (colimitCocone F).pt
⊢ (colimitCocone F).ι.app j xj = (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv (t.ι.app j xj)