[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj (mk (NatTrans.app c.π (Classical.arbitrary J) ≫ (F.obj (Classical.arbitrary J)).hom))).map
          f ≫
        (fun j => homMk (NatTrans.app c.π j)) Y =
      (fun j => homMk (NatTrans.app c.π j)) X ≫ F.map f
[PROOFSTEP]
intro X Y f
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (mk (NatTrans.app c.π (Classical.arbitrary J) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
      (fun j => homMk (NatTrans.app c.π j)) Y =
    (fun j => homMk (NatTrans.app c.π j)) X ≫ F.map f
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case left
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
X Y : J
f : X ⟶ Y
⊢ (((Functor.const J).obj (mk (NatTrans.app c.π (Classical.arbitrary J) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
        (fun j => homMk (NatTrans.app c.π j)) Y).left =
    ((fun j => homMk (NatTrans.app c.π j)) X ≫ F.map f).left
[PROOFSTEP]
simpa using (c.w f).symm
[GOAL]
case right
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
X Y : J
f : X ⟶ Y
⊢ (((Functor.const J).obj (mk (NatTrans.app c.π (Classical.arbitrary J) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
        (fun j => homMk (NatTrans.app c.π j)) Y).right =
    ((fun j => homMk (NatTrans.app c.π j)) X ≫ F.map f).right
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
⊢ (forget B).mapCone (raiseCone c) = c
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ NatTrans.app (raiseCone c).π j = NatTrans.app s.π j
⊢ m = (fun s => homMk (IsLimit.lift t ((forget B).mapCone s))) s
[PROOFSTEP]
ext1
[GOAL]
case h
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ NatTrans.app (raiseCone c).π j = NatTrans.app s.π j
⊢ m.left = ((fun s => homMk (IsLimit.lift t ((forget B).mapCone s))) s).left
[PROOFSTEP]
apply t.hom_ext
[GOAL]
case h
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ NatTrans.app (raiseCone c).π j = NatTrans.app s.π j
⊢ ∀ (j : J),
    m.left ≫ NatTrans.app c.π j = ((fun s => homMk (IsLimit.lift t ((forget B).mapCone s))) s).left ≫ NatTrans.app c.π j
[PROOFSTEP]
intro j
[GOAL]
case h
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ NatTrans.app (raiseCone c).π j = NatTrans.app s.π j
j : J
⊢ m.left ≫ NatTrans.app c.π j = ((fun s => homMk (IsLimit.lift t ((forget B).mapCone s))) s).left ≫ NatTrans.app c.π j
[PROOFSTEP]
simp [← K j]


[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F = pullback.snd
[PROOFSTEP]
convert
  (eq_whisker pullback.condition Limits.prod.fst : (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) = _)
[GOAL]
case h.e'_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F =
    (pullback.fst ≫ prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left)) ≫ prod.fst
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullback.snd =
    (pullback.snd ≫ prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫ prod.fst
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F ≫ F.map WalkingParallelPairHom.left = pullbackFst F ≫ F.map WalkingParallelPairHom.right
[PROOFSTEP]
conv_rhs => rw [pullbackFst_eq_pullback_snd]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
| pullbackFst F ≫ F.map WalkingParallelPairHom.right
[PROOFSTEP]
rw [pullbackFst_eq_pullback_snd]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
| pullbackFst F ≫ F.map WalkingParallelPairHom.right
[PROOFSTEP]
rw [pullbackFst_eq_pullback_snd]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
| pullbackFst F ≫ F.map WalkingParallelPairHom.right
[PROOFSTEP]
rw [pullbackFst_eq_pullback_snd]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F ≫ F.map WalkingParallelPairHom.left = pullback.snd ≫ F.map WalkingParallelPairHom.right
[PROOFSTEP]
convert
  (eq_whisker pullback.condition Limits.prod.snd : (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.one) = _) using
  1
[GOAL]
case h.e'_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F ≫ F.map WalkingParallelPairHom.left =
    (pullback.fst ≫ prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left)) ≫ prod.snd
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullback.snd ≫ F.map WalkingParallelPairHom.right =
    (pullback.snd ≫ prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫ prod.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ (s : Cone F) → s.pt ⟶ (equalizerCone F).pt
[PROOFSTEP]
intro c
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
⊢ c.pt ⟶ (equalizerCone F).pt
[PROOFSTEP]
apply pullback.lift (c.π.app _) (c.π.app _)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
⊢ NatTrans.app c.π WalkingParallelPair.zero ≫
      prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left) =
    NatTrans.app c.π WalkingParallelPair.zero ≫
      prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
⊢ (NatTrans.app c.π WalkingParallelPair.zero ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left)) ≫
      prod.fst =
    (NatTrans.app c.π WalkingParallelPair.zero ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      prod.fst
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
⊢ (NatTrans.app c.π WalkingParallelPair.zero ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left)) ≫
      prod.snd =
    (NatTrans.app c.π WalkingParallelPair.zero ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      prod.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ ∀ (s : Cone F) (j : WalkingParallelPair),
    pullback.lift (NatTrans.app s.π WalkingParallelPair.zero) (NatTrans.app s.π WalkingParallelPair.zero)
          (_ :
            NatTrans.app s.π WalkingParallelPair.zero ≫
                prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left) =
              NatTrans.app s.π WalkingParallelPair.zero ≫
                prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        NatTrans.app (equalizerCone F).π j =
      NatTrans.app s.π j
[PROOFSTEP]
rintro c (_ | _)
[GOAL]
case zero
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
⊢ pullback.lift (NatTrans.app c.π WalkingParallelPair.zero) (NatTrans.app c.π WalkingParallelPair.zero)
        (_ :
          NatTrans.app c.π WalkingParallelPair.zero ≫
              prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left) =
            NatTrans.app c.π WalkingParallelPair.zero ≫
              prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      NatTrans.app (equalizerCone F).π WalkingParallelPair.zero =
    NatTrans.app c.π WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
case one
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
⊢ pullback.lift (NatTrans.app c.π WalkingParallelPair.zero) (NatTrans.app c.π WalkingParallelPair.zero)
        (_ :
          NatTrans.app c.π WalkingParallelPair.zero ≫
              prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left) =
            NatTrans.app c.π WalkingParallelPair.zero ≫
              prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      NatTrans.app (equalizerCone F).π WalkingParallelPair.one =
    NatTrans.app c.π WalkingParallelPair.one
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ ∀ (s : Cone F) (m : s.pt ⟶ (equalizerCone F).pt),
    (∀ (j : WalkingParallelPair), m ≫ NatTrans.app (equalizerCone F).π j = NatTrans.app s.π j) →
      m =
        pullback.lift (NatTrans.app s.π WalkingParallelPair.zero) (NatTrans.app s.π WalkingParallelPair.zero)
          (_ :
            NatTrans.app s.π WalkingParallelPair.zero ≫
                prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left) =
              NatTrans.app s.π WalkingParallelPair.zero ≫
                prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))
[PROOFSTEP]
intro c _ J
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
m✝ : c.pt ⟶ (equalizerCone F).pt
J : ∀ (j : WalkingParallelPair), m✝ ≫ NatTrans.app (equalizerCone F).π j = NatTrans.app c.π j
⊢ m✝ =
    pullback.lift (NatTrans.app c.π WalkingParallelPair.zero) (NatTrans.app c.π WalkingParallelPair.zero)
      (_ :
        NatTrans.app c.π WalkingParallelPair.zero ≫
            prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left) =
          NatTrans.app c.π WalkingParallelPair.zero ≫
            prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))
[PROOFSTEP]
have J0 := J WalkingParallelPair.zero
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
m✝ : c.pt ⟶ (equalizerCone F).pt
J : ∀ (j : WalkingParallelPair), m✝ ≫ NatTrans.app (equalizerCone F).π j = NatTrans.app c.π j
J0 : m✝ ≫ NatTrans.app (equalizerCone F).π WalkingParallelPair.zero = NatTrans.app c.π WalkingParallelPair.zero
⊢ m✝ =
    pullback.lift (NatTrans.app c.π WalkingParallelPair.zero) (NatTrans.app c.π WalkingParallelPair.zero)
      (_ :
        NatTrans.app c.π WalkingParallelPair.zero ≫
            prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left) =
          NatTrans.app c.π WalkingParallelPair.zero ≫
            prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))
[PROOFSTEP]
simp at J0
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
m✝ : c.pt ⟶ (equalizerCone F).pt
J : ∀ (j : WalkingParallelPair), m✝ ≫ NatTrans.app (equalizerCone F).π j = NatTrans.app c.π j
J0 : m✝ ≫ pullbackFst F = NatTrans.app c.π WalkingParallelPair.zero
⊢ m✝ =
    pullback.lift (NatTrans.app c.π WalkingParallelPair.zero) (NatTrans.app c.π WalkingParallelPair.zero)
      (_ :
        NatTrans.app c.π WalkingParallelPair.zero ≫
            prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left) =
          NatTrans.app c.π WalkingParallelPair.zero ≫
            prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))
