[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc :
  IsLimit
    (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
      (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g))
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ m =
    (fun s =>
        IsLimit.lift hc
          (PullbackCone.mk (NatTrans.app s.π { as := WalkingPair.left }) (NatTrans.app s.π { as := WalkingPair.right })
            (_ : NatTrans.app s.π { as := WalkingPair.left } ≫ f = NatTrans.app s.π { as := WalkingPair.right } ≫ g)))
      s
[PROOFSTEP]
let c' :=
  PullbackCone.mk (m ≫ c.π.app ⟨WalkingPair.left⟩) (m ≫ c.π.app ⟨WalkingPair.right⟩ : _) (hX.hom_ext (_ ≫ f) (_ ≫ g))
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc :
  IsLimit
    (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
      (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g))
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left }) (m ≫ NatTrans.app c.π { as := WalkingPair.right })
    (_ : (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f = (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)
⊢ m =
    (fun s =>
        IsLimit.lift hc
          (PullbackCone.mk (NatTrans.app s.π { as := WalkingPair.left }) (NatTrans.app s.π { as := WalkingPair.right })
            (_ : NatTrans.app s.π { as := WalkingPair.left } ≫ f = NatTrans.app s.π { as := WalkingPair.right } ≫ g)))
      s
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc :
  IsLimit
    (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
      (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g))
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left }) (m ≫ NatTrans.app c.π { as := WalkingPair.right })
    (_ : (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f = (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)
⊢ m =
    IsLimit.lift hc
      (PullbackCone.mk (NatTrans.app s.π { as := WalkingPair.left }) (NatTrans.app s.π { as := WalkingPair.right })
        (_ : NatTrans.app s.π { as := WalkingPair.left } ≫ f = NatTrans.app s.π { as := WalkingPair.right } ≫ g))
[PROOFSTEP]
rw [← J, ← J]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc :
  IsLimit
    (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
      (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g))
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left }) (m ≫ NatTrans.app c.π { as := WalkingPair.right })
    (_ : (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f = (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)
⊢ m =
    IsLimit.lift hc
      (PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left })
        (m ≫ NatTrans.app c.π { as := WalkingPair.right })
        (_ :
          (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f =
            (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g))
[PROOFSTEP]
apply hc.hom_ext
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc :
  IsLimit
    (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
      (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g))
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left }) (m ≫ NatTrans.app c.π { as := WalkingPair.right })
    (_ : (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f = (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)
⊢ ∀ (j : WalkingCospan),
    m ≫
        NatTrans.app
          (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
              (_ :
                NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g)).π
          j =
      IsLimit.lift hc
          (PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left })
            (m ≫ NatTrans.app c.π { as := WalkingPair.right })
            (_ :
              (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f =
                (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)) ≫
        NatTrans.app
          (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
              (_ :
                NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g)).π
          j
[PROOFSTEP]
rintro (_ | (_ | _))
[GOAL]
case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc :
  IsLimit
    (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
      (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g))
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left }) (m ≫ NatTrans.app c.π { as := WalkingPair.right })
    (_ : (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f = (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)
⊢ m ≫
      NatTrans.app
        (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
            (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g)).π
        none =
    IsLimit.lift hc
        (PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left })
          (m ≫ NatTrans.app c.π { as := WalkingPair.right })
          (_ :
            (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f =
              (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)) ≫
      NatTrans.app
        (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
            (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g)).π
        none
[PROOFSTEP]
simp only [PullbackCone.mk_π_app_one, PullbackCone.mk_π_app]
[GOAL]
case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc :
  IsLimit
    (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
      (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g))
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left }) (m ≫ NatTrans.app c.π { as := WalkingPair.right })
    (_ : (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f = (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)
⊢ m ≫
      NatTrans.app
        (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
            (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g)).π
        (some WalkingPair.left) =
    IsLimit.lift hc
        (PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left })
          (m ≫ NatTrans.app c.π { as := WalkingPair.right })
          (_ :
            (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f =
              (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)) ≫
      NatTrans.app
        (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
            (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g)).π
        (some WalkingPair.left)
[PROOFSTEP]
simp only [PullbackCone.mk_π_app_one, PullbackCone.mk_π_app]
[GOAL]
case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc :
  IsLimit
    (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
      (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g))
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left }) (m ≫ NatTrans.app c.π { as := WalkingPair.right })
    (_ : (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f = (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)
⊢ m ≫
      NatTrans.app
        (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
            (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g)).π
        (some WalkingPair.right) =
    IsLimit.lift hc
        (PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left })
          (m ≫ NatTrans.app c.π { as := WalkingPair.right })
          (_ :
            (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f =
              (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)) ≫
      NatTrans.app
        (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
            (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g)).π
        (some WalkingPair.right)
[PROOFSTEP]
simp only [PullbackCone.mk_π_app_one, PullbackCone.mk_π_app]
[GOAL]
case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc :
  IsLimit
    (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
      (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g))
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left }) (m ≫ NatTrans.app c.π { as := WalkingPair.right })
    (_ : (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f = (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)
⊢ m ≫ NatTrans.app c.π { as := WalkingPair.left } ≫ f =
    IsLimit.lift hc
        (PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left })
          (m ≫ NatTrans.app c.π { as := WalkingPair.right })
          (_ :
            (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f =
              (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)) ≫
      NatTrans.app c.π { as := WalkingPair.left } ≫ f
case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc :
  IsLimit
    (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
      (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g))
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left }) (m ≫ NatTrans.app c.π { as := WalkingPair.right })
    (_ : (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f = (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)
⊢ m ≫ NatTrans.app c.π { as := WalkingPair.left } =
    IsLimit.lift hc
        (PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left })
          (m ≫ NatTrans.app c.π { as := WalkingPair.right })
          (_ :
            (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f =
              (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)) ≫
      NatTrans.app c.π { as := WalkingPair.left }
case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc :
  IsLimit
    (PullbackCone.mk (NatTrans.app c.π { as := WalkingPair.left }) (NatTrans.app c.π { as := WalkingPair.right })
      (_ : NatTrans.app c.π { as := WalkingPair.left } ≫ f = NatTrans.app c.π { as := WalkingPair.right } ≫ g))
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left }) (m ≫ NatTrans.app c.π { as := WalkingPair.right })
    (_ : (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f = (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)
⊢ m ≫ NatTrans.app c.π { as := WalkingPair.right } =
    IsLimit.lift hc
        (PullbackCone.mk (m ≫ NatTrans.app c.π { as := WalkingPair.left })
          (m ≫ NatTrans.app c.π { as := WalkingPair.right })
          (_ :
            (m ≫ NatTrans.app c.π { as := WalkingPair.left }) ≫ f =
              (m ≫ NatTrans.app c.π { as := WalkingPair.right }) ≫ g)) ≫
      NatTrans.app c.π { as := WalkingPair.right }
[PROOFSTEP]
exacts [(Category.assoc _ _ _).symm.trans (hc.fac_assoc c' WalkingCospan.left f).symm,
  (hc.fac c' WalkingCospan.left).symm, (hc.fac c' WalkingCospan.right).symm]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (PullbackCone.mk h k (_ : h ≫ f = k ≫ g))
⊢ IsLimit (BinaryFan.mk h k)
[PROOFSTEP]
apply isBinaryProductOfIsTerminalIsPullback _ _ H₁
[GOAL]
case hc
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (PullbackCone.mk h k (_ : h ≫ f = k ≫ g))
⊢ IsLimit
    (PullbackCone.mk (NatTrans.app (BinaryFan.mk h k).π { as := WalkingPair.left })
      (NatTrans.app (BinaryFan.mk h k).π { as := WalkingPair.right })
      (_ :
        NatTrans.app (BinaryFan.mk h k).π { as := WalkingPair.left } ≫ ?f =
          NatTrans.app (BinaryFan.mk h k).π { as := WalkingPair.right } ≫ ?g))
case f
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (PullbackCone.mk h k (_ : h ≫ f = k ≫ g))
⊢ (pair X Y).obj { as := WalkingPair.left } ⟶ Z
case g
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (PullbackCone.mk h k (_ : h ≫ f = k ≫ g))
⊢ (pair X Y).obj { as := WalkingPair.right } ⟶ Z
[PROOFSTEP]
exact H₂
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
⊢ IsLimit (PullbackCone.mk h k (_ : h ≫ f = k ≫ g))
[PROOFSTEP]
apply PullbackCone.isLimitAux'
[GOAL]
case create
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
⊢ (s : PullbackCone f g) →
    { l //
      l ≫ PullbackCone.fst (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.fst s ∧
        l ≫ PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.snd s ∧
          ∀ {m : s.pt ⟶ (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)).pt},
            m ≫ PullbackCone.fst (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.fst s →
              m ≫ PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.snd s → m = l }
[PROOFSTEP]
intro s
[GOAL]
case create
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
⊢ { l //
    l ≫ PullbackCone.fst (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.fst s ∧
      l ≫ PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.snd s ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)).pt},
          m ≫ PullbackCone.fst (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.fst s →
            m ≫ PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.snd s → m = l }
[PROOFSTEP]
use H₂.lift (BinaryFan.mk s.fst s.snd)
[GOAL]
case property
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
⊢ IsLimit.lift H₂ (BinaryFan.mk (PullbackCone.fst s) (PullbackCone.snd s)) ≫
        PullbackCone.fst (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) =
      PullbackCone.fst s ∧
    IsLimit.lift H₂ (BinaryFan.mk (PullbackCone.fst s) (PullbackCone.snd s)) ≫
          PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) =
        PullbackCone.snd s ∧
      ∀ {m : s.pt ⟶ (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)).pt},
        m ≫ PullbackCone.fst (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.fst s →
          m ≫ PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.snd s →
            m = IsLimit.lift H₂ (BinaryFan.mk (PullbackCone.fst s) (PullbackCone.snd s))
[PROOFSTEP]
use H₂.fac (BinaryFan.mk s.fst s.snd) ⟨WalkingPair.left⟩
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
⊢ IsLimit.lift H₂ (BinaryFan.mk (PullbackCone.fst s) (PullbackCone.snd s)) ≫
        PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) =
      PullbackCone.snd s ∧
    ∀ {m : s.pt ⟶ (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)).pt},
      m ≫ PullbackCone.fst (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.fst s →
        m ≫ PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.snd s →
          m = IsLimit.lift H₂ (BinaryFan.mk (PullbackCone.fst s) (PullbackCone.snd s))
[PROOFSTEP]
use H₂.fac (BinaryFan.mk s.fst s.snd) ⟨WalkingPair.right⟩
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
⊢ ∀ {m : s.pt ⟶ (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)).pt},
    m ≫ PullbackCone.fst (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.fst s →
      m ≫ PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.snd s →
        m = IsLimit.lift H₂ (BinaryFan.mk (PullbackCone.fst s) (PullbackCone.snd s))
[PROOFSTEP]
intro m h₁ h₂
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)).pt
h₁ : m ≫ PullbackCone.fst (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.snd s
⊢ m = IsLimit.lift H₂ (BinaryFan.mk (PullbackCone.fst s) (PullbackCone.snd s))
[PROOFSTEP]
apply H₂.hom_ext
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)).pt
h₁ : m ≫ PullbackCone.fst (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.snd s
⊢ ∀ (j : Discrete WalkingPair),
    m ≫ NatTrans.app (BinaryFan.mk h k).π j =
      IsLimit.lift H₂ (BinaryFan.mk (PullbackCone.fst s) (PullbackCone.snd s)) ≫ NatTrans.app (BinaryFan.mk h k).π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case right.mk.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)).pt
