[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


[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ F.map (f ≫ Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv)) = F.map 0
[PROOFSTEP]
have reassoc' {W : D} (h : hf.Z ⟶ W) : F.map f ≫ hf.g ≫ h = 0 ≫ h := by rw [← Category.assoc, eq_whisker hf.w]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
W : D
h : NormalMono.Z (F.map f) ⟶ W
⊢ F.map f ≫ NormalMono.g ≫ h = 0 ≫ h
[PROOFSTEP]
rw [← Category.assoc, eq_whisker hf.w]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
reassoc' : ∀ {W : D} (h : NormalMono.Z (F.map f) ⟶ W), F.map f ≫ NormalMono.g ≫ h = 0 ≫ h
⊢ F.map (f ≫ Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv)) = F.map 0
[PROOFSTEP]
simp [reassoc']
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ F.map (Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv)) ≫
      (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).hom =
    NormalMono.g
[PROOFSTEP]
simp only [Full.witness, Category.assoc, Iso.inv_hom_id, Category.comp_id]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ KernelFork.ofι
      (Fork.ι (KernelFork.ofι (F.map f) (_ : F.map f ≫ NormalMono.g = 0)) ≫
        𝟙 ((parallelPair NormalMono.g 0).obj WalkingParallelPair.zero))
      (_ :
        (Fork.ι (KernelFork.ofι (F.map f) (_ : F.map f ≫ NormalMono.g = 0)) ≫
              𝟙 ((parallelPair NormalMono.g 0).obj WalkingParallelPair.zero)) ≫
            F.map (Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv)) =
          0) ≅
    (Cones.postcomposeEquivalence (compNatIso F)).functor.obj
      (F.mapCone
        (KernelFork.ofι f
          (_ : f ≫ Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv) = 0)))
[PROOFSTEP]
apply Iso.symm
[GOAL]
case I
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ (Cones.postcomposeEquivalence (compNatIso F)).functor.obj
      (F.mapCone
        (KernelFork.ofι f
          (_ : f ≫ Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv) = 0))) ≅
    KernelFork.ofι
      (Fork.ι (KernelFork.ofι (F.map f) (_ : F.map f ≫ NormalMono.g = 0)) ≫
        𝟙 ((parallelPair NormalMono.g 0).obj WalkingParallelPair.zero))
      (_ :
        (Fork.ι (KernelFork.ofι (F.map f) (_ : F.map f ≫ NormalMono.g = 0)) ≫
              𝟙 ((parallelPair NormalMono.g 0).obj WalkingParallelPair.zero)) ≫
            F.map (Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv)) =
          0)
