-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.End (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
j j' : J
g : j ⟶ j'
y : (F.obj (op j')).obj j
a :
  Eq (α := (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
    ((hom (FC := Fun) ((G.map g.op).app j) :
          (a : (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j)) →
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
        ((hom (FC := Fun) (NatTrans.app (f.app (op j')) j) :
            (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
              (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j))
          y) :
      (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
    ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
          (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
        ((Hom.hom ((F.map g.op).app j) : (a : (F.obj (op j')).obj j) → (F.obj (op j)).obj j) y) :
      (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
⊢ ∃ (f_1 : j ⟶ j') (y_1 : (G.obj (op j')).obj j),
    Eq (α := (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
        ((hom (FC := Fun) ((G.map f_1.op).app j) :
              (a : (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
            y_1 :
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
        ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
            ((Hom.hom ((F.map g.op).app j) : (a : (F.obj (op j')).obj j) → (F.obj (op j)).obj j) y) :
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j)) ∧
      Eq (α := (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
        ((hom (FC := Fun) ((G.obj (op j')).map f_1) :
              (a : (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
            y_1 :
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
        ((hom (FC := Fun) (NatTrans.app (f.app (op j')) j') :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j')) →
                (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
            ((Hom.hom ((F.obj (op j')).map g) : (a : (F.obj (op j')).obj j) → (F.obj (op j')).obj j') y) :
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
have a₁ : Eq (α := (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
  ((hom (FC := Fun) ((G.obj (op j')).map g) :
        (a : (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j)) →
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
      ((hom (FC := Fun) (NatTrans.app (f.app (op j')) j) :
          (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j))
        y) :
    (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
  ((hom (FC := Fun) (NatTrans.app (f.app (op j')) j') :
        (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j')) →
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
      ((Hom.hom ((F.obj (op j')).map g) : (a : (F.obj (op j')).obj j) → (F.obj (op j')).obj j') y) :
    (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
Tactic: refine ⟨g, (f.app _).app _ y, ?_, ?_⟩