h₁ : m ≫ PullbackCone.fst (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.snd s
⊢ m ≫ NatTrans.app (BinaryFan.mk h k).π { as := WalkingPair.left } =
    IsLimit.lift H₂ (BinaryFan.mk (PullbackCone.fst s) (PullbackCone.snd s)) ≫
      NatTrans.app (BinaryFan.mk h k).π { as := WalkingPair.left }
[PROOFSTEP]
exact h₁.trans (H₂.fac (BinaryFan.mk s.fst s.snd) ⟨WalkingPair.left⟩).symm
[GOAL]
case right.mk.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)).pt
h₁ : m ≫ PullbackCone.fst (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (PullbackCone.mk h k (_ : h ≫ f = k ≫ g)) = PullbackCone.snd s
⊢ m ≫ NatTrans.app (BinaryFan.mk h k).π { as := WalkingPair.right } =
    IsLimit.lift H₂ (BinaryFan.mk (PullbackCone.fst s) (PullbackCone.snd s)) ≫
      NatTrans.app (BinaryFan.mk h k).π { as := WalkingPair.right }
[PROOFSTEP]
exact h₂.trans (H₂.fac (BinaryFan.mk s.fst s.snd) ⟨WalkingPair.right⟩).symm
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ IsLimit (F.mapCone (limitConeOfTerminalAndPullbacks K).cone)
[PROOFSTEP]
apply isBinaryProductOfIsTerminalIsPullback _ _ (isLimitOfHasTerminalOfPreservesLimit F)
[GOAL]
case hc
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ IsLimit
    (PullbackCone.mk (NatTrans.app (F.mapCone (limitConeOfTerminalAndPullbacks K).cone).π { as := WalkingPair.left })
      (NatTrans.app (F.mapCone (limitConeOfTerminalAndPullbacks K).cone).π { as := WalkingPair.right })
      (_ :
        NatTrans.app (F.mapCone (limitConeOfTerminalAndPullbacks K).cone).π { as := WalkingPair.left } ≫ ?f =
          NatTrans.app (F.mapCone (limitConeOfTerminalAndPullbacks K).cone).π { as := WalkingPair.right } ≫ ?g))
case f
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ (K ⋙ F).obj { as := WalkingPair.left } ⟶ F.obj (⊤_ C)
case g
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ (K ⋙ F).obj { as := WalkingPair.right } ⟶ F.obj (⊤_ C)
[PROOFSTEP]
apply isLimitOfHasPullbackOfPreservesLimit
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
⊢ m =
    (fun s =>
        IsColimit.desc hc
          (PushoutCocone.mk (NatTrans.app s.ι { as := WalkingPair.left }) (NatTrans.app s.ι { as := WalkingPair.right })
            (_ : f ≫ NatTrans.app s.ι { as := WalkingPair.left } = g ≫ NatTrans.app s.ι { as := WalkingPair.right })))
      s
[PROOFSTEP]
let c' :=
  PushoutCocone.mk (c.ι.app ⟨WalkingPair.left⟩ ≫ m) (c.ι.app ⟨WalkingPair.right⟩ ≫ m) (hX.hom_ext (f ≫ _) (g ≫ _))
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ m =
    (fun s =>
        IsColimit.desc hc
          (PushoutCocone.mk (NatTrans.app s.ι { as := WalkingPair.left }) (NatTrans.app s.ι { as := WalkingPair.right })
            (_ : f ≫ NatTrans.app s.ι { as := WalkingPair.left } = g ≫ NatTrans.app s.ι { as := WalkingPair.right })))
      s
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ m =
    IsColimit.desc hc
      (PushoutCocone.mk (NatTrans.app s.ι { as := WalkingPair.left }) (NatTrans.app s.ι { as := WalkingPair.right })
        (_ : f ≫ NatTrans.app s.ι { as := WalkingPair.left } = g ≫ NatTrans.app s.ι { as := WalkingPair.right }))
[PROOFSTEP]
rw [← J, ← J]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ m =
    IsColimit.desc hc
      (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m)
        (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
        (_ :
          f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m))
[PROOFSTEP]
apply hc.hom_ext
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ ∀ (j : WalkingSpan),
    NatTrans.app
          (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
              (_ :
                f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right })).ι
          j ≫
        m =
      NatTrans.app
          (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
              (_ :
                f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right })).ι
          j ≫
        IsColimit.desc hc
          (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m)
            (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
            (_ :
              f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m =
                g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m))
