Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁶ : Category.{v_1, u_1} J✝
inst✝⁵ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝⁴ : SmallCategory J
inst✝³ : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := IsFiltered.coeq f.base g.base
a' : I (IsFiltered.coeq f.base g.base)
u : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.coeq f.base g.base) a'
hu : u.base = IsFiltered.coeqHom f.base g.base
this :
  (f.hom ≫ u.hom) ≫
      (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).ι.app
        (Total.mk P (IsFiltered.coeq f.base g.base) a').snd =
    (g.hom ≫ u.hom) ≫
      (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).ι.app (Total.mk P (IsFiltered.coeq f.base g.base) a').snd
j : I (Total.mk P (IsFiltered.coeq f.base g.base) a').fst
p q : a' ⟶ j
hpq :
  (f.hom ≫ u.hom) ≫ (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map p =
    (g.hom ≫ u.hom) ≫ (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map q
⊢ f ≫
      u ≫
        { base := 𝟙 (Total.mk P (IsFiltered.coeq f.base g.base) a').fst,
          hom := (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map (p ≫ IsFiltered.coeqHom p q),
          w := ⋯ } =
    g ≫
      u ≫
        { base := 𝟙 (Total.mk P (IsFiltered.coeq f.base g.base) a').fst,
          hom := (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map (p ≫ IsFiltered.coeqHom p q), w := ⋯ }

Tactic:
apply Total.Hom.ext

Goal state after:
case base
C : Type u
inst✝⁷ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁶ : Category.{v_1, u_1} J✝
inst✝⁵ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝⁴ : SmallCategory J
inst✝³ : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := ⋯
a' : I (IsFiltered.coeq f.base g.base)
u : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.coeq f.base g.base) a'
hu : u.base = IsFiltered.coeqHom f.base g.base
this :
  (f.hom ≫ u.hom) ≫
      (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).ι.app
        (Total.mk P (IsFiltered.coeq f.base g.base) a').snd =
    (g.hom ≫ u.hom) ≫
      (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).ι.app (Total.mk P (IsFiltered.coeq f.base g.base) a').snd
j : I (Total.mk P (IsFiltered.coeq f.base g.base) a').fst
p q : a' ⟶ j
hpq :
  (f.hom ≫ u.hom) ≫ (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map p =
    (g.hom ≫ u.hom) ≫ (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map q
⊢ (f ≫
        u ≫
          { base := 𝟙 (Total.mk P (IsFiltered.coeq f.base g.base) a').fst,
            hom := (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map (p ≫ IsFiltered.coeqHom p q),
            w := ⋯ }).base =
    (g ≫
        u ≫
          { base := 𝟙 (Total.mk P (IsFiltered.coeq f.base g.base) a').fst,
            hom := (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map (p ≫ IsFiltered.coeqHom p q),
            w := ⋯ }).base

case hom
C : Type u
inst✝⁷ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁶ : Category.{v_1, u_1} J✝
inst✝⁵ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝⁴ : SmallCategory J
inst✝³ : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := ⋯
a' : I (IsFiltered.coeq f.base g.base)
u : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.coeq f.base g.base) a'
hu : u.base = IsFiltered.coeqHom f.base g.base
this :
  (f.hom ≫ u.hom) ≫
      (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).ι.app
        (Total.mk P (IsFiltered.coeq f.base g.base) a').snd =
    (g.hom ≫ u.hom) ≫
      (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).ι.app (Total.mk P (IsFiltered.coeq f.base g.base) a').snd
j : I (Total.mk P (IsFiltered.coeq f.base g.base) a').fst
p q : a' ⟶ j
hpq :
  (f.hom ≫ u.hom) ≫ (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map p =
    (g.hom ≫ u.hom) ≫ (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map q
⊢ (f ≫
        u ≫
          { base := 𝟙 (Total.mk P (IsFiltered.coeq f.base g.base) a').fst,
            hom := (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map (p ≫ IsFiltered.coeqHom p q),
            w := ⋯ }).hom =
    (g ≫
        u ≫
          { base := 𝟙 (Total.mk P (IsFiltered.coeq f.base g.base) a').fst,
            hom := (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map (p ≫ IsFiltered.coeqHom p q),
            w := ⋯ }).hom