[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
s : Cone F.op
j : Jᵒᵖ
⊢ ((fun s => (IsColimit.desc hc (Cone.unop s)).op) s ≫ NatTrans.app (Cocone.op c).π j).unop = (NatTrans.app s.π j).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
s : Cone F.op
m : s.pt ⟶ (Cocone.op c).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (Cocone.op c).π j = NatTrans.app s.π j
⊢ m = (fun s => (IsColimit.desc hc (Cone.unop s)).op) s
[PROOFSTEP]
refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
s : Cone F.op
m : s.pt ⟶ (Cocone.op c).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (Cocone.op c).π j = NatTrans.app s.π j
j : J
⊢ (NatTrans.app c.ι j ≫ m.unop).op = (NatTrans.app c.ι j ≫ ((fun s => (IsColimit.desc hc (Cone.unop s)).op) s).unop).op
[PROOFSTEP]
simpa only [Quiver.Hom.unop_op, IsColimit.fac] using w (op j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ C
c : Cone F
hc : IsLimit c
s : Cocone F.op
j : Jᵒᵖ
⊢ (NatTrans.app (Cone.op c).ι j ≫ (fun s => (IsLimit.lift hc (Cocone.unop s)).op) s).unop = (NatTrans.app s.ι j).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ C
c : Cone F
hc : IsLimit c
s : Cocone F.op
m : (Cone.op c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (Cone.op c).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => (IsLimit.lift hc (Cocone.unop s)).op) s
[PROOFSTEP]
refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ C
c : Cone F
hc : IsLimit c
s : Cocone F.op
m : (Cone.op c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (Cone.op c).ι j ≫ m = NatTrans.app s.ι j
j : J
⊢ (m.unop ≫ NatTrans.app c.π j).op = (((fun s => (IsLimit.lift hc (Cocone.unop s)).op) s).unop ≫ NatTrans.app c.π j).op
[PROOFSTEP]
simpa only [Quiver.Hom.unop_op, IsLimit.fac] using w (op j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.leftOp
j : Jᵒᵖ
⊢ ((fun s => (IsColimit.desc hc (coconeOfConeLeftOp s)).unop) s ≫ NatTrans.app (coneLeftOpOfCocone c).π j).op =
    (NatTrans.app s.π j).op
[PROOFSTEP]
simp only [coneLeftOpOfCocone_π_app, op_comp, Quiver.Hom.op_unop, IsColimit.fac, coconeOfConeLeftOp_ι_app, op_unop]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.leftOp
m : s.pt ⟶ (coneLeftOpOfCocone c).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (coneLeftOpOfCocone c).π j = NatTrans.app s.π j
⊢ m = (fun s => (IsColimit.desc hc (coconeOfConeLeftOp s)).unop) s
[PROOFSTEP]
refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.leftOp
m : s.pt ⟶ (coneLeftOpOfCocone c).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (coneLeftOpOfCocone c).π j = NatTrans.app s.π j
j : J
⊢ (NatTrans.app c.ι j ≫ m.op).unop =
    (NatTrans.app c.ι j ≫ ((fun s => (IsColimit.desc hc (coconeOfConeLeftOp s)).unop) s).op).unop
[PROOFSTEP]
simpa only [Quiver.Hom.op_unop, IsColimit.fac, coconeOfConeLeftOp_ι_app] using w (op j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
j : Jᵒᵖ
⊢ (NatTrans.app (coconeLeftOpOfCone c).ι j ≫ (fun s => (IsLimit.lift hc (coneOfCoconeLeftOp s)).unop) s).op =
    (NatTrans.app s.ι j).op
[PROOFSTEP]
simp only [coconeLeftOpOfCone_ι_app, op_comp, Quiver.Hom.op_unop, IsLimit.fac, coneOfCoconeLeftOp_π_app, op_unop]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
m : (coconeLeftOpOfCone c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (coconeLeftOpOfCone c).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => (IsLimit.lift hc (coneOfCoconeLeftOp s)).unop) s
[PROOFSTEP]
refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
m : (coconeLeftOpOfCone c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (coconeLeftOpOfCone c).ι j ≫ m = NatTrans.app s.ι j
j : J
⊢ (m.op ≫ NatTrans.app c.π j).unop =
    (((fun s => (IsLimit.lift hc (coneOfCoconeLeftOp s)).unop) s).op ≫ NatTrans.app c.π j).unop
[PROOFSTEP]
simpa only [Quiver.Hom.op_unop, IsLimit.fac, coneOfCoconeLeftOp_π_app] using w (op j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cocone F
hc : IsColimit c
s : Cone F.rightOp
j : J
⊢ ((fun s => (IsColimit.desc hc (coconeOfConeRightOp s)).op) s ≫ NatTrans.app (coneRightOpOfCocone c).π j).unop =
    (NatTrans.app s.π j).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cocone F
hc : IsColimit c
s : Cone F.rightOp
m : s.pt ⟶ (coneRightOpOfCocone c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneRightOpOfCocone c).π j = NatTrans.app s.π j
⊢ m = (fun s => (IsColimit.desc hc (coconeOfConeRightOp s)).op) s
[PROOFSTEP]
refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cocone F
hc : IsColimit c
s : Cone F.rightOp
m : s.pt ⟶ (coneRightOpOfCocone c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneRightOpOfCocone c).π j = NatTrans.app s.π j
j : Jᵒᵖ
⊢ (NatTrans.app c.ι j ≫ m.unop).op =
    (NatTrans.app c.ι j ≫ ((fun s => (IsColimit.desc hc (coconeOfConeRightOp s)).op) s).unop).op
[PROOFSTEP]
simpa only [Quiver.Hom.unop_op, IsColimit.fac] using w (unop j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
j : J
⊢ (NatTrans.app (coconeRightOpOfCone c).ι j ≫ (fun s => (IsLimit.lift hc (coneOfCoconeRightOp s)).op) s).unop =
    (NatTrans.app s.ι j).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
m : (coconeRightOpOfCone c).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeRightOpOfCone c).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => (IsLimit.lift hc (coneOfCoconeRightOp s)).op) s
[PROOFSTEP]
refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
m : (coconeRightOpOfCone c).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeRightOpOfCone c).ι j ≫ m = NatTrans.app s.ι j
j : Jᵒᵖ
⊢ (m.unop ≫ NatTrans.app c.π j).op =
    (((fun s => (IsLimit.lift hc (coneOfCoconeRightOp s)).op) s).unop ≫ NatTrans.app c.π j).op
[PROOFSTEP]
simpa only [Quiver.Hom.unop_op, IsLimit.fac] using w (unop j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone (Functor.unop F)
j : J
⊢ ((fun s => (IsColimit.desc hc (coconeOfConeUnop s)).unop) s ≫ NatTrans.app (coneUnopOfCocone c).π j).op =
    (NatTrans.app s.π j).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone (Functor.unop F)
m : s.pt ⟶ (coneUnopOfCocone c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneUnopOfCocone c).π j = NatTrans.app s.π j
⊢ m = (fun s => (IsColimit.desc hc (coconeOfConeUnop s)).unop) s
[PROOFSTEP]
refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone (Functor.unop F)
m : s.pt ⟶ (coneUnopOfCocone c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneUnopOfCocone c).π j = NatTrans.app s.π j
j : Jᵒᵖ
⊢ (NatTrans.app c.ι j ≫ m.op).unop =
    (NatTrans.app c.ι j ≫ ((fun s => (IsColimit.desc hc (coconeOfConeUnop s)).unop) s).op).unop
[PROOFSTEP]
simpa only [Quiver.Hom.op_unop, IsColimit.fac] using w (unop j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone (Functor.unop F)
j : J
⊢ (NatTrans.app (coconeUnopOfCone c).ι j ≫ (fun s => (IsLimit.lift hc (coneOfCoconeUnop s)).unop) s).op =
    (NatTrans.app s.ι j).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone (Functor.unop F)
m : (coconeUnopOfCone c).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeUnopOfCone c).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => (IsLimit.lift hc (coneOfCoconeUnop s)).unop) s
[PROOFSTEP]
refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone (Functor.unop F)
m : (coconeUnopOfCone c).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeUnopOfCone c).ι j ≫ m = NatTrans.app s.ι j
j : Jᵒᵖ
⊢ (m.op ≫ NatTrans.app c.π j).unop =
    (((fun s => (IsLimit.lift hc (coneOfCoconeUnop s)).unop) s).op ≫ NatTrans.app c.π j).unop
[PROOFSTEP]
simpa only [Quiver.Hom.op_unop, IsLimit.fac] using w (unop j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ C
c : Cocone F.op
hc : IsColimit c
s : Cone F
j : J
⊢ ((fun s => (IsColimit.desc hc (Cone.op s)).unop) s ≫ NatTrans.app (Cocone.unop c).π j).op = (NatTrans.app s.π j).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ C
c : Cocone F.op
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (Cocone.unop c).pt
w : ∀ (j : J), m ≫ NatTrans.app (Cocone.unop c).π j = NatTrans.app s.π j
⊢ m = (fun s => (IsColimit.desc hc (Cone.op s)).unop) s
[PROOFSTEP]
refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ C
c : Cocone F.op
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (Cocone.unop c).pt
w : ∀ (j : J), m ≫ NatTrans.app (Cocone.unop c).π j = NatTrans.app s.π j
j : Jᵒᵖ
⊢ (NatTrans.app c.ι j ≫ m.op).unop = (NatTrans.app c.ι j ≫ ((fun s => (IsColimit.desc hc (Cone.op s)).unop) s).op).unop
[PROOFSTEP]
simpa only [Quiver.Hom.op_unop, IsColimit.fac] using w (unop j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ C
c : Cone F.op
hc : IsLimit c
s : Cocone F
j : J
⊢ (NatTrans.app (Cone.unop c).ι j ≫ (fun s => (IsLimit.lift hc (Cocone.op s)).unop) s).op = (NatTrans.app s.ι j).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ C
c : Cone F.op
hc : IsLimit c
s : Cocone F
m : (Cone.unop c).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (Cone.unop c).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => (IsLimit.lift hc (Cocone.op s)).unop) s
[PROOFSTEP]
refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ C
c : Cone F.op
hc : IsLimit c
s : Cocone F
m : (Cone.unop c).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (Cone.unop c).ι j ≫ m = NatTrans.app s.ι j
j : Jᵒᵖ
⊢ (m.op ≫ NatTrans.app c.π j).unop = (((fun s => (IsLimit.lift hc (Cocone.op s)).unop) s).op ≫ NatTrans.app c.π j).unop
[PROOFSTEP]
simpa only [Quiver.Hom.op_unop, IsLimit.fac] using w (unop j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F.leftOp
hc : IsColimit c
s : Cone F
j : J
⊢ ((fun s => (IsColimit.desc hc (coconeLeftOpOfCone s)).op) s ≫ NatTrans.app (coneOfCoconeLeftOp c).π j).unop =
    (NatTrans.app s.π j).unop
[PROOFSTEP]
simp only [coneOfCoconeLeftOp_π_app, unop_comp, Quiver.Hom.unop_op, IsColimit.fac, coconeLeftOpOfCone_ι_app, unop_op]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F.leftOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeLeftOp c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfCoconeLeftOp c).π j = NatTrans.app s.π j
⊢ m = (fun s => (IsColimit.desc hc (coconeLeftOpOfCone s)).op) s
[PROOFSTEP]
refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F.leftOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeLeftOp c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfCoconeLeftOp c).π j = NatTrans.app s.π j
j : Jᵒᵖ
⊢ (NatTrans.app c.ι j ≫ m.unop).op =
    (NatTrans.app c.ι j ≫ ((fun s => (IsColimit.desc hc (coconeLeftOpOfCone s)).op) s).unop).op
[PROOFSTEP]
simpa only [Quiver.Hom.unop_op, IsColimit.fac, coneOfCoconeLeftOp_π_app] using w (unop j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
hc : IsLimit c
s : Cocone F
j : J
⊢ (NatTrans.app (coconeOfConeLeftOp c).ι j ≫ (fun s => (IsLimit.lift hc (coneLeftOpOfCocone s)).op) s).unop =
    (NatTrans.app s.ι j).unop
[PROOFSTEP]
simp only [coconeOfConeLeftOp_ι_app, unop_comp, Quiver.Hom.unop_op, IsLimit.fac, coneLeftOpOfCocone_π_app, unop_op]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeLeftOp c).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfConeLeftOp c).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => (IsLimit.lift hc (coneLeftOpOfCocone s)).op) s
[PROOFSTEP]
refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeLeftOp c).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfConeLeftOp c).ι j ≫ m = NatTrans.app s.ι j
j : Jᵒᵖ
⊢ (m.unop ≫ NatTrans.app c.π j).op =
    (((fun s => (IsLimit.lift hc (coneLeftOpOfCocone s)).op) s).unop ≫ NatTrans.app c.π j).op
