[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g
[PROOFSTEP]
simp only [← G.map_comp, comm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ ∀ (j : WalkingCospan),
    NatTrans.app
        ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone (PullbackCone.mk h k comm))).π j =
      (Iso.refl
            ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj
                (G.mapCone (PullbackCone.mk h k comm))).pt).hom ≫
        NatTrans.app (PullbackCone.mk (G.map h) (G.map k) (_ : G.map h ≫ G.map f = G.map k ≫ G.map g)).π j
[PROOFSTEP]
rintro (_ | _ | _)
[GOAL]
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ NatTrans.app
      ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone (PullbackCone.mk h k comm))).π none =
    (Iso.refl
          ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj
              (G.mapCone (PullbackCone.mk h k comm))).pt).hom ≫
      NatTrans.app (PullbackCone.mk (G.map h) (G.map k) (_ : G.map h ≫ G.map f = G.map k ≫ G.map g)).π none
[PROOFSTEP]
dsimp
[GOAL]
case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ NatTrans.app
      ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone (PullbackCone.mk h k comm))).π
      (some WalkingPair.left) =
    (Iso.refl
          ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj
              (G.mapCone (PullbackCone.mk h k comm))).pt).hom ≫
      NatTrans.app (PullbackCone.mk (G.map h) (G.map k) (_ : G.map h ≫ G.map f = G.map k ≫ G.map g)).π
        (some WalkingPair.left)
[PROOFSTEP]
dsimp
[GOAL]
case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ NatTrans.app
      ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone (PullbackCone.mk h k comm))).π
      (some WalkingPair.right) =
    (Iso.refl
          ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj
              (G.mapCone (PullbackCone.mk h k comm))).pt).hom ≫
      NatTrans.app (PullbackCone.mk (G.map h) (G.map k) (_ : G.map h ≫ G.map f = G.map k ≫ G.map g)).π
        (some WalkingPair.right)
[PROOFSTEP]
dsimp
[GOAL]
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ G.map (h ≫ f) ≫ 𝟙 (G.obj Z) = 𝟙 (G.obj W) ≫ G.map h ≫ G.map f
[PROOFSTEP]
simp only [comp_id, id_comp, G.map_comp]
[GOAL]
case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ G.map h ≫ 𝟙 (G.obj X) = 𝟙 (G.obj W) ≫ G.map h
[PROOFSTEP]
simp only [comp_id, id_comp, G.map_comp]
[GOAL]
case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ G.map k ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj W) ≫ G.map k
[PROOFSTEP]
simp only [comp_id, id_comp, G.map_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
l : IsLimit (PullbackCone.mk h k comm)
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g
[PROOFSTEP]
rw [← G.map_comp, ← G.map_comp, comm]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : ReflectsLimit (cospan f g) G
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g
[PROOFSTEP]
simp only [← G.map_comp, comm]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
i : HasPullback f g
⊢ G.map pullback.fst ≫ G.map f = G.map pullback.snd ≫ G.map g
[PROOFSTEP]
simp only [← G.map_comp, pullback.condition]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (G.mapCone c)
[PROOFSTEP]
apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₂} _) _).toFun
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit ((Cones.postcompose (diagramIsoCospan (cospan g f ⋙ G)).hom).obj (G.mapCone c))
[PROOFSTEP]
apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _).symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit
    (PullbackCone.mk (NatTrans.app (G.mapCone c).π WalkingCospan.left)
      (NatTrans.app (G.mapCone c).π WalkingCospan.right)
      (_ :
        NatTrans.app (G.mapCone c).π WalkingCospan.left ≫ (cospan g f ⋙ G).map WalkingCospan.Hom.inl =
          NatTrans.app (G.mapCone c).π WalkingCospan.right ≫ (cospan g f ⋙ G).map WalkingCospan.Hom.inr))
[PROOFSTEP]
apply PullbackCone.flipIsLimit
[GOAL]
case t
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit
    (PullbackCone.mk (NatTrans.app (G.mapCone c).π WalkingCospan.right)
      (NatTrans.app (G.mapCone c).π WalkingCospan.left)
      (_ :
        NatTrans.app (G.mapCone c).π WalkingCospan.right ≫ (cospan g f ⋙ G).map WalkingCospan.Hom.inr =
          NatTrans.app (G.mapCone c).π WalkingCospan.left ≫ (cospan g f ⋙ G).map WalkingCospan.Hom.inl))
