-- 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
h :
  (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i) =
      (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))
      ((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)
⊢ 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))
have h₁ : (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i) =
    (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 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))
    ((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)
Tactic: convert! Iff.rfl