-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.ColimitPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type u_1
I_1 : J_1 → Type u_2
inst_1 : Category.{v_1, u_1} J_1
inst_2 : (j : J_1) → Category.{?u.30679, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.30679, u_2, v, u} (I_1 j) (D_1.obj j)
J : Type w
I : J → Type w
inst_3 : SmallCategory J
inst_4 : (j : J) → SmallCategory (I j)
D : Functor.{w, v, w, u} J C
P : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (D.obj j)
inst_5 : IsFiltered J
inst_6 : ∀ (j : J), IsFiltered.{w, w} (I j)
inst_7 : ∀ (j : J) (i : I j), IsFinitelyPresentable.{w, v, u} ((P j).diag.obj i)
k l : Total (I := I) P
f g : k ⟶ l
a : J := IsFiltered.coeq (f.base (I := I)) (g.base (I := I))
a' : I (IsFiltered.coeq (f.base (I := I)) (g.base (I := I)))
u :
  Total.mk (I := I) P (l.fst (β := fun (j : J) ↦ I j)) (l.snd (β := fun (j : J) ↦ I j)) ⟶
    Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a'
hu : u.base (I := I) = IsFiltered.coeqHom (f.base (I := I)) (g.base (I := I))
this :
  (f.hom (I := I) ≫ u.hom (I := I)) ≫
      NatTrans.app
        (ι
          (P
            ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦
              I j))))
        ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').snd (β := fun (j : J) ↦ I j)) =
    (g.hom (I := I) ≫ u.hom (I := I)) ≫
      NatTrans.app
        (ι
          (P
            ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦
              I j))))
        ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').snd (β := fun (j : J) ↦ I j))
j : I ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦ I j))
p q : a' ⟶ j
hpq :
  (f.hom (I := I) ≫ u.hom (I := I)) ≫
      Functor.map
        (diag
          (P
            ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦
              I j))))
        p =
    (g.hom (I := I) ≫ u.hom (I := I)) ≫
      Functor.map
        (diag
          (P
            ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦
              I j))))
        q
⊢ ∃ (Z : Total (I := I) P) (h : l ⟶ Z), f ≫ h = g ≫ h
have refine : f ≫
    u ≫
      Total.Hom.mk (I := I)
        (𝟙
          ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦ I j)))
        (Functor.map
          (diag
            (P
              ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦
                I j))))
          (p ≫ IsFiltered.coeqHom p q))
        sorry =
  g ≫
    u ≫
      Total.Hom.mk (I := I)
        (𝟙
          ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦ I j)))
        (Functor.map
          (diag
            (P
              ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦
                I j))))
          (p ≫ IsFiltered.coeqHom p q))
        sorry
Tactic: refine ⟨⟨a, IsFiltered.coeq p q⟩,
      u ≫ { base := 𝟙 _, hom := (P _).diag.map (p ≫ IsFiltered.coeqHom p q) }, ?_⟩