case refine'_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).pt ≅
    (CommSq.cocone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).pt

case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).ι.app WalkingCospan.left ≫
      ?refine'_1.hom =
    (CommSq.cocone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).ι.app WalkingCospan.left

case refine'_3
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).ι.app WalkingCospan.right ≫
      ?refine'_1.hom =
    (CommSq.cocone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).ι.app WalkingCospan.right
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
refine'
  IsPushout.of_isColimit' (F.map_commSq s.toCommSq)
    (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext _ _ _)
      (isColimitOfPreserves F s.isColimit))
no goals
case refine'_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).pt ≅
    (CommSq.cocone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).pt
rfl
no goals
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).ι.app WalkingCospan.left ≫
      (Iso.refl ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).pt).hom =
    (CommSq.cocone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).ι.app WalkingCospan.left
simp
no goals
case refine'_3
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).ι.app WalkingCospan.right ≫
      (Iso.refl ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).pt).hom =
    (CommSq.cocone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).ι.app WalkingCospan.right
simp