[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PushoutCocone.inl (PullbackCone.op (cone p)) ≫ (Iso.refl (PullbackCone.op (cone p)).pt).hom =
    PushoutCocone.inl (cocone (_ : CommSq h.op i.op f.op g.op))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PushoutCocone.inr (PullbackCone.op (cone p)) ≫ (Iso.refl (PullbackCone.op (cone p)).pt).hom =
    PushoutCocone.inr (cocone (_ : CommSq h.op i.op f.op g.op))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PullbackCone.fst (PushoutCocone.op (cocone p)) =
    (Iso.refl (PushoutCocone.op (cocone p)).pt).hom ≫ PullbackCone.fst (cone (_ : CommSq h.op i.op f.op g.op))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PullbackCone.snd (PushoutCocone.op (cocone p)) =
    (Iso.refl (PushoutCocone.op (cocone p)).pt).hom ≫ PullbackCone.snd (cone (_ : CommSq h.op i.op f.op g.op))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PushoutCocone.inl (PullbackCone.unop (cone p)) ≫ (Iso.refl (PullbackCone.unop (cone p)).pt).hom =
    PushoutCocone.inl (cocone (_ : CommSq h.unop i.unop f.unop g.unop))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PushoutCocone.inr (PullbackCone.unop (cone p)) ≫ (Iso.refl (PullbackCone.unop (cone p)).pt).hom =
    PushoutCocone.inr (cocone (_ : CommSq h.unop i.unop f.unop g.unop))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PullbackCone.fst (PushoutCocone.unop (cocone p)) =
    (Iso.refl (PushoutCocone.unop (cocone p)).pt).hom ≫ PullbackCone.fst (cone (_ : CommSq h.unop i.unop f.unop g.unop))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ PullbackCone.snd (PushoutCocone.unop (cocone p)) =
    (Iso.refl (PushoutCocone.unop (cocone p)).pt).hom ≫ PullbackCone.snd (cone (_ : CommSq h.unop i.unop f.unop g.unop))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
h : IsLimit c
⊢ PullbackCone.fst c =
    (Iso.refl c.pt).hom ≫
      PullbackCone.fst
        (PullbackCone.mk (PullbackCone.fst c) (PullbackCone.snd c)
          (_ : PullbackCone.fst c ≫ f = PullbackCone.snd c ≫ g))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
h : IsLimit c
⊢ PullbackCone.snd c =
    (Iso.refl c.pt).hom ≫
      PullbackCone.snd
        (PullbackCone.mk (PullbackCone.fst c) (PullbackCone.snd c)
          (_ : PullbackCone.fst c ≫ f = PullbackCone.snd c ≫ g))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ ∀ (j : Discrete WalkingPair),
    NatTrans.app c.π j =
      (Iso.refl c.pt).hom ≫
        NatTrans.app (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ NatTrans.app c.π { as := WalkingPair.left } =
    (Iso.refl c.pt).hom ≫
      NatTrans.app (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π
        { as := WalkingPair.left }
[PROOFSTEP]
dsimp
[GOAL]
case mk.left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ BinaryFan.fst c = 𝟙 c.pt ≫ BinaryFan.fst c
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ NatTrans.app c.π { as := WalkingPair.right } =
    (Iso.refl c.pt).hom ≫
      NatTrans.app (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π
        { as := WalkingPair.right }
[PROOFSTEP]
dsimp
[GOAL]
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ BinaryFan.snd c = 𝟙 c.pt ≫ BinaryFan.snd c
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
⊢ IsPullback prod.fst prod.snd 0 0
[PROOFSTEP]
convert @of_is_product _ _ X Y 0 _ (limit.isLimit _) HasZeroObject.zeroIsTerminal
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (isoPullback h).hom ≫ pullback.fst = fst
[PROOFSTEP]
dsimp [isoPullback, cone, CommSq.cone]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (limit.isoLimitCone { cone := PullbackCone.mk fst snd (_ : fst ≫ f = snd ≫ g), isLimit := isLimit h }).inv ≫
      pullback.fst =
    fst
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (isoPullback h).hom ≫ pullback.snd = snd
[PROOFSTEP]
dsimp [isoPullback, cone, CommSq.cone]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (limit.isoLimitCone { cone := PullbackCone.mk fst snd (_ : fst ≫ f = snd ≫ g), isLimit := isLimit h }).inv ≫
      pullback.snd =
    snd
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (isoPullback h).inv ≫ fst = pullback.fst
[PROOFSTEP]
simp [Iso.inv_comp_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (isoPullback h).inv ≫ snd = pullback.snd
[PROOFSTEP]
simp [Iso.inv_comp_eq]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
⊢ IsLimit (CommSq.cone sq)
[PROOFSTEP]
refine' PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by aesop_cat) (fun s => _) (by aesop_cat)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
⊢ ∀ (s : PullbackCone f g), (fun s => PullbackCone.fst s ≫ inv fst) s ≫ fst = PullbackCone.fst s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
⊢ ∀ (s : PullbackCone f g) (m : s.pt ⟶ P),
    m ≫ fst = PullbackCone.fst s → m ≫ snd = PullbackCone.snd s → m = (fun s => PullbackCone.fst s ≫ inv fst) s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
s : PullbackCone f g
⊢ (fun s => PullbackCone.fst s ≫ inv fst) s ≫ snd = PullbackCone.snd s
[PROOFSTEP]
simp only [← cancel_mono g, Category.assoc, ← sq.w, IsIso.inv_hom_id_assoc, s.condition]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : PushoutCocone f g
h : IsColimit c
⊢ PushoutCocone.inl c ≫ (Iso.refl c.pt).hom =
    PushoutCocone.inl
      (PushoutCocone.mk (PushoutCocone.inl c) (PushoutCocone.inr c)
        (_ : f ≫ PushoutCocone.inl c = g ≫ PushoutCocone.inr c))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : PushoutCocone f g
h : IsColimit c
⊢ PushoutCocone.inr c ≫ (Iso.refl c.pt).hom =
    PushoutCocone.inr
      (PushoutCocone.mk (PushoutCocone.inl c) (PushoutCocone.inr c)
        (_ : f ≫ PushoutCocone.inl c = g ≫ PushoutCocone.inr c))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ ∀ (j : Discrete WalkingPair),
    NatTrans.app c.ι j ≫ (Iso.refl c.pt).hom =
      NatTrans.app (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ NatTrans.app c.ι { as := WalkingPair.left } ≫ (Iso.refl c.pt).hom =
    NatTrans.app (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι
      { as := WalkingPair.left }
[PROOFSTEP]
dsimp
[GOAL]
case mk.left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ BinaryCofan.inl c ≫ 𝟙 c.pt = BinaryCofan.inl c
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ NatTrans.app c.ι { as := WalkingPair.right } ≫ (Iso.refl c.pt).hom =
    NatTrans.app (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι
      { as := WalkingPair.right }
[PROOFSTEP]
dsimp
[GOAL]
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ BinaryCofan.inr c ≫ 𝟙 c.pt = BinaryCofan.inr c
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝² : HasBinaryCoproduct X Y
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
⊢ IsPushout 0 0 coprod.inl coprod.inr
[PROOFSTEP]
convert @of_is_coproduct _ _ 0 X Y _ (colimit.isColimit _) HasZeroObject.zeroIsInitial
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inl ≫ (isoPushout h).inv = inl
[PROOFSTEP]
dsimp [isoPushout, cocone, CommSq.cocone]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inl ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk inl inr (_ : f ≫ inl = g ≫ inr), isColimit := isColimit h }).hom =
    inl
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr ≫ (isoPushout h).inv = inr
[PROOFSTEP]
dsimp [isoPushout, cocone, CommSq.cocone]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk inl inr (_ : f ≫ inl = g ≫ inr), isColimit := isColimit h }).hom =
    inr
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ inl ≫ (isoPushout h).hom = pushout.inl
[PROOFSTEP]
simp [← Iso.eq_comp_inv]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ inr ≫ (isoPushout h).hom = pushout.inr
[PROOFSTEP]
simp [← Iso.eq_comp_inv]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X✝ Y Z : C
fst : P ⟶ X✝
snd : P ⟶ Y
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ 𝟙 X = 0 ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X✝ Y Z : C
fst : P ⟶ X✝
snd : P ⟶ Y
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cone (cospan (𝟙 X) 0)
⊢ ∀ (j : WalkingCospan),
    (fun s => 0) s ≫ NatTrans.app (PullbackCone.mk 0 0 (_ : 0 ≫ 𝟙 X = 0 ≫ 0)).π j = NatTrans.app s.π j
[PROOFSTEP]
simpa using @PullbackCone.equalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _) (by simpa using (PullbackCone.condition s).symm)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X✝ Y Z : C
fst : P ⟶ X✝
snd : P ⟶ Y
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cone (cospan (𝟙 X) 0)
⊢ 0 ≫ PullbackCone.fst s = 𝟙 s.pt ≫ PullbackCone.fst s
[PROOFSTEP]
simpa using (PullbackCone.condition s).symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X✝ Y Z : C
fst : P ⟶ X✝
snd : P ⟶ Y
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ CommSq 0 (𝟙 X) 0 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X✝ Y Z : C
fst : P ⟶ X✝
snd : P ⟶ Y
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ((zeroProdIso X).symm ≪≫ (pullbackZeroZeroIso 0 X).symm).hom ≫ pullback.fst = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X✝ Y Z : C
fst : P ⟶ X✝
snd : P ⟶ Y
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ((zeroProdIso X).symm ≪≫ (pullbackZeroZeroIso 0 X).symm).hom ≫ pullback.snd = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback b.fst b.snd 0 0
[PROOFSTEP]
convert IsPullback.of_is_product' h.isLimit HasZeroObject.zeroIsTerminal
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback b.inl 0 b.snd 0
[PROOFSTEP]
refine' of_right _ (by simp) (of_isBilimit h)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ b.inl ≫ b.snd = 0 ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback (b.inl ≫ b.fst) 0 0 (0 ≫ 0)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback b.inr 0 b.fst 0
[PROOFSTEP]
apply flip
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback 0 b.inr 0 b.fst
[PROOFSTEP]
refine' of_bot _ (by simp) (of_isBilimit h)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ 0 ≫ 0 = b.inr ≫ b.fst
[PROOFSTEP]
simp
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback 0 (b.inr ≫ b.snd) (0 ≫ 0) 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback 0 0 b.inl b.inr
[PROOFSTEP]
refine' IsPullback.of_right _ (by simp) (IsPullback.inl_snd' h).flip
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ 0 ≫ b.inl = 0 ≫ b.inr
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPullback (0 ≫ 0) 0 0 (b.inr ≫ b.snd)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ 0 = 𝟙 X ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ ∀ (j : WalkingSpan),
    NatTrans.app (PushoutCocone.mk 0 0 (_ : 0 ≫ 0 = 𝟙 X ≫ 0)).ι j ≫ (fun s => 0) s = NatTrans.app s.ι j
[PROOFSTEP]
have c := @PushoutCocone.coequalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _) (by simp) (by simpa using PushoutCocone.condition s)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ PushoutCocone.inl s ≫ 0 = PushoutCocone.inl s ≫ 𝟙 s.pt
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ PushoutCocone.inr s ≫ 0 = PushoutCocone.inr s ≫ 𝟙 s.pt
[PROOFSTEP]
simpa using PushoutCocone.condition s
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
c : ∀ (j : WalkingSpan), NatTrans.app s.ι j ≫ 0 = NatTrans.app s.ι j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan),
    NatTrans.app (PushoutCocone.mk 0 0 (_ : 0 ≫ 0 = 𝟙 X ≫ 0)).ι j ≫ (fun s => 0) s = NatTrans.app s.ι j