[PROOFSTEP]
simpa only [Quiver.Hom.unop_op, IsLimit.fac, coconeOfConeLeftOp_ι_app] using w (unop j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cocone F.rightOp
hc : IsColimit c
s : Cone F
j : Jᵒᵖ
⊢ ((fun s => (IsColimit.desc hc (coconeRightOpOfCone s)).unop) s ≫ NatTrans.app (coneOfCoconeRightOp c).π j).op =
    (NatTrans.app s.π j).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cocone F.rightOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeRightOp c).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (coneOfCoconeRightOp c).π j = NatTrans.app s.π j
⊢ m = (fun s => (IsColimit.desc hc (coconeRightOpOfCone s)).unop) s
[PROOFSTEP]
refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cocone F.rightOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeRightOp c).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (coneOfCoconeRightOp c).π j = NatTrans.app s.π j
j : J
⊢ (NatTrans.app c.ι j ≫ m.op).unop =
    (NatTrans.app c.ι j ≫ ((fun s => (IsColimit.desc hc (coconeRightOpOfCone s)).unop) s).op).unop
[PROOFSTEP]
simpa only [Quiver.Hom.op_unop, IsColimit.fac] using w (op j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cone F.rightOp
hc : IsLimit c
s : Cocone F
j : Jᵒᵖ
⊢ (NatTrans.app (coconeOfConeRightOp c).ι j ≫ (fun s => (IsLimit.lift hc (coneRightOpOfCocone s)).unop) s).op =
    (NatTrans.app s.ι j).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cone F.rightOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeRightOp c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (coconeOfConeRightOp c).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => (IsLimit.lift hc (coneRightOpOfCocone s)).unop) s
