-- 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
base :
  (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))
              ⋯).base
      (I := I) =
    (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))
              ⋯).base
      (I := I)
⊢ 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))
          ⋯ =
    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))
          ⋯
have hom : (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).hom
    (I := I) =
  (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).hom
    (I := I)
Tactic: apply Total.Hom.ext