[PROOFSTEP]
dsimp at c 
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
c : ∀ (j : WalkingSpan), NatTrans.app s.ι j ≫ 0 = NatTrans.app s.ι j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan),
    NatTrans.app (PushoutCocone.mk 0 0 (_ : 0 ≫ 0 = 𝟙 X ≫ 0)).ι j ≫ (fun s => 0) s = NatTrans.app s.ι j
[PROOFSTEP]
simpa using c
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ CommSq 0 0 (𝟙 X) 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 𝟙 X ≫ ((coprodZeroIso X).symm ≪≫ (pushoutZeroZeroIso X 0).symm).hom = pushout.inl
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X✝ Y P : C
f : Z ⟶ X✝
g : Z ⟶ Y
inl : X✝ ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ ((coprodZeroIso X).symm ≪≫ (pushoutZeroZeroIso X 0).symm).hom = pushout.inr
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout 0 0 b.inl b.inr
[PROOFSTEP]
convert IsPushout.of_is_coproduct' h.isColimit HasZeroObject.zeroIsInitial
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout b.inl 0 b.snd 0
[PROOFSTEP]
apply flip
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout 0 b.inl 0 b.snd
[PROOFSTEP]
refine' of_right _ (by simp) (of_isBilimit h)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ 0 ≫ 0 = b.inl ≫ b.snd
[PROOFSTEP]
simp
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout (0 ≫ 0) 0 0 (b.inr ≫ b.snd)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout b.inr 0 b.fst 0
[PROOFSTEP]
refine' of_bot _ (by simp) (of_isBilimit h)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ b.inr ≫ b.fst = 0 ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout 0 (0 ≫ 0) (b.inl ≫ b.fst) 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout b.fst b.snd 0 0
[PROOFSTEP]
refine' IsPushout.of_right _ (by simp) (IsPushout.inl_snd' h)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ b.fst ≫ 0 = b.snd ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : BinaryBicone.IsBilimit b
⊢ IsPushout (b.inl ≫ b.fst) 0 0 (0 ≫ 0)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ IsColimit (CommSq.cocone sq)
[PROOFSTEP]
refine' PushoutCocone.IsColimit.mk _ (fun s => inv inr ≫ s.inr) (fun s => _) (by aesop_cat) (by aesop_cat)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ ∀ (s : PushoutCocone f g), inr ≫ (fun s => inv inr ≫ PushoutCocone.inr s) s = PushoutCocone.inr s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ ∀ (s : PushoutCocone f g) (m : P ⟶ s.pt),
    inl ≫ m = PushoutCocone.inl s → inr ≫ m = PushoutCocone.inr s → m = (fun s => inv inr ≫ PushoutCocone.inr s) s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
