-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : (z : F.ColimitType) → ULift.{u, 0} Bool := fun (z : F.ColimitType) ↦ { down := decide (x = z) }
this :
  ∀ (z : F.ColimitType),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.desc
              ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
                (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
          (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
            (fun (X : Type u) ↦ X)
              ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
        (F.descColimitType c z) =
      f z
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
              (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
        (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
          (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
      (F.descColimitType c x) =
    f y
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
              (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
        (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
          (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
      (F.descColimitType c y) =
    f y
⊢ f x = f y
have rw₂ : Eq (α := ULift.{u, 0} Bool)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
              (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
        (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
          (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
      (F.descColimitType c y) :
    (fun (X : Type u) ↦ X)
      (Cocone.pt.{w, u, v, u + 1} (J := J) (F := F)
        ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
              (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
        (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
          (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
      (F.descColimitType c y) :
    (fun (X : Type u) ↦ X)
      (Cocone.pt.{w, u, v, u + 1} (J := J) (F := F)
        ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))))
Tactic: rw [← this x, h, ← this y]