[PROOFSTEP]
apply pullback.hom_ext
[GOAL]
case h₀
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
m✝ : c.pt ⟶ (equalizerCone F).pt
J : ∀ (j : WalkingParallelPair), m✝ ≫ NatTrans.app (equalizerCone F).π j = NatTrans.app c.π j
J0 : m✝ ≫ pullbackFst F = NatTrans.app c.π WalkingParallelPair.zero
⊢ m✝ ≫ pullback.fst =
    pullback.lift (NatTrans.app c.π WalkingParallelPair.zero) (NatTrans.app c.π WalkingParallelPair.zero)
        (_ :
          NatTrans.app c.π WalkingParallelPair.zero ≫
              prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left) =
            NatTrans.app c.π WalkingParallelPair.zero ≫
              prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      pullback.fst
[PROOFSTEP]
rwa [limit.lift_π]
[GOAL]
case h₁
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
m✝ : c.pt ⟶ (equalizerCone F).pt
J : ∀ (j : WalkingParallelPair), m✝ ≫ NatTrans.app (equalizerCone F).π j = NatTrans.app c.π j
J0 : m✝ ≫ pullbackFst F = NatTrans.app c.π WalkingParallelPair.zero
⊢ m✝ ≫ pullback.snd =
    pullback.lift (NatTrans.app c.π WalkingParallelPair.zero) (NatTrans.app c.π WalkingParallelPair.zero)
        (_ :
          NatTrans.app c.π WalkingParallelPair.zero ≫
              prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left) =
            NatTrans.app c.π WalkingParallelPair.zero ≫
              prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      pullback.snd
