[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
⊢ ∀ (j : Discrete WalkingPair),
    NatTrans.app ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).π j =
      (Iso.refl ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt).hom ≫
        NatTrans.app (BinaryFan.mk (G.map f) (G.map g)).π j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case mk.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
⊢ NatTrans.app ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).π
      { as := WalkingPair.left } =
    (Iso.refl ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt).hom ≫
      NatTrans.app (BinaryFan.mk (G.map f) (G.map g)).π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
⊢ NatTrans.app ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).π
      { as := WalkingPair.right } =
    (Iso.refl ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt).hom ≫
      NatTrans.app (BinaryFan.mk (G.map f) (G.map g)).π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ PreservesLimit (pair X Y) G
[PROOFSTEP]
apply preservesLimitOfPreservesLimitCone (prodIsProd X Y)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsLimit (G.mapCone (BinaryFan.mk prod.fst prod.snd))
[PROOFSTEP]
apply (isLimitMapConeBinaryFanEquiv _ _ _).symm _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsLimit (BinaryFan.mk (G.map prod.fst) (G.map prod.snd))
[PROOFSTEP]
refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (pair (G.obj X) (G.obj Y))) ?_
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsIso (IsLimit.lift (limit.isLimit (pair (G.obj X) (G.obj Y))) (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)))
[PROOFSTEP]
apply i
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ IsIso (prodComparison G X Y)
[PROOFSTEP]
rw [← PreservesLimitPair.iso_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ IsIso (PreservesLimitPair.iso G X Y).hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
⊢ ∀ (j : Discrete WalkingPair),
    NatTrans.app
          ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).ι j ≫
        (Iso.refl
            ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj
                (G.mapCocone (BinaryCofan.mk f g))).pt).hom =
      NatTrans.app (BinaryCofan.mk (G.map f) (G.map g)).ι j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case mk.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
⊢ NatTrans.app ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).ι
        { as := WalkingPair.left } ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj
              (G.mapCocone (BinaryCofan.mk f g))).pt).hom =
    NatTrans.app (BinaryCofan.mk (G.map f) (G.map g)).ι { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
⊢ NatTrans.app ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).ι
        { as := WalkingPair.right } ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj
              (G.mapCocone (BinaryCofan.mk f g))).pt).hom =
    NatTrans.app (BinaryCofan.mk (G.map f) (G.map g)).ι { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ PreservesColimit (pair X Y) G
[PROOFSTEP]
apply preservesColimitOfPreservesColimitCocone (coprodIsCoprod X Y)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsColimit (G.mapCocone (BinaryCofan.mk coprod.inl coprod.inr))
[PROOFSTEP]
apply (isColimitMapCoconeBinaryCofanEquiv _ _ _).symm _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsColimit (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr))
[PROOFSTEP]
refine @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (pair (G.obj X) (G.obj Y))) ?_
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsIso
    (IsColimit.desc (colimit.isColimit (pair (G.obj X) (G.obj Y)))
      (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)))
[PROOFSTEP]
apply i
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝² : HasBinaryCoproduct X Y
inst✝¹ : HasBinaryCoproduct (G.obj X) (G.obj Y)
inst✝ : PreservesColimit (pair X Y) G
⊢ IsIso (coprodComparison G X Y)
[PROOFSTEP]
rw [← PreservesColimitPair.iso_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝² : HasBinaryCoproduct X Y
inst✝¹ : HasBinaryCoproduct (G.obj X) (G.obj Y)
inst✝ : PreservesColimit (pair X Y) G
⊢ IsIso (PreservesColimitPair.iso G X Y).hom
[PROOFSTEP]
infer_instance