s : PushoutCocone f g
⊢ inl ≫ (fun s => inv inr ≫ PushoutCocone.inr s) s = PushoutCocone.inl s
[PROOFSTEP]
simp only [← cancel_epi f, s.condition, sq.w_assoc, IsIso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ IsLimit (Fork.ofι f (_ : f ≫ g = f ≫ g'))
[PROOFSTEP]
fapply Fork.IsLimit.mk
[GOAL]
case lift
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ (s : Fork g g') → s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
[PROOFSTEP]
exact fun s => H.isLimit.lift (PullbackCone.mk s.ι s.ι s.condition)
[GOAL]
case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g'),
    IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
        Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) =
      Fork.ι s
[PROOFSTEP]
exact fun s => H.isLimit.fac _ WalkingCospan.left
[GOAL]
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g') (m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt),
    m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s →
      m = IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g'))
[PROOFSTEP]
intro s m e
[GOAL]
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ m = IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g'))
[PROOFSTEP]
apply PullbackCone.IsLimit.hom_ext H.isLimit
[GOAL]
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ m ≫ PullbackCone.fst (cone H) =
    IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
      PullbackCone.fst (cone H)
[PROOFSTEP]
refine' e.trans _
[GOAL]
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ m ≫ PullbackCone.snd (cone H) =
    IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
      PullbackCone.snd (cone H)
[PROOFSTEP]
refine' e.trans _
[GOAL]
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ Fork.ι s =
    IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
      PullbackCone.fst (cone H)
[PROOFSTEP]
symm
[GOAL]
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ Fork.ι s =
    IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
      PullbackCone.snd (cone H)
[PROOFSTEP]
symm
[GOAL]
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
      PullbackCone.fst (cone H) =
    Fork.ι s
[PROOFSTEP]
exact H.isLimit.fac _ _
[GOAL]
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f (_ : f ≫ g = f ≫ g')).pt
e : m ≫ Fork.ι (Fork.ofι f (_ : f ≫ g = f ≫ g')) = Fork.ι s
⊢ IsLimit.lift (isLimit H) (PullbackCone.mk (Fork.ι s) (Fork.ι s) (_ : Fork.ι s ≫ g = Fork.ι s ≫ g')) ≫
      PullbackCone.snd (cone H) =
    Fork.ι s
[PROOFSTEP]
exact H.isLimit.fac _ _
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ IsColimit (Cofork.ofπ g (_ : f ≫ g = f' ≫ g))
[PROOFSTEP]
fapply Cofork.IsColimit.mk
[GOAL]
case desc
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ (s : Cofork f f') → (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
[PROOFSTEP]
exact fun s => H.isColimit.desc (PushoutCocone.mk s.π s.π s.condition)
[GOAL]
case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f'),
    Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫
        IsColimit.desc (isColimit H)
          (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s)) =
      Cofork.π s
[PROOFSTEP]
exact fun s => H.isColimit.fac _ WalkingSpan.left
[GOAL]
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f') (m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt),
    Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s →
      m =
        IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s))
[PROOFSTEP]
intro s m e
[GOAL]
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ m = IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s))
[PROOFSTEP]
apply PushoutCocone.IsColimit.hom_ext H.isColimit
[GOAL]
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ PushoutCocone.inl (cocone H) ≫ m =
    PushoutCocone.inl (cocone H) ≫
      IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s))
[PROOFSTEP]
refine' e.trans _
[GOAL]
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ PushoutCocone.inr (cocone H) ≫ m =
    PushoutCocone.inr (cocone H) ≫
      IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s))
[PROOFSTEP]
refine' e.trans _
[GOAL]
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ Cofork.π s =
    PushoutCocone.inl (cocone H) ≫
      IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s))