[PROOFSTEP]
refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cone F.rightOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeRightOp c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (coconeOfConeRightOp c).ι j ≫ m = NatTrans.app s.ι j
j : J
⊢ (m.op ≫ NatTrans.app c.π j).unop =
    (((fun s => (IsLimit.lift hc (coneRightOpOfCocone s)).unop) s).op ≫ NatTrans.app c.π j).unop
[PROOFSTEP]
simpa only [Quiver.Hom.op_unop, IsLimit.fac] using w (op j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cocone (Functor.unop F)
hc : IsColimit c
s : Cone F
j : Jᵒᵖ
⊢ ((fun s => (IsColimit.desc hc (coconeUnopOfCone s)).op) s ≫ NatTrans.app (coneOfCoconeUnop c).π j).unop =
    (NatTrans.app s.π j).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cocone (Functor.unop F)
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeUnop c).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (coneOfCoconeUnop c).π j = NatTrans.app s.π j
⊢ m = (fun s => (IsColimit.desc hc (coconeUnopOfCone s)).op) s
[PROOFSTEP]
refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cocone (Functor.unop F)
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeUnop c).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (coneOfCoconeUnop c).π j = NatTrans.app s.π j
j : J
⊢ (NatTrans.app c.ι j ≫ m.unop).op =
    (NatTrans.app c.ι j ≫ ((fun s => (IsColimit.desc hc (coconeUnopOfCone s)).op) s).unop).op
