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 : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
i' : S' ⟶ S
inst✝³ : HasPushout f g
inst✝² : HasPushout (i ≫ f) (i ≫ g)
inst✝¹ : HasPushout (i' ≫ i ≫ f) (i' ≫ i ≫ g)
inst✝ : HasPushout ((i' ≫ i) ≫ f) ((i' ≫ i) ≫ g)
⊢ mapLift f g (i' ≫ i) =
    (congrHom (_ : (i' ≫ i) ≫ f = i' ≫ i ≫ f) (_ : (i' ≫ i) ≫ g = i' ≫ i ≫ g)).hom ≫
      mapLift (i ≫ f) (i ≫ g) i' ≫ mapLift f g i
aesop_cat