-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
rw :
  Eq (α := (colimitCocone F).pt)
      ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
          ((hom (FC := TypeCat.Fun) (t.ι.app i) :
                (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
              xi :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i)) :
        (colimitCocone F).pt)
      ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
          ((hom (FC := TypeCat.Fun) (t.ι.app j) :
                (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
              xj :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j)) :
        (colimitCocone F).pt) ↔
    Eq (α :=
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
      ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app i) :
            (a : (fun (X : Type u) ↦ X) (F.obj i)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i))
          xi :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
      ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj j))
          xj :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) j))
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
      ((hom (FC := TypeCat.Fun) (t.ι.app i) :
            (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
          xi :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
      ((hom (FC := TypeCat.Fun) (t.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
          xj :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j)) ↔
    Eq (α :=
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
      ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app i) :
            (a : (fun (X : Type u) ↦ X) (F.obj i)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i))
          xi :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
      ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj j))
          xj :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) j))

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

Premises used: CategoryTheory.Iso.toEquiv, Function.Injective.eq_iff, CategoryTheory.Limits.Types.colimitCoconeIsColimit, Equiv.injective, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso