-- 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
⊢ (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))
              ⋯).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))
              ⋯).hom
      (I := I)
have hom : Eq (α :=
  Functor.obj (diag (P (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ⟶
    (P a).diag.obj (IsFiltered.coeq p q))
  (g.hom (I := I) ≫
    u.hom (I := I) ≫
      Functor.map (diag (P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))))) q ≫
        Functor.map (diag (P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))))) (IsFiltered.coeqHom p q))
  (g.hom (I := I) ≫
    u.hom (I := I) ≫
      Functor.map (diag (P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))))) p ≫
        Functor.map (diag (P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))))) (IsFiltered.coeqHom p q))
Tactic: simp only [Functor.map_comp, comp_hom, reassoc_of% hpq]