-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
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
⊢ 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))
have 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))
Tactic: rw [← (IsColimit.coconePointUniqueUpToIso ht (colimitCoconeIsColimit F)).toEquiv.injective.eq_iff]