[PROOFSTEP]
apply (isLimitMapConePullbackConeEquiv _ _).toFun
[GOAL]
case t
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit
    (G.mapCone (PullbackCone.mk (NatTrans.app c.π WalkingCospan.right) (NatTrans.app c.π WalkingCospan.left) ?m.19346))
[PROOFSTEP]
refine @PreservesLimit.preserves _ _ _ _ _ _ _ _ ?_ _ ?_
[GOAL]
case t.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ PreservesLimit (cospan ((cospan g f).map WalkingCospan.Hom.inr) ((cospan g f).map WalkingCospan.Hom.inl)) G
[PROOFSTEP]
dsimp
[GOAL]
case t.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ PreservesLimit (cospan f g) G
[PROOFSTEP]
infer_instance
[GOAL]
case t.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk (NatTrans.app c.π WalkingCospan.right) (NatTrans.app c.π WalkingCospan.left) ?m.19346)
[PROOFSTEP]
apply PullbackCone.flipIsLimit
[GOAL]
case t.refine_2.t
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit
    (PullbackCone.mk (NatTrans.app c.π WalkingCospan.left) (NatTrans.app c.π WalkingCospan.right)
      (_ :
        NatTrans.app c.π WalkingCospan.left ≫ (cospan g f).map WalkingCospan.Hom.inl =
          NatTrans.app c.π WalkingCospan.right ≫ (cospan g f).map WalkingCospan.Hom.inr))
[PROOFSTEP]
apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit ((Cones.postcompose (diagramIsoCospan (cospan g f)).hom).obj c)
[PROOFSTEP]
exact (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₁} _) _).invFun hc
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ NatTrans.app c.π WalkingCospan.right ≫ (cospan g f).map WalkingCospan.Hom.inr =
    NatTrans.app c.π WalkingCospan.left ≫ (cospan g f).map WalkingCospan.Hom.inl
[PROOFSTEP]
exact (c.π.naturality WalkingCospan.Hom.inr).symm.trans (c.π.naturality WalkingCospan.Hom.inl : _)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).hom ≫ pullback.fst = G.map pullback.fst
[PROOFSTEP]
simp [PreservesPullback.iso]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).hom ≫ pullback.snd = G.map pullback.snd
[PROOFSTEP]
simp [PreservesPullback.iso]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).inv ≫ G.map pullback.fst = pullback.fst
[PROOFSTEP]
simp [PreservesPullback.iso, Iso.inv_comp_eq]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).inv ≫ G.map pullback.snd = pullback.snd
[PROOFSTEP]
simp [PreservesPullback.iso, Iso.inv_comp_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k
[PROOFSTEP]
simp only [← G.map_comp, comm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ ∀ (j : WalkingSpan),
    NatTrans.app
          ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).ι
          j ≫
        (Iso.refl
            ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
                (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
      NatTrans.app (PushoutCocone.mk (G.map h) (G.map k) (_ : G.map f ≫ G.map h = G.map g ≫ G.map k)).ι j
[PROOFSTEP]
rintro (_ | _ | _)
[GOAL]
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι
        none ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
    NatTrans.app (PushoutCocone.mk (G.map h) (G.map k) (_ : G.map f ≫ G.map h = G.map g ≫ G.map k)).ι none
[PROOFSTEP]
dsimp
[GOAL]
case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι
        (some WalkingPair.left) ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
    NatTrans.app (PushoutCocone.mk (G.map h) (G.map k) (_ : G.map f ≫ G.map h = G.map g ≫ G.map k)).ι
      (some WalkingPair.left)
[PROOFSTEP]
dsimp
[GOAL]
case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι
        (some WalkingPair.right) ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
    NatTrans.app (PushoutCocone.mk (G.map h) (G.map k) (_ : G.map f ≫ G.map h = G.map g ≫ G.map k)).ι
      (some WalkingPair.right)
[PROOFSTEP]
dsimp
[GOAL]
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj W) ≫ G.map (f ≫ h)) ≫ 𝟙 (G.obj Z) = G.map f ≫ G.map h
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp, ← G.map_comp]
[GOAL]
case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj X) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp, ← G.map_comp]
[GOAL]
case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj Y) ≫ G.map k) ≫ 𝟙 (G.obj Z) = G.map k
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp, ← G.map_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
l : IsColimit (PushoutCocone.mk h k comm)
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k
[PROOFSTEP]
simp only [← G.map_comp, comm]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : ReflectsColimit (span f g) G
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k
[PROOFSTEP]
simp only [← G.map_comp, comm]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
i : HasPushout f g
⊢ G.map f ≫ G.map pushout.inl = G.map g ≫ G.map pushout.inr
[PROOFSTEP]
simp only [← G.map_comp, pushout.condition]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (G.mapCocone c)
[PROOFSTEP]
apply (IsColimit.precomposeHomEquiv (diagramIsoSpan.{v₂} _).symm _).toFun
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit ((Cocones.precompose (diagramIsoSpan (span g f ⋙ G)).symm.hom).obj (G.mapCocone c))
[PROOFSTEP]
apply IsColimit.ofIsoColimit _ (PushoutCocone.isoMk _).symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit
    (PushoutCocone.mk (NatTrans.app (G.mapCocone c).ι WalkingSpan.left)
      (NatTrans.app (G.mapCocone c).ι WalkingSpan.right)
      (_ :
        (span g f ⋙ G).map WalkingSpan.Hom.fst ≫ NatTrans.app (G.mapCocone c).ι WalkingSpan.left =
          (span g f ⋙ G).map WalkingSpan.Hom.snd ≫ NatTrans.app (G.mapCocone c).ι WalkingSpan.right))