[PROOFSTEP]
erw [limit.lift_π, ← J0, pullbackFst_eq_pullback_snd]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ c.pt ⟶ (G.mapCone (equalizerCone K)).pt
[PROOFSTEP]
refine' pullback.lift ?_ ?_ ?_ ≫ (PreservesPullback.iso _ _ _).inv
[GOAL]
case refine'_1
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ c.pt ⟶ G.obj (K.obj WalkingParallelPair.zero)
[PROOFSTEP]
exact c.π.app WalkingParallelPair.zero
[GOAL]
case refine'_2
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ c.pt ⟶ G.obj (K.obj WalkingParallelPair.zero)
[PROOFSTEP]
exact c.π.app WalkingParallelPair.zero
[GOAL]
case refine'_3
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ NatTrans.app c.π WalkingParallelPair.zero ≫
      G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)) =
    NatTrans.app c.π WalkingParallelPair.zero ≫
      G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))
[PROOFSTEP]
apply (mapIsLimitOfPreservesOfIsLimit G _ _ (prodIsProd _ _)).hom_ext
[GOAL]
case refine'_3
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ ∀ (j : Discrete WalkingPair),
    (NatTrans.app c.π WalkingParallelPair.zero ≫
          G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))) ≫
        NatTrans.app (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π j =
      (NatTrans.app c.π WalkingParallelPair.zero ≫
          G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
        NatTrans.app (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case refine'_3.mk.left
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (NatTrans.app c.π WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))) ≫
      NatTrans.app (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π { as := WalkingPair.left } =
    (NatTrans.app c.π WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
      NatTrans.app (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π { as := WalkingPair.left }
[PROOFSTEP]
simp only [Category.assoc, ← G.map_comp, prod.lift_fst, BinaryFan.π_app_left, BinaryFan.mk_fst]
[GOAL]
case refine'_3.mk.right
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (NatTrans.app c.π WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))) ≫
      NatTrans.app (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π { as := WalkingPair.right } =
    (NatTrans.app c.π WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
      NatTrans.app (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π { as := WalkingPair.right }
[PROOFSTEP]
simp only [BinaryFan.π_app_right, BinaryFan.mk_snd, Category.assoc, ← G.map_comp, prod.lift_snd]
[GOAL]
case refine'_3.mk.right
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ NatTrans.app c.π WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.left) =
    NatTrans.app c.π WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.right)
[PROOFSTEP]
exact (c.π.naturality WalkingParallelPairHom.left).symm.trans (c.π.naturality WalkingParallelPairHom.right)
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
j : WalkingParallelPair
⊢ (fun c =>
          pullback.lift (NatTrans.app c.π WalkingParallelPair.zero) (NatTrans.app c.π WalkingParallelPair.zero)
              (_ :
                NatTrans.app c.π WalkingParallelPair.zero ≫
                    G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)) =
                  NatTrans.app c.π WalkingParallelPair.zero ≫
                    G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
            (PreservesPullback.iso G
                (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
                (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv)
        c ≫
      NatTrans.app (G.mapCone (equalizerCone K)).π j =
    NatTrans.app c.π j
[PROOFSTEP]
rcases j with (_ | _)
[GOAL]
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (fun c =>
          pullback.lift (NatTrans.app c.π WalkingParallelPair.zero) (NatTrans.app c.π WalkingParallelPair.zero)
              (_ :
                NatTrans.app c.π WalkingParallelPair.zero ≫
                    G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)) =
                  NatTrans.app c.π WalkingParallelPair.zero ≫
                    G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
            (PreservesPullback.iso G
                (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
                (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv)
        c ≫
      NatTrans.app (G.mapCone (equalizerCone K)).π WalkingParallelPair.zero =
    NatTrans.app c.π WalkingParallelPair.zero
[PROOFSTEP]
simp only [Category.comp_id, PreservesPullback.iso_inv_fst, Cone.ofFork_π, G.map_comp,
  PreservesPullback.iso_inv_fst_assoc, Functor.mapCone_π_app, eqToHom_refl, Category.assoc, Fork.ofι_π_app,
  pullback.lift_fst, pullback.lift_fst_assoc]
[GOAL]
case one
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (fun c =>
          pullback.lift (NatTrans.app c.π WalkingParallelPair.zero) (NatTrans.app c.π WalkingParallelPair.zero)
              (_ :
                NatTrans.app c.π WalkingParallelPair.zero ≫
                    G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)) =
                  NatTrans.app c.π WalkingParallelPair.zero ≫
                    G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
            (PreservesPullback.iso G
                (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
                (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv)
        c ≫
      NatTrans.app (G.mapCone (equalizerCone K)).π WalkingParallelPair.one =
    NatTrans.app c.π WalkingParallelPair.one
[PROOFSTEP]
simp only [Category.comp_id, PreservesPullback.iso_inv_fst, Cone.ofFork_π, G.map_comp,
  PreservesPullback.iso_inv_fst_assoc, Functor.mapCone_π_app, eqToHom_refl, Category.assoc, Fork.ofι_π_app,
  pullback.lift_fst, pullback.lift_fst_assoc]
[GOAL]
case one
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ NatTrans.app c.π WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.left) =
    NatTrans.app c.π WalkingParallelPair.one
[PROOFSTEP]
exact (c.π.naturality WalkingParallelPairHom.left).symm.trans (Category.id_comp _)
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
s : Cone (K ⋙ G)
m : s.pt ⟶ (G.mapCone (equalizerCone K)).pt
h : ∀ (j : WalkingParallelPair), m ≫ NatTrans.app (G.mapCone (equalizerCone K)).π j = NatTrans.app s.π j
⊢ m =
    (fun c =>
        pullback.lift (NatTrans.app c.π WalkingParallelPair.zero) (NatTrans.app c.π WalkingParallelPair.zero)
            (_ :
              NatTrans.app c.π WalkingParallelPair.zero ≫
                  G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)) =
                NatTrans.app c.π WalkingParallelPair.zero ≫
                  G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
          (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
              (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv)
      s
[PROOFSTEP]
rw [Iso.eq_comp_inv]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
s : Cone (K ⋙ G)
m : s.pt ⟶ (G.mapCone (equalizerCone K)).pt
h : ∀ (j : WalkingParallelPair), m ≫ NatTrans.app (G.mapCone (equalizerCone K)).π j = NatTrans.app s.π j
⊢ m ≫
      (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).hom =
    pullback.lift (NatTrans.app s.π WalkingParallelPair.zero) (NatTrans.app s.π WalkingParallelPair.zero)
      (_ :
        NatTrans.app s.π WalkingParallelPair.zero ≫
            G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)) =
          NatTrans.app s.π WalkingParallelPair.zero ≫
            G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))
[PROOFSTEP]
have := h WalkingParallelPair.zero
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
s : Cone (K ⋙ G)
m : s.pt ⟶ (G.mapCone (equalizerCone K)).pt
h : ∀ (j : WalkingParallelPair), m ≫ NatTrans.app (G.mapCone (equalizerCone K)).π j = NatTrans.app s.π j
this :
  m ≫ NatTrans.app (G.mapCone (equalizerCone K)).π WalkingParallelPair.zero = NatTrans.app s.π WalkingParallelPair.zero
⊢ m ≫
      (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).hom =
    pullback.lift (NatTrans.app s.π WalkingParallelPair.zero) (NatTrans.app s.π WalkingParallelPair.zero)
      (_ :
        NatTrans.app s.π WalkingParallelPair.zero ≫
            G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)) =
          NatTrans.app s.π WalkingParallelPair.zero ≫
            G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))
[PROOFSTEP]
dsimp [equalizerCone] at this
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
s : Cone (K ⋙ G)
m : s.pt ⟶ (G.mapCone (equalizerCone K)).pt
h : ∀ (j : WalkingParallelPair), m ≫ NatTrans.app (G.mapCone (equalizerCone K)).π j = NatTrans.app s.π j
this : m ≫ G.map (pullbackFst K ≫ 𝟙 (K.obj WalkingParallelPair.zero)) = NatTrans.app s.π WalkingParallelPair.zero
⊢ m ≫
      (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).hom =
    pullback.lift (NatTrans.app s.π WalkingParallelPair.zero) (NatTrans.app s.π WalkingParallelPair.zero)
      (_ :
        NatTrans.app s.π WalkingParallelPair.zero ≫
            G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)) =
          NatTrans.app s.π WalkingParallelPair.zero ≫
            G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
s : Cone (K ⋙ G)
m : s.pt ⟶ (G.mapCone (equalizerCone K)).pt
h : ∀ (j : WalkingParallelPair), m ≫ NatTrans.app (G.mapCone (equalizerCone K)).π j = NatTrans.app s.π j
this : m ≫ G.map (pullbackFst K ≫ 𝟙 (K.obj WalkingParallelPair.zero)) = NatTrans.app s.π WalkingParallelPair.zero
⊢ (m ≫
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).hom) ≫
      pullback.fst =
    pullback.lift (NatTrans.app s.π WalkingParallelPair.zero) (NatTrans.app s.π WalkingParallelPair.zero)
        (_ :
          NatTrans.app s.π WalkingParallelPair.zero ≫
              G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)) =
            NatTrans.app s.π WalkingParallelPair.zero ≫
              G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
      pullback.fst