[PROOFSTEP]
symm
[GOAL]
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ Cofork.π s =
    PushoutCocone.inr (cocone H) ≫
      IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s))
[PROOFSTEP]
symm
[GOAL]
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ PushoutCocone.inl (cocone H) ≫
      IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s)) =
    Cofork.π s
[PROOFSTEP]
exact H.isColimit.fac _ _
[GOAL]
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)).pt ⟶ s.pt
e : Cofork.π (Cofork.ofπ g (_ : f ≫ g = f' ≫ g)) ≫ m = Cofork.π s
⊢ PushoutCocone.inr (cocone H) ≫
      IsColimit.desc (isColimit H) (PushoutCocone.mk (Cofork.π s) (Cofork.π s) (_ : f ≫ Cofork.π s = f' ≫ Cofork.π s)) =
    Cofork.π s
[PROOFSTEP]
exact H.isColimit.fac _ _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproduct X Y
⊢ BicartesianSq biprod.fst biprod.snd 0 0
[PROOFSTEP]
convert of_is_biproduct₁ (BinaryBiproduct.isBilimit X Y)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproduct X Y
⊢ BicartesianSq 0 0 biprod.inl biprod.inr
[PROOFSTEP]
convert of_is_biproduct₂ (BinaryBiproduct.isBilimit X Y)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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)
[PROOFSTEP]
refine'
  IsPullback.of_isLimit' (F.map_commSq s.toCommSq)
    (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext _ _ _) (isLimitOfPreserves F s.isLimit))
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
⊢ NatTrans.app ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).π
      WalkingCospan.left =
    (Iso.refl ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).pt).hom ≫
      NatTrans.app (CommSq.cone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).π WalkingCospan.left