[PROOFSTEP]
apply PushoutCocone.flipIsColimit
[GOAL]
case t
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit
    (PushoutCocone.mk (NatTrans.app (G.mapCocone c).ι WalkingSpan.right)
      (NatTrans.app (G.mapCocone c).ι WalkingSpan.left)
      (_ :
        (span g f ⋙ G).map WalkingSpan.Hom.snd ≫ NatTrans.app (G.mapCocone c).ι WalkingSpan.right =
          (span g f ⋙ G).map WalkingSpan.Hom.fst ≫ NatTrans.app (G.mapCocone c).ι WalkingSpan.left))
[PROOFSTEP]
apply (isColimitMapCoconePushoutCoconeEquiv _ _).toFun
[GOAL]
case t
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit
    (G.mapCocone (PushoutCocone.mk (NatTrans.app c.ι WalkingSpan.right) (NatTrans.app c.ι WalkingSpan.left) ?m.60067))
[PROOFSTEP]
refine
  @PreservesColimit.preserves _ _ _ _ _ _ _ _ ?_ _
    ?_
      -- Porting note: more TC coddling
[GOAL]
case t.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ PreservesColimit (span ((span g f).map WalkingSpan.Hom.snd) ((span g f).map WalkingSpan.Hom.fst)) G
[PROOFSTEP]
dsimp
[GOAL]
case t.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ PreservesColimit (span f g) G
[PROOFSTEP]
infer_instance
[GOAL]
case t.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (PushoutCocone.mk (NatTrans.app c.ι WalkingSpan.right) (NatTrans.app c.ι WalkingSpan.left) ?m.60067)
[PROOFSTEP]
apply PushoutCocone.flipIsColimit
[GOAL]
case t.refine_2.t
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι WalkingSpan.left) (NatTrans.app c.ι WalkingSpan.right)
      (_ :
        (span g f).map WalkingSpan.Hom.fst ≫ NatTrans.app c.ι WalkingSpan.left =
          (span g f).map WalkingSpan.Hom.snd ≫ NatTrans.app c.ι WalkingSpan.right))
[PROOFSTEP]
apply IsColimit.ofIsoColimit _ (PushoutCocone.isoMk _)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit ((Cocones.precompose (diagramIsoSpan (span g f)).inv).obj c)
[PROOFSTEP]
exact (IsColimit.precomposeHomEquiv (diagramIsoSpan.{v₁} _) _).invFun hc
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ (span g f).map WalkingSpan.Hom.snd ≫ NatTrans.app c.ι WalkingSpan.right =
    (span g f).map WalkingSpan.Hom.fst ≫ NatTrans.app c.ι WalkingSpan.left