[PROOFSTEP]
simpa only [Quiver.Hom.unop_op, IsColimit.fac] using w (op j)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cone (Functor.unop F)
hc : IsLimit c
s : Cocone F
j : Jᵒᵖ
⊢ (NatTrans.app (coconeOfConeUnop c).ι j ≫ (fun s => (IsLimit.lift hc (coneUnopOfCocone s)).op) s).unop =
    (NatTrans.app s.ι j).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cone (Functor.unop F)
hc : IsLimit c
s : Cocone F
m : (coconeOfConeUnop c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (coconeOfConeUnop c).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => (IsLimit.lift hc (coneUnopOfCocone s)).op) s
[PROOFSTEP]
refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cone (Functor.unop F)
hc : IsLimit c
s : Cocone F
m : (coconeOfConeUnop c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (coconeOfConeUnop c).ι j ≫ m = NatTrans.app s.ι j
j : J
⊢ (m.unop ≫ NatTrans.app c.π j).op =
    (((fun s => (IsLimit.lift hc (coneUnopOfCocone s)).op) s).unop ≫ NatTrans.app c.π j).op
[PROOFSTEP]
simpa only [Quiver.Hom.unop_op, IsLimit.fac] using w (op j)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
inst✝ : HasProductsOfShape X C
⊢ HasCoproductsOfShape X Cᵒᵖ
[PROOFSTEP]
haveI : HasLimitsOfShape (Discrete X)ᵒᵖ C := hasLimitsOfShape_of_equivalence (Discrete.opposite X).symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
inst✝ : HasProductsOfShape X C
this : HasLimitsOfShape (Discrete X)ᵒᵖ C
⊢ HasCoproductsOfShape X Cᵒᵖ
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
inst✝ : HasCoproductsOfShape X C
⊢ HasProductsOfShape X Cᵒᵖ
[PROOFSTEP]
haveI : HasColimitsOfShape (Discrete X)ᵒᵖ C := hasColimitsOfShape_of_equivalence (Discrete.opposite X).symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
inst✝ : HasCoproductsOfShape X C
this : HasColimitsOfShape (Discrete X)ᵒᵖ C
⊢ HasProductsOfShape X Cᵒᵖ
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
inst✝ : HasCoequalizers C
⊢ HasEqualizers Cᵒᵖ
[PROOFSTEP]
haveI : HasColimitsOfShape WalkingParallelPairᵒᵖ C := hasColimitsOfShape_of_equivalence walkingParallelPairOpEquiv
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
inst✝ : HasCoequalizers C
this : HasColimitsOfShape WalkingParallelPairᵒᵖ C
⊢ HasEqualizers Cᵒᵖ
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
inst✝ : HasEqualizers C
⊢ HasCoequalizers Cᵒᵖ
[PROOFSTEP]
haveI : HasLimitsOfShape WalkingParallelPairᵒᵖ C := hasLimitsOfShape_of_equivalence walkingParallelPairOpEquiv
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
inst✝ : HasEqualizers C
this : HasLimitsOfShape WalkingParallelPairᵒᵖ C
⊢ HasCoequalizers Cᵒᵖ
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
inst✝ : HasPushouts C
⊢ HasPullbacks Cᵒᵖ
[PROOFSTEP]
haveI : HasColimitsOfShape WalkingCospanᵒᵖ C := hasColimitsOfShape_of_equivalence walkingCospanOpEquiv.symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
inst✝ : HasPushouts C
this : HasColimitsOfShape WalkingCospanᵒᵖ C
⊢ HasPullbacks Cᵒᵖ
[PROOFSTEP]
apply hasLimitsOfShape_op_of_hasColimitsOfShape
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
inst✝ : HasPullbacks C
⊢ HasPushouts Cᵒᵖ
[PROOFSTEP]
haveI : HasLimitsOfShape WalkingSpanᵒᵖ C := hasLimitsOfShape_of_equivalence walkingSpanOpEquiv.symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
inst✝ : HasPullbacks C
this : HasLimitsOfShape WalkingSpanᵒᵖ C
⊢ HasPushouts Cᵒᵖ
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (X_1 : WalkingSpan) → (span f.op g.op).obj X_1 ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj X_1
[PROOFSTEP]
rintro (_ | _ | _)
[GOAL]
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).obj none ≅ (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj none
[PROOFSTEP]
rfl
[GOAL]
case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).obj (some WalkingPair.left) ≅
    (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj (some WalkingPair.left)
[PROOFSTEP]
rfl
[GOAL]
case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).obj (some WalkingPair.right) ≅
    (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).obj (some WalkingPair.right)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ {X_1 Y_1 : WalkingSpan} (f_1 : X_1 ⟶ Y_1),
    (span f.op g.op).map f_1 ≫
        (Option.casesOn Y_1 (Iso.refl ((span f.op g.op).obj none)) fun val =>
            WalkingPair.casesOn val (Iso.refl ((span f.op g.op).obj (some WalkingPair.left)))
              (Iso.refl ((span f.op g.op).obj (some WalkingPair.right)))).hom =
      (Option.casesOn X_1 (Iso.refl ((span f.op g.op).obj none)) fun val =>
            WalkingPair.casesOn val (Iso.refl ((span f.op g.op).obj (some WalkingPair.left)))
              (Iso.refl ((span f.op g.op).obj (some WalkingPair.right)))).hom ≫
        (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map f_1
[PROOFSTEP]
rintro (_ | _ | _) (_ | _ | _) f
[GOAL]
case none.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ none
⊢ (span f✝.op g.op).map f ≫
      (Option.casesOn none (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case none.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ (span f✝.op g.op).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case none.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ (span f✝.op g.op).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case some.left.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ (span f✝.op g.op).map f ≫
      (Option.casesOn none (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case some.left.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (span f✝.op g.op).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case some.left.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (span f✝.op g.op).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case some.right.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ (span f✝.op g.op).map f ≫
      (Option.casesOn none (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case some.right.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (span f✝.op g.op).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case some.right.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (span f✝.op g.op).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case none.none.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.id none) ≫
      (Option.casesOn none (Iso.refl ((span f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.id none)
[PROOFSTEP]
aesop_cat
[GOAL]
case none.some.left.init
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.init WalkingPair.left) ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.init WalkingPair.left)
[PROOFSTEP]
aesop_cat
[GOAL]
case none.some.right.init
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.init WalkingPair.right) ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.init WalkingPair.right)
[PROOFSTEP]
aesop_cat
[GOAL]
case some.left.some.left.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.id (some WalkingPair.left))
[PROOFSTEP]
aesop_cat
[GOAL]
case some.right.some.right.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (span f.op g.op).map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((span f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((span f.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map (WidePushoutShape.Hom.id (some WalkingPair.right))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g).op ≅ 𝟭 WalkingCospanᵒᵖ ⋙ (cospan f g).op
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (X_1 : WalkingCospan) → (cospan f.op g.op).obj X_1 ≅ (walkingSpanOpEquiv.inverse ⋙ (span f g).op).obj X_1
[PROOFSTEP]
rintro (_ | _ | _)
[GOAL]
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.op g.op).obj none ≅ (walkingSpanOpEquiv.inverse ⋙ (span f g).op).obj none
[PROOFSTEP]
rfl
[GOAL]
case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.op g.op).obj (some WalkingPair.left) ≅
    (walkingSpanOpEquiv.inverse ⋙ (span f g).op).obj (some WalkingPair.left)
[PROOFSTEP]
rfl
[GOAL]
case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.op g.op).obj (some WalkingPair.right) ≅
    (walkingSpanOpEquiv.inverse ⋙ (span f g).op).obj (some WalkingPair.right)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ ∀ {X_1 Y_1 : WalkingCospan} (f_1 : X_1 ⟶ Y_1),
    (cospan f.op g.op).map f_1 ≫
        (Option.casesOn Y_1 (Iso.refl ((cospan f.op g.op).obj none)) fun val =>
            WalkingPair.casesOn val (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.left)))
              (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.right)))).hom =
      (Option.casesOn X_1 (Iso.refl ((cospan f.op g.op).obj none)) fun val =>
            WalkingPair.casesOn val (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.left)))
              (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.right)))).hom ≫
        (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map f_1
[PROOFSTEP]
rintro (_ | _ | _) (_ | _ | _) f
[GOAL]
case none.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ none
⊢ (cospan f✝.op g.op).map f ≫
      (Option.casesOn none (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case none.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ (cospan f✝.op g.op).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case none.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ (cospan f✝.op g.op).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case some.left.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ (cospan f✝.op g.op).map f ≫
      (Option.casesOn none (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case some.left.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (cospan f✝.op g.op).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case some.left.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (cospan f✝.op g.op).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case some.right.none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ (cospan f✝.op g.op).map f ≫
      (Option.casesOn none (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case some.right.some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (cospan f✝.op g.op).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case some.right.some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (cospan f✝.op g.op).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f✝.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f✝.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f✝ g).op).map f
[PROOFSTEP]
cases f
[GOAL]
case none.none.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.op g.op).map (WidePullbackShape.Hom.id none) ≫
      (Option.casesOn none (Iso.refl ((cospan f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((cospan f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map (WidePullbackShape.Hom.id none)
[PROOFSTEP]
aesop_cat
[GOAL]
case some.left.none.term
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.op g.op).map (WidePullbackShape.Hom.term WalkingPair.left) ≫
      (Option.casesOn none (Iso.refl ((cospan f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map (WidePullbackShape.Hom.term WalkingPair.left)
[PROOFSTEP]
aesop_cat
[GOAL]
case some.left.some.left.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.op g.op).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map (WidePullbackShape.Hom.id (some WalkingPair.left))
[PROOFSTEP]
aesop_cat
[GOAL]
case some.right.none.term
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.op g.op).map (WidePullbackShape.Hom.term WalkingPair.right) ≫
      (Option.casesOn none (Iso.refl ((cospan f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map (WidePullbackShape.Hom.term WalkingPair.right)
[PROOFSTEP]
aesop_cat
[GOAL]
case some.right.some.right.id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (cospan f.op g.op).map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f.op g.op).obj none)) fun val =>
          WalkingPair.casesOn val (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f.op g.op).obj (some WalkingPair.right)))).hom ≫
      (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map (WidePullbackShape.Hom.id (some WalkingPair.right))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ (span f g).op ≅ 𝟭 WalkingSpanᵒᵖ ⋙ (span f g).op
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ PullbackCone.fst (unop c) = (inl c).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ PullbackCone.snd (unop c) = (inr c).unop
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ PullbackCone.fst (op c) = (inl c).op
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ PullbackCone.snd (op c) = (inr c).op
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ PushoutCocone.inl (unop c) = (fst c).unop
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ PushoutCocone.inr (unop c) = (snd c).unop
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ PushoutCocone.inl (op c) = (fst c).op
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ PushoutCocone.inr (op c) = (snd c).op
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ fst (PushoutCocone.unop (op c)) = (Iso.refl (PushoutCocone.unop (op c)).pt).hom ≫ fst c
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ snd (PushoutCocone.unop (op c)) = (Iso.refl (PushoutCocone.unop (op c)).pt).hom ≫ snd c
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ fst (PushoutCocone.op (unop c)) = (Iso.refl (PushoutCocone.op (unop c)).pt).hom ≫ fst c
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ snd (PushoutCocone.op (unop c)) = (Iso.refl (PushoutCocone.op (unop c)).pt).hom ≫ snd c
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ inl (PullbackCone.unop (op c)) ≫ (Iso.refl (PullbackCone.unop (op c)).pt).hom = inl c
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ inr (PullbackCone.unop (op c)) ≫ (Iso.refl (PullbackCone.unop (op c)).pt).hom = inr c
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ inl (PullbackCone.op (unop c)) ≫ (Iso.refl (PullbackCone.op (unop c)).pt).hom = inl c
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ inr (PullbackCone.op (unop c)) ≫ (Iso.refl (PullbackCone.op (unop c)).pt).hom = inr c
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsColimit c ≃ IsLimit (op c)
[PROOFSTEP]
apply equivOfSubsingletonOfSubsingleton
[GOAL]
case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsColimit c → IsLimit (op c)
[PROOFSTEP]
intro h
[GOAL]
case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
h : IsColimit c
⊢ IsLimit (op c)
[PROOFSTEP]
exact
  (IsLimit.postcomposeHomEquiv _ _).invFun
    ((IsLimit.whiskerEquivalenceEquiv walkingSpanOpEquiv.symm).toFun (isLimitCoconeOp _ h))
[GOAL]
case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsLimit (op c) → IsColimit c
[PROOFSTEP]
intro h
[GOAL]
case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
h : IsLimit (op c)
⊢ IsColimit c
[PROOFSTEP]
exact
  (IsColimit.equivIsoColimit c.opUnop).toFun
    (isColimitConeUnop _ ((IsLimit.postcomposeHomEquiv _ _).invFun ((IsLimit.whiskerEquivalenceEquiv _).toFun h)))
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsColimit c ≃ IsLimit (unop c)
[PROOFSTEP]
apply equivOfSubsingletonOfSubsingleton
[GOAL]
case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsColimit c → IsLimit (unop c)
[PROOFSTEP]
intro h
[GOAL]
case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
h : IsColimit c
⊢ IsLimit (unop c)
[PROOFSTEP]
exact isLimitCoconeUnop _ ((IsColimit.precomposeHomEquiv _ _).invFun ((IsColimit.whiskerEquivalenceEquiv _).toFun h))
[GOAL]
case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsLimit (unop c) → IsColimit c
[PROOFSTEP]
intro h
[GOAL]
case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
h : IsLimit (unop c)
⊢ IsColimit c
[PROOFSTEP]
exact
  (IsColimit.equivIsoColimit c.unopOp).toFun
    ((IsColimit.precomposeHomEquiv _ _).invFun
      ((IsColimit.whiskerEquivalenceEquiv walkingCospanOpEquiv.symm).toFun (isColimitConeOp _ h)))
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ NatTrans.app (PushoutCocone.unop (colimit.cocone (span f.op g.op))).π WalkingCospan.left = pushout.inl.unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ NatTrans.app (PushoutCocone.unop (colimit.cocone (span f.op g.op))).π WalkingCospan.right = pushout.inr.unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ pushout.inl ≫ (pullbackIsoUnopPushout f g).hom.op = pullback.fst.op
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pushout.inl ≫ (pullbackIsoUnopPushout f g).hom.op).unop = pullback.fst.op.unop
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pullbackIsoUnopPushout f g).hom ≫ pushout.inl.unop = pullback.fst
[PROOFSTEP]
rw [← pullbackIsoUnopPushout_inv_fst, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ pushout.inr ≫ (pullbackIsoUnopPushout f g).hom.op = pullback.snd.op
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pushout.inr ≫ (pullbackIsoUnopPushout f g).hom.op).unop = pullback.snd.op.unop
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pullbackIsoUnopPushout f g).hom ≫ pushout.inr.unop = pullback.snd
[PROOFSTEP]
rw [← pullbackIsoUnopPushout_inv_snd, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ NatTrans.app (PullbackCone.unop (limit.cone (cospan f.op g.op))).ι WalkingSpan.left = pullback.fst.unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ NatTrans.app (PullbackCone.unop (limit.cone (cospan f.op g.op))).ι WalkingSpan.right = pullback.snd.unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ (pushoutIsoUnopPullback f g).inv.op ≫ pullback.fst = pushout.inl.op
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ ((pushoutIsoUnopPullback f g).inv.op ≫ pullback.fst).unop = pushout.inl.op.unop
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ pullback.fst.unop ≫ (pushoutIsoUnopPullback f g).inv = pushout.inl
[PROOFSTEP]
rw [← pushoutIsoUnopPullback_inl_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ (pushoutIsoUnopPullback f g).inv.op ≫ pullback.snd = pushout.inr.op
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ ((pushoutIsoUnopPullback f g).inv.op ≫ pullback.snd).unop = pushout.inr.op.unop
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ pullback.snd.unop ≫ (pushoutIsoUnopPullback f g).inv = pushout.inr
[PROOFSTEP]
rw [← pushoutIsoUnopPullback_inr_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X✝ : Type v₂
inst✝ : HasZeroMorphisms C
X Y Q : C
p : Y ⟶ Q
f : X ⟶ Y
w : f ≫ p = 0
h : IsColimit (CokernelCofork.ofπ p w)
⊢ p.op ≫ f.op = 0
[PROOFSTEP]
rw [← op_comp, w, op_zero]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X✝ : Type v₂
inst✝ : HasZeroMorphisms C
X Y Q : C
p : Y ⟶ Q
f : X ⟶ Y
w : f ≫ p = 0
h : IsColimit (CokernelCofork.ofπ p w)
W'✝ : Cᵒᵖ
x : W'✝ ⟶ op Y
hx : x ≫ f.op = 0
b : W'✝ ⟶ op Q
hb : b ≫ p.op = x
⊢ Cofork.π (CokernelCofork.ofπ p w) ≫ b.unop =
    Cofork.π (CokernelCofork.ofπ p w) ≫
      ((fun {W'} x hx => (IsColimit.desc h (CokernelCofork.ofπ x.unop (_ : f ≫ x.unop = 0))).op) x hx).unop
[PROOFSTEP]
simpa only [Quiver.Hom.unop_op, Cofork.IsColimit.π_desc] using Quiver.Hom.op_inj hb
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X✝ : Type v₂
inst✝ : HasZeroMorphisms C
X Y Q : Cᵒᵖ
p : Y ⟶ Q
f : X ⟶ Y
w : f ≫ p = 0
h : IsColimit (CokernelCofork.ofπ p w)
⊢ p.unop ≫ f.unop = 0
[PROOFSTEP]
rw [← unop_comp, w, unop_zero]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X✝ : Type v₂
inst✝ : HasZeroMorphisms C
X Y Q : Cᵒᵖ
p : Y ⟶ Q
f : X ⟶ Y
w : f ≫ p = 0
h : IsColimit (CokernelCofork.ofπ p w)
W'✝ : C
x : W'✝ ⟶ Y.unop
hx : x ≫ f.unop = 0
b : W'✝ ⟶ Q.unop
hb : b ≫ p.unop = x
⊢ Cofork.π (CokernelCofork.ofπ p w) ≫ b.op =
    Cofork.π (CokernelCofork.ofπ p w) ≫
      ((fun {W'} x hx => (IsColimit.desc h (CokernelCofork.ofπ x.op (_ : f ≫ x.op = 0))).unop) x hx).op
[PROOFSTEP]
simpa only [Quiver.Hom.op_unop, Cofork.IsColimit.π_desc] using Quiver.Hom.unop_inj hb
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X✝ : Type v₂
inst✝ : HasZeroMorphisms C
K X Y : C
i : K ⟶ X
f : X ⟶ Y
w : i ≫ f = 0
h : IsLimit (KernelFork.ofι i w)
⊢ f.op ≫ i.op = 0
[PROOFSTEP]
rw [← op_comp, w, op_zero]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X✝ : Type v₂
inst✝ : HasZeroMorphisms C
K X Y : C
i : K ⟶ X
f : X ⟶ Y
w : i ≫ f = 0
h : IsLimit (KernelFork.ofι i w)
Z'✝ : Cᵒᵖ
x : op X ⟶ Z'✝
hx : f.op ≫ x = 0
b : op K ⟶ Z'✝
hb : i.op ≫ b = x
⊢ b.unop ≫ Fork.ι (KernelFork.ofι i w) =
    ((fun {Z'} x hx => (IsLimit.lift h (KernelFork.ofι x.unop (_ : x.unop ≫ f = 0))).op) x hx).unop ≫
      Fork.ι (KernelFork.ofι i w)
[PROOFSTEP]
simpa only [Quiver.Hom.unop_op, Fork.IsLimit.lift_ι] using Quiver.Hom.op_inj hb
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X✝ : Type v₂
inst✝ : HasZeroMorphisms C
K X Y : Cᵒᵖ
i : K ⟶ X
f : X ⟶ Y
w : i ≫ f = 0
h : IsLimit (KernelFork.ofι i w)
⊢ f.unop ≫ i.unop = 0
[PROOFSTEP]
rw [← unop_comp, w, unop_zero]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X✝ : Type v₂
inst✝ : HasZeroMorphisms C
K X Y : Cᵒᵖ
i : K ⟶ X
f : X ⟶ Y
w : i ≫ f = 0
h : IsLimit (KernelFork.ofι i w)
Z'✝ : C
x : X.unop ⟶ Z'✝
hx : f.unop ≫ x = 0
b : K.unop ⟶ Z'✝
hb : i.unop ≫ b = x
⊢ b.op ≫ Fork.ι (KernelFork.ofι i w) =
    ((fun {Z'} x hx => (IsLimit.lift h (KernelFork.ofι x.op (_ : x.op ≫ f = 0))).unop) x hx).op ≫
      Fork.ι (KernelFork.ofι i w)
[PROOFSTEP]
simpa only [Quiver.Hom.op_unop, Fork.IsLimit.lift_ι] using Quiver.Hom.unop_inj hb
