-- Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean
theorem isColimit_exists_of_rep_eq {D : Cocone F} {i j : J} (hD : IsColimit D)
    (x : ToType (F.obj i)) (y : ToType (F.obj j)) (h : D.ι.app _ x = D.ι.app _ y) :
    ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max t w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
J : Type w
inst✝² : Category.{r, w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : ToType (F.obj i)
y : ToType (F.obj j)
h : (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y

Tactic:
let hE : IsColimit E := isColimitOfPreserves _ hD

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max t w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
J : Type w
inst✝² : Category.{r, w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : ToType (F.obj i)
y : ToType (F.obj j)
h : (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max t w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
J : Type w
inst✝² : Category.{r, w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : ToType (F.obj i)
y : ToType (F.obj j)
h : (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y

Tactic:
let E := (forget C).mapCocone D

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max t w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
J : Type w
inst✝² : Category.{r, w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : ToType (F.obj i)
y : ToType (F.obj j)
h : (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max t w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
J : Type w
inst✝² : Category.{r, w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : ToType (F.obj i)
y : ToType (F.obj j)
h : (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y

Tactic:
exact (Types.FilteredColimit.isColimit_eq_iff (F ⋙ forget C) hE).mp h

Result:
no goals