no goals
C : Type u
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
W X✝ Y✝ Z X Y S T S' : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
i' : S ⟶ S'
inst✝³ : HasPullback f g
inst✝² : HasPullback (f ≫ i) (g ≫ i)
inst✝¹ : HasPullback (f ≫ i ≫ i') (g ≫ i ≫ i')
inst✝ : HasPullback ((f ≫ i) ≫ i') ((g ≫ i) ≫ i')
⊢ mapDesc f g (i ≫ i') =
    mapDesc f g i ≫
      mapDesc (f ≫ i) (g ≫ i) i' ≫ (congrHom (_ : (f ≫ i) ≫ i' = f ≫ i ≫ i') (_ : (g ≫ i) ≫ i' = g ≫ i ≫ i')).hom
aesop_cat