[PROOFSTEP]
simp only [PreservesPullback.iso_hom_snd, Category.assoc, PreservesPullback.iso_hom_fst, pullback.lift_fst,
  pullback.lift_snd, Category.comp_id, ← pullbackFst_eq_pullback_snd, ← this]
[GOAL]
case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
s : Cone (K ⋙ G)
m : s.pt ⟶ (G.mapCone (equalizerCone K)).pt
h : ∀ (j : WalkingParallelPair), m ≫ NatTrans.app (G.mapCone (equalizerCone K)).π j = NatTrans.app s.π j
this : m ≫ G.map (pullbackFst K ≫ 𝟙 (K.obj WalkingParallelPair.zero)) = NatTrans.app s.π WalkingParallelPair.zero
⊢ (m ≫
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).hom) ≫
      pullback.snd =
    pullback.lift (NatTrans.app s.π WalkingParallelPair.zero) (NatTrans.app s.π WalkingParallelPair.zero)
        (_ :
          NatTrans.app s.π WalkingParallelPair.zero ≫
              G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)) =
            NatTrans.app s.π WalkingParallelPair.zero ≫
              G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
      pullback.snd
[PROOFSTEP]
simp only [PreservesPullback.iso_hom_snd, Category.assoc, PreservesPullback.iso_hom_fst, pullback.lift_fst,
  pullback.lift_snd, Category.comp_id, ← pullbackFst_eq_pullback_snd, ← this]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ pushoutInl F = pushout.inr