[PROOFSTEP]
rintro (_ | (_ | _))
[GOAL]
case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ NatTrans.app
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
            (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right })).ι
        none ≫
      m =
    NatTrans.app
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
            (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right })).ι
        none ≫
      IsColimit.desc hc
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m)
          (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
          (_ :
            f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m))
[PROOFSTEP]
simp only [PushoutCocone.mk_ι_app_zero, PushoutCocone.mk_ι_app, Category.assoc]
[GOAL]
case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ NatTrans.app
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
            (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right })).ι
        (some WalkingPair.left) ≫
      m =
    NatTrans.app
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
            (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right })).ι
        (some WalkingPair.left) ≫
      IsColimit.desc hc
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m)
          (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
          (_ :
            f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m))
[PROOFSTEP]
simp only [PushoutCocone.mk_ι_app_zero, PushoutCocone.mk_ι_app, Category.assoc]
[GOAL]
case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ NatTrans.app
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
            (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right })).ι
        (some WalkingPair.right) ≫
      m =
    NatTrans.app
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
            (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right })).ι
        (some WalkingPair.right) ≫
      IsColimit.desc hc
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m)
          (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
          (_ :
            f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m))
[PROOFSTEP]
simp only [PushoutCocone.mk_ι_app_zero, PushoutCocone.mk_ι_app, Category.assoc]
[GOAL]
case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m =
    f ≫
      NatTrans.app c.ι { as := WalkingPair.left } ≫
        IsColimit.desc hc
          (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m)
            (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
            (_ :
              f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m =
                g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m))
