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✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsLimit (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))
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✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsPullback f g h i
refine' ⟨⟨e⟩, ⟨isLimitOfReflects F <| _⟩⟩
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✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))).pt ≅
    (cone H).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✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))).π.app
      WalkingCospan.left =
    ?refine'_1.hom ≫ (cone H).π.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✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))).π.app
      WalkingCospan.right =
    ?refine'_1.hom ≫ (cone H).π.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✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsLimit (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))
refine'
  (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext _ _ _)).symm
    H.isLimit
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✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))).pt ≅
    (cone H).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✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))).π.app
      WalkingCospan.left =
    ?refine'_1.hom ≫ (cone H).π.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✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))).π.app
      WalkingCospan.right =
    ?refine'_1.hom ≫ (cone H).π.app WalkingCospan.right
exacts [Iso.refl _, (Category.comp_id _).trans (Category.id_comp _).symm,
  (Category.comp_id _).trans (Category.id_comp _).symm]