[PROOFSTEP]
convert (whisker_eq Limits.coprod.inl pushout.condition : (_ : F.obj _ ⟶ constructCoequalizer _) = _)
[GOAL]
case h.e'_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ pushoutInl F =
    coprod.inl ≫ coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫ pushout.inl
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ pushout.inr =
    coprod.inl ≫ coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫ pushout.inr
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ F.map WalkingParallelPairHom.left ≫ pushoutInl F = F.map WalkingParallelPairHom.right ≫ pushoutInl F
[PROOFSTEP]
conv_rhs => rw [pushoutInl_eq_pushout_inr]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
| F.map WalkingParallelPairHom.right ≫ pushoutInl F
[PROOFSTEP]
rw [pushoutInl_eq_pushout_inr]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
| F.map WalkingParallelPairHom.right ≫ pushoutInl F
[PROOFSTEP]
rw [pushoutInl_eq_pushout_inr]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
| F.map WalkingParallelPairHom.right ≫ pushoutInl F
[PROOFSTEP]
rw [pushoutInl_eq_pushout_inr]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ F.map WalkingParallelPairHom.left ≫ pushoutInl F = F.map WalkingParallelPairHom.right ≫ pushout.inr
[PROOFSTEP]
convert (whisker_eq Limits.coprod.inr pushout.condition : (_ : F.obj _ ⟶ constructCoequalizer _) = _) using 1
[GOAL]
case h.e'_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ F.map WalkingParallelPairHom.left ≫ pushoutInl F =
    coprod.inr ≫ coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫ pushout.inl
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ F.map WalkingParallelPairHom.right ≫ pushout.inr =
    coprod.inr ≫ coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫ pushout.inr
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ (s : Cocone F) → (coequalizerCocone F).pt ⟶ s.pt
[PROOFSTEP]
intro c
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
⊢ (coequalizerCocone F).pt ⟶ c.pt
[PROOFSTEP]
apply pushout.desc (c.ι.app _) (c.ι.app _)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
⊢ coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
      NatTrans.app c.ι WalkingParallelPair.one =
    coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
      NatTrans.app c.ι WalkingParallelPair.one
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
⊢ coprod.inl ≫
      coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
        NatTrans.app c.ι WalkingParallelPair.one =
    coprod.inl ≫
      coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
        NatTrans.app c.ι WalkingParallelPair.one
[PROOFSTEP]
simp
[GOAL]
case h₂
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
⊢ coprod.inr ≫
      coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
        NatTrans.app c.ι WalkingParallelPair.one =
    coprod.inr ≫
      coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
        NatTrans.app c.ι WalkingParallelPair.one
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ ∀ (s : Cocone F) (j : WalkingParallelPair),
    NatTrans.app (coequalizerCocone F).ι j ≫
        pushout.desc (NatTrans.app s.ι WalkingParallelPair.one) (NatTrans.app s.ι WalkingParallelPair.one)
          (_ :
            coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
                NatTrans.app s.ι WalkingParallelPair.one =
              coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
                NatTrans.app s.ι WalkingParallelPair.one) =
      NatTrans.app s.ι j
[PROOFSTEP]
rintro c (_ | _)
[GOAL]
case zero
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
⊢ NatTrans.app (coequalizerCocone F).ι WalkingParallelPair.zero ≫
      pushout.desc (NatTrans.app c.ι WalkingParallelPair.one) (NatTrans.app c.ι WalkingParallelPair.one)
        (_ :
          coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
              NatTrans.app c.ι WalkingParallelPair.one =
            coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
              NatTrans.app c.ι WalkingParallelPair.one) =
    NatTrans.app c.ι WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