[PROOFSTEP]
exact (c.ι.naturality WalkingSpan.Hom.snd).trans (c.ι.naturality WalkingSpan.Hom.fst).symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inl ≫ (iso G f g).hom = G.map pushout.inl
[PROOFSTEP]
delta PreservesPushout.iso
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inl ≫
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (span (G.map f) (G.map g)))
          (isColimitOfHasPushoutOfPreservesColimit G f g)).hom =
    G.map pushout.inl
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inr ≫ (iso G f g).hom = G.map pushout.inr
[PROOFSTEP]
delta PreservesPushout.iso
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inr ≫
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (span (G.map f) (G.map g)))
          (isColimitOfHasPushoutOfPreservesColimit G f g)).hom =
    G.map pushout.inr
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ G.map pushout.inl ≫ (iso G f g).inv = pushout.inl
[PROOFSTEP]
simp [PreservesPushout.iso, Iso.comp_inv_eq]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ G.map pushout.inr ≫ (iso G f g).inv = pushout.inr
[PROOFSTEP]
simp [PreservesPushout.iso, Iso.comp_inv_eq]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ PreservesLimit (cospan f g) G
[PROOFSTEP]
apply preservesLimitOfPreservesLimitCone (pullbackIsPullback f g)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsLimit (G.mapCone (PullbackCone.mk pullback.fst pullback.snd (_ : pullback.fst ≫ f = pullback.snd ≫ g)))
[PROOFSTEP]
apply (isLimitMapConePullbackConeEquiv _ _).symm _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsLimit
    (PullbackCone.mk (G.map pullback.fst) (G.map pullback.snd)
      (_ : G.map pullback.fst ≫ G.map f = G.map pullback.snd ≫ G.map g))
[PROOFSTEP]
refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (cospan (G.map f) (G.map g))) ?_
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsIso
    (IsLimit.lift (limit.isLimit (cospan (G.map f) (G.map g)))
      (PullbackCone.mk (G.map pullback.fst) (G.map pullback.snd)
        (_ : G.map pullback.fst ≫ G.map f = G.map pullback.snd ≫ G.map g)))
[PROOFSTEP]
apply i
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : HasPullback f g
inst✝¹ : HasPullback (G.map f) (G.map g)
inst✝ : PreservesLimit (cospan f g) G
⊢ IsIso (pullbackComparison G f g)
[PROOFSTEP]
rw [← PreservesPullback.iso_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : HasPullback f g
inst✝¹ : HasPullback (G.map f) (G.map g)
inst✝ : PreservesLimit (cospan f g) G
⊢ IsIso (PreservesPullback.iso G f g).hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ PreservesColimit (span f g) G
[PROOFSTEP]
apply preservesColimitOfPreservesColimitCocone (pushoutIsPushout f g)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ IsColimit (G.mapCocone (PushoutCocone.mk pushout.inl pushout.inr (_ : f ≫ pushout.inl = g ≫ pushout.inr)))
[PROOFSTEP]
apply
  (isColimitMapCoconePushoutCoconeEquiv _ _).symm
    _
      -- Porting note: apply no longer creates goals for instances
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ IsColimit
    (PushoutCocone.mk (G.map pushout.inl) (G.map pushout.inr)
      (_ : G.map f ≫ G.map pushout.inl = G.map g ≫ G.map pushout.inr))
[PROOFSTEP]
refine @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (span (G.map f) (G.map g))) ?_
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ IsIso
    (IsColimit.desc (colimit.isColimit (span (G.map f) (G.map g)))
      (PushoutCocone.mk (G.map pushout.inl) (G.map pushout.inr)
        (_ : G.map f ≫ G.map pushout.inl = G.map g ≫ G.map pushout.inr)))
[PROOFSTEP]
apply i
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
⊢ IsIso (pushoutComparison G f g)
[PROOFSTEP]
rw [← PreservesPushout.iso_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
⊢ IsIso (PreservesPushout.iso G f g).hom
[PROOFSTEP]
infer_instance
