-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (goal)
Goal:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H :
  Eq (α := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
lem :
  ∀ (x y : (fun (X : Type u) ↦ X) Y),
    Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x y →
      (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun (x y : Y) ↦ x ∈ U ↔ y ∈ U
x : (fun (X : Type u) ↦ X) Y
y : Y
hy : y ∈ U
e' :
  Eq (α := Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            y :
          (coequalizerColimit f g).cocone.pt) :
      Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            x :
          (coequalizerColimit f g).cocone.pt) :
      Z)
e'' :
  Function.Injective (α := (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) (β :=
    (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
    (⇑(hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv) :
      (a : (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) → (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
⊢ Eq (α :=
    Quot (α := Y)
      (Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)))
    (Quot.mk
      (Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
      y)
    (Quot.mk
      (Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
      x)
have h₁ : Eq (α := (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
  ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
        (a : (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) → (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
      (Quot.mk
        (Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
          (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
          (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
        y) :
    (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
  ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
        (a : (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) → (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
      (Quot.mk
        (Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
          (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
          (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
        x) :
    (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
Tactic: apply e''