case one
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
⊢ NatTrans.app (coequalizerCocone F).ι WalkingParallelPair.one ≫
      pushout.desc (NatTrans.app c.ι WalkingParallelPair.one) (NatTrans.app c.ι WalkingParallelPair.one)
        (_ :
          coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
              NatTrans.app c.ι WalkingParallelPair.one =
            coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
              NatTrans.app c.ι WalkingParallelPair.one) =
    NatTrans.app c.ι WalkingParallelPair.one
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ ∀ (s : Cocone F) (m : (coequalizerCocone F).pt ⟶ s.pt),
    (∀ (j : WalkingParallelPair), NatTrans.app (coequalizerCocone F).ι j ≫ m = NatTrans.app s.ι j) →
      m =
        pushout.desc (NatTrans.app s.ι WalkingParallelPair.one) (NatTrans.app s.ι WalkingParallelPair.one)
          (_ :
            coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
                NatTrans.app s.ι WalkingParallelPair.one =
              coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
                NatTrans.app s.ι WalkingParallelPair.one)
[PROOFSTEP]
intro c m J
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), NatTrans.app (coequalizerCocone F).ι j ≫ m = NatTrans.app c.ι j
⊢ m =
    pushout.desc (NatTrans.app c.ι WalkingParallelPair.one) (NatTrans.app c.ι WalkingParallelPair.one)
      (_ :
        coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
            NatTrans.app c.ι WalkingParallelPair.one =
          coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
            NatTrans.app c.ι WalkingParallelPair.one)
[PROOFSTEP]
have J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one := by simpa using J WalkingParallelPair.one
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), NatTrans.app (coequalizerCocone F).ι j ≫ m = NatTrans.app c.ι j
⊢ pushoutInl F ≫ m = NatTrans.app c.ι WalkingParallelPair.one
[PROOFSTEP]
simpa using J WalkingParallelPair.one
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), NatTrans.app (coequalizerCocone F).ι j ≫ m = NatTrans.app c.ι j
J1 : pushoutInl F ≫ m = NatTrans.app c.ι WalkingParallelPair.one
⊢ m =
    pushout.desc (NatTrans.app c.ι WalkingParallelPair.one) (NatTrans.app c.ι WalkingParallelPair.one)
      (_ :
        coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
            NatTrans.app c.ι WalkingParallelPair.one =
          coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
            NatTrans.app c.ι WalkingParallelPair.one)
[PROOFSTEP]
apply pushout.hom_ext
[GOAL]
case h₀
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), NatTrans.app (coequalizerCocone F).ι j ≫ m = NatTrans.app c.ι j
J1 : pushoutInl F ≫ m = NatTrans.app c.ι WalkingParallelPair.one
⊢ pushout.inl ≫ m =
    pushout.inl ≫
      pushout.desc (NatTrans.app c.ι WalkingParallelPair.one) (NatTrans.app c.ι WalkingParallelPair.one)
        (_ :
          coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
              NatTrans.app c.ι WalkingParallelPair.one =
            coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
              NatTrans.app c.ι WalkingParallelPair.one)
[PROOFSTEP]
rw [colimit.ι_desc]
[GOAL]
case h₀
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), NatTrans.app (coequalizerCocone F).ι j ≫ m = NatTrans.app c.ι j
J1 : pushoutInl F ≫ m = NatTrans.app c.ι WalkingParallelPair.one
⊢ pushout.inl ≫ m =
    NatTrans.app
      (PushoutCocone.mk (NatTrans.app c.ι WalkingParallelPair.one) (NatTrans.app c.ι WalkingParallelPair.one)
          (_ :
            coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
                NatTrans.app c.ι WalkingParallelPair.one =
              coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
                NatTrans.app c.ι WalkingParallelPair.one)).ι
      WalkingSpan.left
[PROOFSTEP]
exact J1
[GOAL]
case h₁
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), NatTrans.app (coequalizerCocone F).ι j ≫ m = NatTrans.app c.ι j
J1 : pushoutInl F ≫ m = NatTrans.app c.ι WalkingParallelPair.one
⊢ pushout.inr ≫ m =
    pushout.inr ≫
      pushout.desc (NatTrans.app c.ι WalkingParallelPair.one) (NatTrans.app c.ι WalkingParallelPair.one)
        (_ :
          coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
              NatTrans.app c.ι WalkingParallelPair.one =
            coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
              NatTrans.app c.ι WalkingParallelPair.one)
[PROOFSTEP]
rw [colimit.ι_desc, ← pushoutInl_eq_pushout_inr]
[GOAL]
case h₁
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), NatTrans.app (coequalizerCocone F).ι j ≫ m = NatTrans.app c.ι j
J1 : pushoutInl F ≫ m = NatTrans.app c.ι WalkingParallelPair.one
⊢ pushoutInl F ≫ m =
    NatTrans.app
      (PushoutCocone.mk (NatTrans.app c.ι WalkingParallelPair.one) (NatTrans.app c.ι WalkingParallelPair.one)
          (_ :
            coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
                NatTrans.app c.ι WalkingParallelPair.one =
              coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
                NatTrans.app c.ι WalkingParallelPair.one)).ι
      WalkingSpan.right