[PROOFSTEP]
simp
[GOAL]
case refine'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
⊢ NatTrans.app ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).π
      WalkingCospan.right =
    (Iso.refl ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (IsPullback.cone s))).pt).hom ≫
      NatTrans.app (CommSq.cone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).π WalkingCospan.right
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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)
[PROOFSTEP]
refine'
  IsPushout.of_isColimit' (F.map_commSq s.toCommSq)
    (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext _ _ _) (isColimitOfPreserves F s.isColimit))
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
⊢ NatTrans.app ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).ι
        WalkingCospan.left ≫
      (Iso.refl ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).pt).hom =
    NatTrans.app (CommSq.cocone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).ι WalkingCospan.left
[PROOFSTEP]
simp
[GOAL]
case refine'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
⊢ NatTrans.app ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).ι
        WalkingCospan.right ≫
      (Iso.refl ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (IsPushout.cocone s))).pt).hom =
    NatTrans.app (CommSq.cocone (_ : CommSq (F.map f) (F.map g) (F.map h) (F.map i))).ι WalkingCospan.right
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
[PROOFSTEP]
refine' ⟨⟨e⟩, ⟨isLimitOfReflects F <| _⟩⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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)))
[PROOFSTEP]
refine' (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext _ _ _)).symm H.isLimit
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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)
⊢ NatTrans.app
      ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))).π
      WalkingCospan.left =
    ?refine'_1.hom ≫ NatTrans.app (cone H).π WalkingCospan.left
case refine'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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)
⊢ NatTrans.app
      ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g (_ : f ≫ h = g ≫ i)))).π
      WalkingCospan.right =
    ?refine'_1.hom ≫ NatTrans.app (cone H).π WalkingCospan.right
[PROOFSTEP]
exacts [Iso.refl _, (Category.comp_id _).trans (Category.id_comp _).symm,
  (Category.comp_id _).trans (Category.id_comp _).symm]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} 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
inst✝ : Faithful F
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)
[PROOFSTEP]
simpa only [F.map_comp] using H.w
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsPushout f g h i
[PROOFSTEP]
refine' ⟨⟨e⟩, ⟨isColimitOfReflects F <| _⟩⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsColimit (F.mapCocone (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)))
[PROOFSTEP]
refine' (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext _ _ _)).symm H.isColimit
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)))).pt ≅
    (cocone H).pt
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ NatTrans.app
        ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)))).ι
        WalkingCospan.left ≫
      ?refine'_1.hom =
    NatTrans.app (cocone H).ι WalkingCospan.left
case refine'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ NatTrans.app
        ((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)))).ι
        WalkingCospan.right ≫
      ?refine'_1.hom =
    NatTrans.app (cocone H).ι WalkingCospan.right
[PROOFSTEP]
exacts [Iso.refl _, (Category.comp_id _).trans (Category.id_comp _), (Category.comp_id _).trans (Category.id_comp _)]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝¹ : ReflectsColimit (span f g) F
inst✝ : Faithful F
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)
[PROOFSTEP]
simpa only [F.map_comp] using H.w