[PROOFSTEP]
apply isoOfι
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
f : X ⟶ Y
I : NormalMono f
⊢ f ≫ g = f ≫ 0
[PROOFSTEP]
simpa using I.w
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ g ≫ k ≫ NormalMono.g = 0
[PROOFSTEP]
have reassoc' {W : C} (h' : S ⟶ W) : f ≫ h ≫ h' = g ≫ k ≫ h' := by simp only [← Category.assoc, eq_whisker comm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
W : C
h' : S ⟶ W
⊢ f ≫ h ≫ h' = g ≫ k ≫ h'
[PROOFSTEP]
simp only [← Category.assoc, eq_whisker comm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
reassoc' : ∀ {W : C} (h' : S ⟶ W), f ≫ h ≫ h' = g ≫ k ≫ h'
⊢ g ≫ k ≫ NormalMono.g = 0
[PROOFSTEP]
rw [← reassoc', hn.w, HasZeroMorphisms.comp_zero]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ IsLimit (KernelFork.ofι g (_ : g ≫ k ≫ NormalMono.g = 0))
[PROOFSTEP]
letI gr := regularOfIsPullbackSndOfRegular comm t
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
gr : RegularMono g := regularOfIsPullbackSndOfRegular comm t
⊢ IsLimit (KernelFork.ofι g (_ : g ≫ k ≫ NormalMono.g = 0))
[PROOFSTEP]
have q := (HasZeroMorphisms.comp_zero k hn.Z).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
gr : RegularMono g := regularOfIsPullbackSndOfRegular comm t
q : 0 = k ≫ 0
⊢ IsLimit (KernelFork.ofι g (_ : g ≫ k ≫ NormalMono.g = 0))
[PROOFSTEP]
convert gr.isLimit
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : NormalMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ RegularMono f
[PROOFSTEP]
haveI := normalMonoOfMono f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : NormalMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
this : NormalMono f
⊢ RegularMono f
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ F.map (Full.preimage ((Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g) ≫ f) = F.map 0
[PROOFSTEP]
simp [hf.w]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ (Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).symm.hom ≫
      F.map (Full.preimage ((Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g)) =
    NormalEpi.g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ CokernelCofork.ofπ
      (𝟙 ((parallelPair NormalEpi.g 0).obj WalkingParallelPair.one) ≫
        Cofork.π (CokernelCofork.ofπ (F.map f) (_ : NormalEpi.g ≫ F.map f = 0)))
      (_ :
        F.map (Full.preimage ((Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g)) ≫
            𝟙 ((parallelPair NormalEpi.g 0).obj WalkingParallelPair.one) ≫
              Cofork.π (CokernelCofork.ofπ (F.map f) (_ : NormalEpi.g ≫ F.map f = 0)) =
          0) ≅
    (Cocones.precomposeEquivalence (compNatIso F).symm).functor.obj
      (F.mapCocone
        (CokernelCofork.ofπ f
          (_ : Full.preimage ((Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g) ≫ f = 0)))
[PROOFSTEP]
apply Iso.symm
[GOAL]
case I
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ (Cocones.precomposeEquivalence (compNatIso F).symm).functor.obj
      (F.mapCocone
        (CokernelCofork.ofπ f
          (_ : Full.preimage ((Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g) ≫ f = 0))) ≅
    CokernelCofork.ofπ
      (𝟙 ((parallelPair NormalEpi.g 0).obj WalkingParallelPair.one) ≫
        Cofork.π (CokernelCofork.ofπ (F.map f) (_ : NormalEpi.g ≫ F.map f = 0)))
      (_ :
        F.map (Full.preimage ((Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g)) ≫
            𝟙 ((parallelPair NormalEpi.g 0).obj WalkingParallelPair.one) ≫
              Cofork.π (CokernelCofork.ofπ (F.map f) (_ : NormalEpi.g ≫ F.map f = 0)) =
          0)
[PROOFSTEP]
apply isoOfπ
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
f : X ⟶ Y
I : NormalEpi f
⊢ g ≫ f = 0 ≫ f
[PROOFSTEP]
simpa using I.w
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ (NormalEpi.g ≫ f) ≫ h = 0
[PROOFSTEP]
have reassoc' {W : C} (h' : R ⟶ W) : gn.g ≫ g ≫ h' = 0 ≫ h' := by rw [← Category.assoc, eq_whisker gn.w]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
W : C
h' : R ⟶ W
⊢ NormalEpi.g ≫ g ≫ h' = 0 ≫ h'
[PROOFSTEP]
rw [← Category.assoc, eq_whisker gn.w]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
reassoc' : ∀ {W : C} (h' : R ⟶ W), NormalEpi.g ≫ g ≫ h' = 0 ≫ h'
⊢ (NormalEpi.g ≫ f) ≫ h = 0
[PROOFSTEP]
rw [Category.assoc, comm, reassoc', zero_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ IsColimit (CokernelCofork.ofπ h (_ : (NormalEpi.g ≫ f) ≫ h = 0))
[PROOFSTEP]
letI hn := regularOfIsPushoutSndOfRegular comm t
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
hn : RegularEpi h := regularOfIsPushoutSndOfRegular comm t
⊢ IsColimit (CokernelCofork.ofπ h (_ : (NormalEpi.g ≫ f) ≫ h = 0))
[PROOFSTEP]
have q := (@zero_comp _ _ _ gn.W _ _ f).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
hn : RegularEpi h := regularOfIsPushoutSndOfRegular comm t
q : 0 = 0 ≫ f
⊢ IsColimit (CokernelCofork.ofπ h (_ : (NormalEpi.g ≫ f) ≫ h = 0))
[PROOFSTEP]
convert hn.isColimit
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
⊢ ∀ {Z' : Cᵒᵖ} (g' : X ⟶ Z') (eq' : NormalMono.g.op ≫ g' = 0) (m_1 : Y ⟶ Z'),
    f ≫ m_1 = g' →
      m_1 =
        (fun {Z'} g' w' =>
            (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop
                  (_ : { unop := g'.unop ≫ NormalMono.g }.unop = { unop := 0 }.unop))).op)
          g' eq'
[PROOFSTEP]
rintro Z' g' w' m' rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ m' =
    (fun {Z'} g' w' =>
        (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop
              (_ : { unop := g'.unop ≫ NormalMono.g }.unop = { unop := 0 }.unop))).op)
      (f ≫ m') w'
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ m'.unop =
    ((fun {Z'} g' w' =>
          (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop
                (_ : { unop := g'.unop ≫ NormalMono.g }.unop = { unop := 0 }.unop))).op)
        (f ≫ m') w').unop
[PROOFSTEP]
apply m.isLimit.uniq (KernelFork.ofι (m'.unop ≫ f.unop) _) m'.unop
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ ∀ (j : WalkingParallelPair),
    m'.unop ≫ NatTrans.app (KernelFork.ofι f.unop (_ : f.unop ≫ NormalMono.g = 0)).π j =
      NatTrans.app
        (KernelFork.ofι (m'.unop ≫ f.unop) (_ : { unop := (f ≫ m').unop ≫ NormalMono.g }.unop = { unop := 0 }.unop)).π j
[PROOFSTEP]
rintro (⟨⟩ | ⟨⟩)
[GOAL]
case a.zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ m'.unop ≫ NatTrans.app (KernelFork.ofι f.unop (_ : f.unop ≫ NormalMono.g = 0)).π WalkingParallelPair.zero =
    NatTrans.app
      (KernelFork.ofι (m'.unop ≫ f.unop) (_ : { unop := (f ≫ m').unop ≫ NormalMono.g }.unop = { unop := 0 }.unop)).π
      WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
case a.one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ m'.unop ≫ NatTrans.app (KernelFork.ofι f.unop (_ : f.unop ≫ NormalMono.g = 0)).π WalkingParallelPair.one =
    NatTrans.app
      (KernelFork.ofι (m'.unop ≫ f.unop) (_ : { unop := (f ≫ m').unop ≫ NormalMono.g }.unop = { unop := 0 }.unop)).π
      WalkingParallelPair.one
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
⊢ ∀ {W' : Cᵒᵖ} (g' : W' ⟶ Y) (eq' : g' ≫ NormalEpi.g.op = 0) (m_1 : W' ⟶ X),
    m_1 ≫ f = g' →
      m_1 =
        (fun {W'} g' w' =>
            (↑(CokernelCofork.IsColimit.desc' NormalEpi.isColimit g'.unop
                  (_ : { unop := NormalEpi.g ≫ g'.unop }.unop = { unop := 0 }.unop))).op)
          g' eq'
[PROOFSTEP]
rintro Z' g' w' m' rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ m' =
    (fun {W'} g' w' =>
        (↑(CokernelCofork.IsColimit.desc' NormalEpi.isColimit g'.unop
              (_ : { unop := NormalEpi.g ≫ g'.unop }.unop = { unop := 0 }.unop))).op)
      (m' ≫ f) w'
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ m'.unop =
    ((fun {W'} g' w' =>
          (↑(CokernelCofork.IsColimit.desc' NormalEpi.isColimit g'.unop
                (_ : { unop := NormalEpi.g ≫ g'.unop }.unop = { unop := 0 }.unop))).op)
        (m' ≫ f) w').unop
[PROOFSTEP]
apply m.isColimit.uniq (CokernelCofork.ofπ (f.unop ≫ m'.unop) _) m'.unop
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ ∀ (j : WalkingParallelPair),
    NatTrans.app (CokernelCofork.ofπ f.unop (_ : NormalEpi.g ≫ f.unop = 0)).ι j ≫ m'.unop =
      NatTrans.app
        (CokernelCofork.ofπ (f.unop ≫ m'.unop)
            (_ : { unop := NormalEpi.g ≫ (m' ≫ f).unop }.unop = { unop := 0 }.unop)).ι
        j
[PROOFSTEP]
rintro (⟨⟩ | ⟨⟩)
[GOAL]
case a.zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ NatTrans.app (CokernelCofork.ofπ f.unop (_ : NormalEpi.g ≫ f.unop = 0)).ι WalkingParallelPair.zero ≫ m'.unop =
    NatTrans.app
      (CokernelCofork.ofπ (f.unop ≫ m'.unop) (_ : { unop := NormalEpi.g ≫ (m' ≫ f).unop }.unop = { unop := 0 }.unop)).ι
      WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
case a.one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ NatTrans.app (CokernelCofork.ofπ f.unop (_ : NormalEpi.g ≫ f.unop = 0)).ι WalkingParallelPair.one ≫ m'.unop =
    NatTrans.app
      (CokernelCofork.ofπ (f.unop ≫ m'.unop) (_ : { unop := NormalEpi.g ≫ (m' ≫ f).unop }.unop = { unop := 0 }.unop)).ι
      WalkingParallelPair.one
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : NormalEpiCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
⊢ RegularEpi f
[PROOFSTEP]
haveI := normalEpiOfEpi f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : NormalEpiCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
this : NormalEpi f
⊢ RegularEpi f
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasPullbacks C
⊢ HasPullbacks (Over B)
[PROOFSTEP]
letI : HasLimitsOfShape (ULiftHom.{v} (ULift.{v} WalkingCospan)) C :=
  hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv.{v} _)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasPullbacks C
this : HasLimitsOfShape (ULiftHom (ULift WalkingCospan)) C :=
  hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv WalkingCospan)
⊢ HasPullbacks (Over B)
[PROOFSTEP]
letI : Category (ULiftHom.{v} (ULift.{v} WalkingCospan)) := inferInstance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasPullbacks C
this✝ : HasLimitsOfShape (ULiftHom (ULift WalkingCospan)) C :=
  hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv WalkingCospan)
this : Category.{v, v} (ULiftHom (ULift WalkingCospan)) := inferInstance
⊢ HasPullbacks (Over B)
[PROOFSTEP]
exact hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv.{v, v} _).symm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasEqualizers C
⊢ HasEqualizers (Over B)
[PROOFSTEP]
letI : HasLimitsOfShape (ULiftHom.{v} (ULift.{v} WalkingParallelPair)) C :=
  hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv.{v} _)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasEqualizers C
this : HasLimitsOfShape (ULiftHom (ULift WalkingParallelPair)) C :=
  hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv WalkingParallelPair)
⊢ HasEqualizers (Over B)
[PROOFSTEP]
letI : Category (ULiftHom.{v} (ULift.{v} WalkingParallelPair)) := inferInstance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasEqualizers C
this✝ : HasLimitsOfShape (ULiftHom (ULift WalkingParallelPair)) C :=
  hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv WalkingParallelPair)
this : Category.{v, v} (ULiftHom (ULift WalkingParallelPair)) := inferInstance
⊢ HasEqualizers (Over B)
[PROOFSTEP]
exact hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv.{v, v} _).symm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
⊢ HasFiniteLimits (Over B)
[PROOFSTEP]
apply @hasFiniteLimits_of_hasEqualizers_and_finite_products _ _ ?_ ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
⊢ HasFiniteProducts (Over B)
[PROOFSTEP]
exact ConstructProducts.over_finiteProducts_of_finiteWidePullbacks
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
⊢ HasEqualizers (Over B)
[PROOFSTEP]
apply @hasEqualizers_of_hasPullbacks_and_binary_products _ _ ?_ _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
⊢ HasBinaryProducts (Over B)
[PROOFSTEP]
haveI : HasPullbacks C := ⟨inferInstance⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
this : HasPullbacks C
⊢ HasBinaryProducts (Over B)
[PROOFSTEP]
exact ConstructProducts.over_binaryProduct_of_pullback
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
⊢ HasLimitsOfSize.{w, ?u.4486, v, max u v} (Over B)
[PROOFSTEP]
apply @has_limits_of_hasEqualizers_and_products _ _ ?_ ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
⊢ HasProducts (Over B)
[PROOFSTEP]
exact ConstructProducts.over_products_of_widePullbacks
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
⊢ HasEqualizers (Over B)
[PROOFSTEP]
apply @hasEqualizers_of_hasPullbacks_and_binary_products _ _ ?_ _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
⊢ HasBinaryProducts (Over B)
[PROOFSTEP]
haveI : HasPullbacks C := ⟨inferInstance⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
this : HasPullbacks C
⊢ HasBinaryProducts (Over B)
[PROOFSTEP]
exact ConstructProducts.over_binaryProduct_of_pullback