[PROOFSTEP]
exact J1
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ (G.mapCocone (coequalizerCocone K)).pt ⟶ c.pt
[PROOFSTEP]
refine' (PreservesPushout.iso _ _ _).inv ≫ pushout.desc _ _ _
[GOAL]
case refine'_1
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ G.obj (K.obj WalkingParallelPair.one) ⟶ c.pt
[PROOFSTEP]
exact c.ι.app WalkingParallelPair.one
[GOAL]
case refine'_2
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ G.obj (K.obj WalkingParallelPair.one) ⟶ c.pt
[PROOFSTEP]
exact c.ι.app WalkingParallelPair.one
[GOAL]
case refine'_3
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
      NatTrans.app c.ι WalkingParallelPair.one =
    G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
      NatTrans.app c.ι WalkingParallelPair.one
[PROOFSTEP]
apply (mapIsColimitOfPreservesOfIsColimit G _ _ (coprodIsCoprod _ _)).hom_ext
[GOAL]
case refine'_3
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ ∀ (j : Discrete WalkingPair),
    NatTrans.app (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι j ≫
        G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
          NatTrans.app c.ι WalkingParallelPair.one =
      NatTrans.app (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι j ≫
        G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
          NatTrans.app c.ι WalkingParallelPair.one
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case refine'_3.mk.left
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ NatTrans.app (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι { as := WalkingPair.left } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
        NatTrans.app c.ι WalkingParallelPair.one =
    NatTrans.app (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι { as := WalkingPair.left } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        NatTrans.app c.ι WalkingParallelPair.one
[PROOFSTEP]
simp only [BinaryCofan.ι_app_left, BinaryCofan.mk_inl, Category.assoc, ← G.map_comp_assoc, coprod.inl_desc]
[GOAL]
case refine'_3.mk.right
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ NatTrans.app (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι { as := WalkingPair.right } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
        NatTrans.app c.ι WalkingParallelPair.one =
    NatTrans.app (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι { as := WalkingPair.right } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        NatTrans.app c.ι WalkingParallelPair.one
[PROOFSTEP]
simp only [BinaryCofan.ι_app_right, BinaryCofan.mk_inr, Category.assoc, ← G.map_comp_assoc, coprod.inr_desc]
[GOAL]
case refine'_3.mk.right
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ G.map (K.map WalkingParallelPairHom.left) ≫ NatTrans.app c.ι WalkingParallelPair.one =
    G.map (K.map WalkingParallelPairHom.right) ≫ NatTrans.app c.ι WalkingParallelPair.one
[PROOFSTEP]
exact (c.ι.naturality WalkingParallelPairHom.left).trans (c.ι.naturality WalkingParallelPairHom.right).symm
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
j : WalkingParallelPair
⊢ NatTrans.app (G.mapCocone (coequalizerCocone K)).ι j ≫
      (fun c =>
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
                (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).inv ≫
            pushout.desc (NatTrans.app c.ι WalkingParallelPair.one) (NatTrans.app c.ι WalkingParallelPair.one)
              (_ :
                G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
                    NatTrans.app c.ι WalkingParallelPair.one =
                  G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
                    NatTrans.app c.ι WalkingParallelPair.one))
        c =
    NatTrans.app c.ι j
[PROOFSTEP]
rcases j with (_ | _)
[GOAL]
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ NatTrans.app (G.mapCocone (coequalizerCocone K)).ι WalkingParallelPair.zero ≫
      (fun c =>
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
                (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).inv ≫
            pushout.desc (NatTrans.app c.ι WalkingParallelPair.one) (NatTrans.app c.ι WalkingParallelPair.one)
              (_ :
                G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
                    NatTrans.app c.ι WalkingParallelPair.one =
                  G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
                    NatTrans.app c.ι WalkingParallelPair.one))
        c =
    NatTrans.app c.ι WalkingParallelPair.zero
[PROOFSTEP]
simp only [Functor.mapCocone_ι_app, Cocone.ofCofork_ι, Category.id_comp, eqToHom_refl, Category.assoc, Functor.map_comp,
  Cofork.ofπ_ι_app, pushout.inl_desc, PreservesPushout.inl_iso_inv_assoc]
[GOAL]
case one
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ NatTrans.app (G.mapCocone (coequalizerCocone K)).ι WalkingParallelPair.one ≫
      (fun c =>
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
                (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).inv ≫
            pushout.desc (NatTrans.app c.ι WalkingParallelPair.one) (NatTrans.app c.ι WalkingParallelPair.one)
              (_ :
                G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
                    NatTrans.app c.ι WalkingParallelPair.one =
                  G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
                    NatTrans.app c.ι WalkingParallelPair.one))
        c =
    NatTrans.app c.ι WalkingParallelPair.one
[PROOFSTEP]
simp only [Functor.mapCocone_ι_app, Cocone.ofCofork_ι, Category.id_comp, eqToHom_refl, Category.assoc, Functor.map_comp,
  Cofork.ofπ_ι_app, pushout.inl_desc, PreservesPushout.inl_iso_inv_assoc]
[GOAL]
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ G.map (K.map WalkingParallelPairHom.left) ≫ NatTrans.app c.ι WalkingParallelPair.one =
    NatTrans.app c.ι WalkingParallelPair.zero
[PROOFSTEP]
exact (c.ι.naturality WalkingParallelPairHom.left).trans (Category.comp_id _)
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), NatTrans.app (G.mapCocone (coequalizerCocone K)).ι j ≫ m = NatTrans.app s.ι j
⊢ m =
    (fun c =>
        (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
              (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).inv ≫
          pushout.desc (NatTrans.app c.ι WalkingParallelPair.one) (NatTrans.app c.ι WalkingParallelPair.one)
            (_ :
              G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
                  NatTrans.app c.ι WalkingParallelPair.one =
                G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
                  NatTrans.app c.ι WalkingParallelPair.one))
      s
[PROOFSTEP]
rw [Iso.eq_inv_comp]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), NatTrans.app (G.mapCocone (coequalizerCocone K)).ι j ≫ m = NatTrans.app s.ι j
⊢ (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).hom ≫
      m =
    pushout.desc (NatTrans.app s.ι WalkingParallelPair.one) (NatTrans.app s.ι WalkingParallelPair.one)
      (_ :
        G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
            NatTrans.app s.ι WalkingParallelPair.one =
          G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
            NatTrans.app s.ι WalkingParallelPair.one)
[PROOFSTEP]
have := h WalkingParallelPair.one
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), NatTrans.app (G.mapCocone (coequalizerCocone K)).ι j ≫ m = NatTrans.app s.ι j
this :
  NatTrans.app (G.mapCocone (coequalizerCocone K)).ι WalkingParallelPair.one ≫ m =
    NatTrans.app s.ι WalkingParallelPair.one
⊢ (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).hom ≫
      m =
    pushout.desc (NatTrans.app s.ι WalkingParallelPair.one) (NatTrans.app s.ι WalkingParallelPair.one)
      (_ :
        G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
            NatTrans.app s.ι WalkingParallelPair.one =
          G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
            NatTrans.app s.ι WalkingParallelPair.one)
[PROOFSTEP]
dsimp [coequalizerCocone] at this
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), NatTrans.app (G.mapCocone (coequalizerCocone K)).ι j ≫ m = NatTrans.app s.ι j
this : G.map (𝟙 (K.obj WalkingParallelPair.one) ≫ pushoutInl K) ≫ m = NatTrans.app s.ι WalkingParallelPair.one
⊢ (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).hom ≫
      m =
    pushout.desc (NatTrans.app s.ι WalkingParallelPair.one) (NatTrans.app s.ι WalkingParallelPair.one)
      (_ :
        G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
            NatTrans.app s.ι WalkingParallelPair.one =
          G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
            NatTrans.app s.ι WalkingParallelPair.one)
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), NatTrans.app (G.mapCocone (coequalizerCocone K)).ι j ≫ m = NatTrans.app s.ι j
this : G.map (𝟙 (K.obj WalkingParallelPair.one) ≫ pushoutInl K) ≫ m = NatTrans.app s.ι WalkingParallelPair.one
⊢ pushout.inl ≫
      (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).hom ≫
        m =
    pushout.inl ≫
      pushout.desc (NatTrans.app s.ι WalkingParallelPair.one) (NatTrans.app s.ι WalkingParallelPair.one)
        (_ :
          G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
              NatTrans.app s.ι WalkingParallelPair.one =
            G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
              NatTrans.app s.ι WalkingParallelPair.one)
[PROOFSTEP]
simp only [PreservesPushout.inl_iso_hom_assoc, Category.id_comp, pushout.inl_desc, pushout.inr_desc,
  PreservesPushout.inr_iso_hom_assoc, ← pushoutInl_eq_pushout_inr, ← this]
[GOAL]
case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), NatTrans.app (G.mapCocone (coequalizerCocone K)).ι j ≫ m = NatTrans.app s.ι j
this : G.map (𝟙 (K.obj WalkingParallelPair.one) ≫ pushoutInl K) ≫ m = NatTrans.app s.ι WalkingParallelPair.one
⊢ pushout.inr ≫
      (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).hom ≫
        m =
    pushout.inr ≫
      pushout.desc (NatTrans.app s.ι WalkingParallelPair.one) (NatTrans.app s.ι WalkingParallelPair.one)
        (_ :
          G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
              NatTrans.app s.ι WalkingParallelPair.one =
            G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
              NatTrans.app s.ι WalkingParallelPair.one)
[PROOFSTEP]
simp only [PreservesPushout.inl_iso_hom_assoc, Category.id_comp, pushout.inl_desc, pushout.inr_desc,
  PreservesPushout.inr_iso_hom_assoc, ← pushoutInl_eq_pushout_inr, ← this]