case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ NatTrans.app c.ι { as := WalkingPair.left } ≫ m =
    NatTrans.app c.ι { as := WalkingPair.left } ≫
      IsColimit.desc hc
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m)
          (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
          (_ :
            f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m))
case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ NatTrans.app c.ι { as := WalkingPair.right } ≫ m =
    NatTrans.app c.ι { as := WalkingPair.right } ≫
      IsColimit.desc hc
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m)
          (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
          (_ :
            f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m))
[PROOFSTEP]
congr 1
[GOAL]
case none.e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ NatTrans.app c.ι { as := WalkingPair.left } ≫ m =
    NatTrans.app c.ι { as := WalkingPair.left } ≫
      IsColimit.desc hc
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m)
          (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
          (_ :
            f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m))
case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ NatTrans.app c.ι { as := WalkingPair.left } ≫ m =
    NatTrans.app c.ι { as := WalkingPair.left } ≫
      IsColimit.desc hc
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m)
          (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
          (_ :
            f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m))
case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left }) (NatTrans.app c.ι { as := WalkingPair.right })
      (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } = g ≫ NatTrans.app c.ι { as := WalkingPair.right }))
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j
c' : PushoutCocone f g :=
  PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m) (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
    (_ : f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
⊢ NatTrans.app c.ι { as := WalkingPair.right } ≫ m =
    NatTrans.app c.ι { as := WalkingPair.right } ≫
      IsColimit.desc hc
        (PushoutCocone.mk (NatTrans.app c.ι { as := WalkingPair.left } ≫ m)
          (NatTrans.app c.ι { as := WalkingPair.right } ≫ m)
          (_ :
            f ≫ NatTrans.app c.ι { as := WalkingPair.left } ≫ m = g ≫ NatTrans.app c.ι { as := WalkingPair.right } ≫ m))
[PROOFSTEP]
exacts [(hc.fac c' WalkingSpan.left).symm, (hc.fac c' WalkingSpan.left).symm, (hc.fac c' WalkingSpan.right).symm]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g))
⊢ IsColimit (BinaryCofan.mk f g)
[PROOFSTEP]
apply isBinaryCoproductOfIsInitialIsPushout _ _ H₁
[GOAL]
case hc
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g))
⊢ IsColimit
    (PushoutCocone.mk (NatTrans.app (BinaryCofan.mk f g).ι { as := WalkingPair.left })
      (NatTrans.app (BinaryCofan.mk f g).ι { as := WalkingPair.right })
      (_ :
        ?f ≫ NatTrans.app (BinaryCofan.mk f g).ι { as := WalkingPair.left } =
          ?g ≫ NatTrans.app (BinaryCofan.mk f g).ι { as := WalkingPair.right }))
case f
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g))
⊢ W ⟶ (pair X Y).obj { as := WalkingPair.left }
case g
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g))
⊢ W ⟶ (pair X Y).obj { as := WalkingPair.right }
[PROOFSTEP]
exact H₂
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
⊢ IsColimit (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g))
[PROOFSTEP]
apply PushoutCocone.isColimitAux'
[GOAL]
case create
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
⊢ (s : PushoutCocone h k) →
    { l //
      PushoutCocone.inl (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ l = PushoutCocone.inl s ∧
        PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ l = PushoutCocone.inr s ∧
          ∀ {m : (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)).pt ⟶ s.pt},
            PushoutCocone.inl (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inl s →
              PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inr s → m = l }
[PROOFSTEP]
intro s
[GOAL]
case create
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ { l //
    PushoutCocone.inl (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ l = PushoutCocone.inl s ∧
      PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ l = PushoutCocone.inr s ∧
        ∀ {m : (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)).pt ⟶ s.pt},
          PushoutCocone.inl (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inl s →
            PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inr s → m = l }
[PROOFSTEP]
use H₂.desc (BinaryCofan.mk s.inl s.inr)
[GOAL]
case property
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ PushoutCocone.inl (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫
        IsColimit.desc H₂ (BinaryCofan.mk (PushoutCocone.inl s) (PushoutCocone.inr s)) =
      PushoutCocone.inl s ∧
    PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫
          IsColimit.desc H₂ (BinaryCofan.mk (PushoutCocone.inl s) (PushoutCocone.inr s)) =
        PushoutCocone.inr s ∧
      ∀ {m : (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)).pt ⟶ s.pt},
        PushoutCocone.inl (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inl s →
          PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inr s →
            m = IsColimit.desc H₂ (BinaryCofan.mk (PushoutCocone.inl s) (PushoutCocone.inr s))
[PROOFSTEP]
use H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.left⟩
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫
        IsColimit.desc H₂ (BinaryCofan.mk (PushoutCocone.inl s) (PushoutCocone.inr s)) =
      PushoutCocone.inr s ∧
    ∀ {m : (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)).pt ⟶ s.pt},
      PushoutCocone.inl (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inl s →
        PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inr s →
          m = IsColimit.desc H₂ (BinaryCofan.mk (PushoutCocone.inl s) (PushoutCocone.inr s))
[PROOFSTEP]
use H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.right⟩
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ ∀ {m : (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)).pt ⟶ s.pt},
    PushoutCocone.inl (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inl s →
      PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inr s →
        m = IsColimit.desc H₂ (BinaryCofan.mk (PushoutCocone.inl s) (PushoutCocone.inr s))
[PROOFSTEP]
intro m h₁ h₂
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)).pt ⟶ s.pt
h₁ : PushoutCocone.inl (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inl s
h₂ : PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inr s
⊢ m = IsColimit.desc H₂ (BinaryCofan.mk (PushoutCocone.inl s) (PushoutCocone.inr s))
[PROOFSTEP]
apply H₂.hom_ext
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)).pt ⟶ s.pt
h₁ : PushoutCocone.inl (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inl s
h₂ : PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inr s
⊢ ∀ (j : Discrete WalkingPair),
    NatTrans.app (BinaryCofan.mk f g).ι j ≫ m =
      NatTrans.app (BinaryCofan.mk f g).ι j ≫
        IsColimit.desc H₂ (BinaryCofan.mk (PushoutCocone.inl s) (PushoutCocone.inr s))
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case right.mk.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)).pt ⟶ s.pt
h₁ : PushoutCocone.inl (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inl s
h₂ : PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inr s
⊢ NatTrans.app (BinaryCofan.mk f g).ι { as := WalkingPair.left } ≫ m =
    NatTrans.app (BinaryCofan.mk f g).ι { as := WalkingPair.left } ≫
      IsColimit.desc H₂ (BinaryCofan.mk (PushoutCocone.inl s) (PushoutCocone.inr s))
[PROOFSTEP]
exact h₁.trans (H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.left⟩).symm
[GOAL]
case right.mk.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)).pt ⟶ s.pt
h₁ : PushoutCocone.inl (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inl s
h₂ : PushoutCocone.inr (PushoutCocone.mk f g (_ : h ≫ f = k ≫ g)) ≫ m = PushoutCocone.inr s
⊢ NatTrans.app (BinaryCofan.mk f g).ι { as := WalkingPair.right } ≫ m =
    NatTrans.app (BinaryCofan.mk f g).ι { as := WalkingPair.right } ≫
      IsColimit.desc H₂ (BinaryCofan.mk (PushoutCocone.inl s) (PushoutCocone.inr s))
[PROOFSTEP]
exact h₂.trans (H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.right⟩).symm
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : PreservesColimitsOfShape WalkingSpan F
K : Discrete WalkingPair ⥤ C
⊢ IsColimit (F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone)
[PROOFSTEP]
apply isBinaryCoproductOfIsInitialIsPushout _ _ (isColimitOfHasInitialOfPreservesColimit F)
[GOAL]
case hc
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : PreservesColimitsOfShape WalkingSpan F
K : Discrete WalkingPair ⥤ C
⊢ IsColimit
    (PushoutCocone.mk
      (NatTrans.app (F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι { as := WalkingPair.left })
      (NatTrans.app (F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι { as := WalkingPair.right })
      (_ :
        ?f ≫ NatTrans.app (F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι { as := WalkingPair.left } =
          ?g ≫ NatTrans.app (F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι { as := WalkingPair.right }))
case f
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : PreservesColimitsOfShape WalkingSpan F
K : Discrete WalkingPair ⥤ C
⊢ F.obj (⊥_ C) ⟶ (K ⋙ F).obj { as := WalkingPair.left }
case g
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty) F
inst✝ : PreservesColimitsOfShape WalkingSpan F
K : Discrete WalkingPair ⥤ C
⊢ F.obj (⊥_ C) ⟶ (K ⋙ F).obj { as := WalkingPair.right }
[PROOFSTEP]
apply isColimitOfHasPushoutOfPreservesColimit
