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✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).pt ≅
    (CommSq.cone (_ : 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✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).π.app WalkingCospan.left =
    ?refine'_1.hom ≫ (CommSq.cone (_ : 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✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).π.app WalkingCospan.right =
    ?refine'_1.hom ≫ (CommSq.cone (_ : 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✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
refine'
  IsPullback.of_isLimit' (F.map_commSq s.toCommSq)
    (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext _ _ _)
      (isLimitOfPreserves F s.isLimit))
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✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).π.app WalkingCospan.right =
    (Iso.refl ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).pt).hom ≫
      (CommSq.cone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).π.app WalkingCospan.right
. simp
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✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).pt ≅
    (CommSq.cone (_ : 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✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).π.app WalkingCospan.left =
    (Iso.refl ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).pt).hom ≫
      (CommSq.cone (_ : 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✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).π.app WalkingCospan.right =
    (Iso.refl ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).pt).hom ≫
      (CommSq.cone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).π.app WalkingCospan.right
simp