case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
⊢ IsVanKampen H → IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))

case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
⊢ IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)) → IsVanKampen H
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
⊢ IsVanKampen H ↔ IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
constructor
case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔
    ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)
case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
⊢ IsVanKampen H → IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
intro H F' c' α fα eα hα
case mp.refine'_1
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)

case mp.refine'_2
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h

case mp.refine'_3
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i

case mp.refine'_4
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
    (c'.ι.app WalkingSpan.right)

case mp.refine'_5
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i ↔
    ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)
case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔
    ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)
refine' Iff.trans _
    ((H (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app _) (c'.ι.app _)
      (α.app _) (α.app _) (α.app _) fα (by convert hα WalkingSpan.Hom.fst)
      (by convert hα WalkingSpan.Hom.snd) _ _ _).trans _)
case mp.refine'_5.mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i →
    ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)

case mp.refine'_5.mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ (∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)) →
    IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
case mp.refine'_5
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i ↔
    ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)
constructor
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ IsPullback (F'.map WalkingSpan.Hom.fst) (α.app WalkingSpan.zero) (α.app WalkingSpan.left) f
convert hα WalkingSpan.Hom.fst
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ IsPullback (F'.map WalkingSpan.Hom.snd) (α.app WalkingSpan.zero) (α.app WalkingSpan.right) g
convert hα WalkingSpan.Hom.snd
case mp.refine'_1
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
case mp.refine'_1
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
have : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left =
    F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right := by
  simp only [Cocone.w]
case mp.refine'_1
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ Nonempty (IsColimit (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this)) ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)

J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (Cocones.precompose (diagramIsoSpan F').inv).obj c' ≅
    PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this
case mp.refine'_1
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
rw [(IsColimit.equivOfNatIsoOfIso (diagramIsoSpan F') c' (PushoutCocone.mk _ _ this)
      _).nonempty_congr]
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
simp only [Cocone.w]
no goals
case mp.refine'_1
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ Nonempty (IsColimit (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this)) ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
exact ⟨fun h => ⟨⟨this⟩, h⟩, fun h => h.2⟩
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ ∀ (j : WalkingSpan),
    ((Cocones.precompose (diagramIsoSpan F').inv).obj c').ι.app j ≫ (Iso.refl c'.pt).hom =
      (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app j
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (Cocones.precompose (diagramIsoSpan F').inv).obj c' ≅
    PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this
refine' Cocones.ext (Iso.refl c'.pt) _
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ ∀ (j : WalkingSpan),
    ((Cocones.precompose (diagramIsoSpan F').inv).obj c').ι.app j ≫ (Iso.refl c'.pt).hom =
      (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app j
rintro (_ | _ | _) <;> dsimp <;>
  simp only [c'.w, Category.assoc, Category.id_comp, Category.comp_id]
no goals
case mp.refine'_2
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
exact ⟨NatTrans.congr_app eα.symm _⟩
no goals
case mp.refine'_3
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
exact ⟨NatTrans.congr_app eα.symm _⟩
no goals
case mp.refine'_4
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
    (c'.ι.app WalkingSpan.right)
exact ⟨by simp⟩
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
simp
case mp.refine'_5.mp.intro.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (c'.ι.app none) (α.app none) fα ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app none)

case mp.refine'_5.mp.intro.some.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (c'.ι.app (some WalkingPair.left)) (α.app (some WalkingPair.left)) fα
    ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app (some WalkingPair.left))

case mp.refine'_5.mp.intro.some.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (c'.ι.app (some WalkingPair.right)) (α.app (some WalkingPair.right)) fα
    ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app (some WalkingPair.right))
case mp.refine'_5.mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i →
    ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)
rintro ⟨h₁, h₂⟩ (_ | _ | _)
no goals
case mp.refine'_5.mp.intro.some.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (c'.ι.app (some WalkingPair.left)) (α.app (some WalkingPair.left)) fα
    ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app (some WalkingPair.left))

case mp.refine'_5.mp.intro.some.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (c'.ι.app (some WalkingPair.right)) (α.app (some WalkingPair.right)) fα
    ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app (some WalkingPair.right))
exacts [h₁, h₂]
case mp.refine'_5.mp.intro.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left) (α.app none) fα
    ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app none)
case mp.refine'_5.mp.intro.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (c'.ι.app none) (α.app none) fα ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app none)
rw [← c'.w WalkingSpan.Hom.fst]
no goals
case mp.refine'_5.mp.intro.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left) (α.app none) fα
    ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app none)
exact (hα WalkingSpan.Hom.fst).paste_horiz h₁
case mp.refine'_5.mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h✝ : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h✝ i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h✝ i (_ : f ≫ h✝ = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h✝ i (_ : f ≫ h✝ = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h : ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h✝ i (_ : f ≫ h✝ = g ≫ i)).ι.app j)
⊢ IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h✝ ∧
    IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
case mp.refine'_5.mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ (∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)) →
    IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
intro h
no goals
case mp.refine'_5.mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h✝ : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h✝ i
H : IsVanKampen H✝
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h✝ i (_ : f ≫ h✝ = g ≫ i)).pt
eα : α ≫ (PushoutCocone.mk h✝ i (_ : f ≫ h✝ = g ≫ i)).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
h : ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h✝ i (_ : f ≫ h✝ = g ≫ i)).ι.app j)
⊢ IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h✝ ∧
    IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
exact ⟨h _, h _⟩
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
⊢ IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)) → IsVanKampen H
introv H W' hf hg hh hi w
case mpr.refine'_1
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ Nonempty (IsColimit (CommSq.cocone w))

case mpr.refine'_2
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ∀ ⦃X_1 Y_1 : WalkingSpan⦄ (f_1 : X_1 ⟶ Y_1),
    ((span f' g').map f_1 ≫ Option.casesOn Y_1 αW fun val => WalkingPair.casesOn val αX αY) =
      (Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫ (span f g).map f_1

case mpr.refine'_3
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫
      (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι =
    (CommSq.cocone w).ι ≫ (Functor.const WalkingSpan).map αZ

case mpr.refine'_4
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ NatTrans.Equifibered (NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY)

case mpr.refine'_5
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (∀ (j : WalkingSpan),
      IsPullback ((CommSq.cocone w).ι.app j)
        ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app j) αZ
        ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
refine'
  Iff.trans _ ((H w.cocone ⟨by rintro (_ | _ | _); exacts [αW, αX, αY], _⟩ αZ _ _).trans _)
case mpr.refine'_2
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ∀ ⦃X_1 Y_1 : WalkingSpan⦄ (f_1 : X_1 ⟶ Y_1),
    ((span f' g').map f_1 ≫ Option.casesOn Y_1 αW fun val => WalkingPair.casesOn val αX αY) =
      (Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫ (span f g).map f_1

case mpr.refine'_3
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫
      (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι =
    (CommSq.cocone w).ι ≫ (Functor.const WalkingSpan).map αZ

case mpr.refine'_4
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ NatTrans.Equifibered (NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY)

case mpr.refine'_5
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (∀ (j : WalkingSpan),
      IsPullback ((CommSq.cocone w).ι.app j)
        ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app j) αZ
        ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

case mpr.refine'_1
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ Nonempty (IsColimit (CommSq.cocone w))
case mpr.refine'_1
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ Nonempty (IsColimit (CommSq.cocone w))

case mpr.refine'_2
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ∀ ⦃X_1 Y_1 : WalkingSpan⦄ (f_1 : X_1 ⟶ Y_1),
    ((span f' g').map f_1 ≫ Option.casesOn Y_1 αW fun val => WalkingPair.casesOn val αX αY) =
      (Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫ (span f g).map f_1

case mpr.refine'_3
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫
      (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι =
    (CommSq.cocone w).ι ≫ (Functor.const WalkingSpan).map αZ

case mpr.refine'_4
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ NatTrans.Equifibered (NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY)

case mpr.refine'_5
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (∀ (j : WalkingSpan),
      IsPullback ((CommSq.cocone w).ι.app j)
        ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app j) αZ
        ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
rotate_left
case none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (span f' g').obj none ⟶ (span f g).obj none

case some.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (span f' g').obj (some WalkingPair.left) ⟶ (span f g).obj (some WalkingPair.left)

case some.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (span f' g').obj (some WalkingPair.right) ⟶ (span f g).obj (some WalkingPair.right)
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (X_1 : WalkingSpan) → (span f' g').obj X_1 ⟶ (span f g).obj X_1
rintro (_ | _ | _)
no goals
case none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (span f' g').obj none ⟶ (span f g).obj none

case some.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (span f' g').obj (some WalkingPair.left) ⟶ (span f g).obj (some WalkingPair.left)

case some.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (span f' g').obj (some WalkingPair.right) ⟶ (span f g).obj (some WalkingPair.right)
exacts [αW, αX, αY]
case mpr.refine'_2.id
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ (_ : f ≫ h = g ≫ i✝))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ ((span f' g').map (WidePushoutShape.Hom.id i) ≫ Option.casesOn i αW fun val => WalkingPair.casesOn val αX αY) =
    (Option.casesOn i αW fun val => WalkingPair.casesOn val αX αY) ≫ (span f g).map (WidePushoutShape.Hom.id i)

case mpr.refine'_2.init.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.left) ≫
      Option.casesOn (some WalkingPair.left) αW fun val => WalkingPair.casesOn val αX αY) =
    (Option.casesOn none αW fun val => WalkingPair.casesOn val αX αY) ≫
      (span f g).map (WidePushoutShape.Hom.init WalkingPair.left)

case mpr.refine'_2.init.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.right) ≫
      Option.casesOn (some WalkingPair.right) αW fun val => WalkingPair.casesOn val αX αY) =
    (Option.casesOn none αW fun val => WalkingPair.casesOn val αX αY) ≫
      (span f g).map (WidePushoutShape.Hom.init WalkingPair.right)
case mpr.refine'_2
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ∀ ⦃X_1 Y_1 : WalkingSpan⦄ (f_1 : X_1 ⟶ Y_1),
    ((span f' g').map f_1 ≫ Option.casesOn Y_1 αW fun val => WalkingPair.casesOn val αX αY) =
      (Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫ (span f g).map f_1
rintro i _ (_ | _ | _)
no goals
case mpr.refine'_2.init.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.left) ≫
      Option.casesOn (some WalkingPair.left) αW fun val => WalkingPair.casesOn val αX αY) =
    (Option.casesOn none αW fun val => WalkingPair.casesOn val αX αY) ≫
      (span f g).map (WidePushoutShape.Hom.init WalkingPair.left)

case mpr.refine'_2.init.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.right) ≫
      Option.casesOn (some WalkingPair.right) αW fun val => WalkingPair.casesOn val αX αY) =
    (Option.casesOn none αW fun val => WalkingPair.casesOn val αX αY) ≫
      (span f g).map (WidePushoutShape.Hom.init WalkingPair.right)
exacts [hf.w, hg.w]
case mpr.refine'_2.id
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ (_ : f ≫ h = g ≫ i✝))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ (span f' g').map (𝟙 i) ≫ Option.rec αW (fun val => WalkingPair.rec αX αY val) i =
    Option.rec αW (fun val => WalkingPair.rec αX αY val) i ≫ (span f g).map (𝟙 i)
case mpr.refine'_2.id
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ (_ : f ≫ h = g ≫ i✝))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ ((span f' g').map (WidePushoutShape.Hom.id i) ≫ Option.casesOn i αW fun val => WalkingPair.casesOn val αX αY) =
    (Option.casesOn i αW fun val => WalkingPair.casesOn val αX αY) ≫ (span f g).map (WidePushoutShape.Hom.id i)
dsimp
no goals
case mpr.refine'_2.id
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ (_ : f ≫ h = g ≫ i✝))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ (span f' g').map (𝟙 i) ≫ Option.rec αW (fun val => WalkingPair.rec αX αY val) i =
    Option.rec αW (fun val => WalkingPair.rec αX αY val) i ≫ (span f g).map (𝟙 i)
simp only [Functor.map_id, Category.comp_id, Category.id_comp]
case mpr.refine'_3.w.h.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫
          (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι).app
      none =
    ((CommSq.cocone w).ι ≫ (Functor.const WalkingSpan).map αZ).app none

case mpr.refine'_3.w.h.some.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫
          (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι).app
      (some WalkingPair.left) =
    ((CommSq.cocone w).ι ≫ (Functor.const WalkingSpan).map αZ).app (some WalkingPair.left)

case mpr.refine'_3.w.h.some.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫
          (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι).app
      (some WalkingPair.right) =
    ((CommSq.cocone w).ι ≫ (Functor.const WalkingSpan).map αZ).app (some WalkingPair.right)
case mpr.refine'_3
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫
      (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι =
    (CommSq.cocone w).ι ≫ (Functor.const WalkingSpan).map αZ
ext (_ | _ | _)
no goals
case mpr.refine'_3.w.h.some.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫
          (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι).app
      (some WalkingPair.left) =
    ((CommSq.cocone w).ι ≫ (Functor.const WalkingSpan).map αZ).app (some WalkingPair.left)

case mpr.refine'_3.w.h.some.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫
          (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι).app
      (some WalkingPair.right) =
    ((CommSq.cocone w).ι ≫ (Functor.const WalkingSpan).map αZ).app (some WalkingPair.right)
exacts [hh.w.symm, hi.w.symm]
case mpr.refine'_3.w.h.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ αW ≫ f ≫ h = (CommSq.cocone w).ι.app none ≫ αZ
case mpr.refine'_3.w.h.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY) ≫
          (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι).app
      none =
    ((CommSq.cocone w).ι ≫ (Functor.const WalkingSpan).map αZ).app none
dsimp
case mpr.refine'_3.w.h.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ αW ≫ f ≫ h = (f' ≫ PushoutCocone.inl (CommSq.cocone w)) ≫ αZ
case mpr.refine'_3.w.h.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ αW ≫ f ≫ h = (CommSq.cocone w).ι.app none ≫ αZ
rw [PushoutCocone.condition_zero]
no goals
case mpr.refine'_3.w.h.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ αW ≫ f ≫ h = (f' ≫ PushoutCocone.inl (CommSq.cocone w)) ≫ αZ
erw [Category.assoc, hh.w, hf.w_assoc]
case mpr.refine'_4.id
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ (_ : f ≫ h = g ≫ i✝))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ IsPullback ((span f' g').map (WidePushoutShape.Hom.id i))
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app i)
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app i)
    ((span f g).map (WidePushoutShape.Hom.id i))

case mpr.refine'_4.init.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPullback ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.left))
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app none)
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app
      (some WalkingPair.left))
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left))

case mpr.refine'_4.init.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPullback ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.right))
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app none)
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app
      (some WalkingPair.right))
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right))
case mpr.refine'_4
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ NatTrans.Equifibered (NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY)
rintro i _ (_ | _ | _)
no goals
case mpr.refine'_4.init.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPullback ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.left))
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app none)
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app
      (some WalkingPair.left))
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left))

case mpr.refine'_4.init.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPullback ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.right))
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app none)
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app
      (some WalkingPair.right))
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right))
exacts [hf, hg]
case mpr.refine'_4.id
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ (_ : f ≫ h = g ≫ i✝))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ IsPullback ((span f' g').map (𝟙 i)) (Option.rec αW (fun val => WalkingPair.rec αX αY val) i)
    (Option.rec αW (fun val => WalkingPair.rec αX αY val) i) ((span f g).map (𝟙 i))
case mpr.refine'_4.id
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ (_ : f ≫ h = g ≫ i✝))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ IsPullback ((span f' g').map (WidePushoutShape.Hom.id i))
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app i)
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app i)
    ((span f g).map (WidePushoutShape.Hom.id i))
dsimp
case mpr.refine'_4.id
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ (_ : f ≫ h = g ≫ i✝))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ IsPullback (𝟙 ((span f' g').obj i)) (Option.rec αW (fun val => WalkingPair.rec αX αY val) i)
    (Option.rec αW (fun val => WalkingPair.rec αX αY val) i) (𝟙 ((span f g).obj i))
case mpr.refine'_4.id
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ (_ : f ≫ h = g ≫ i✝))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ IsPullback ((span f' g').map (𝟙 i)) (Option.rec αW (fun val => WalkingPair.rec αX αY val) i)
    (Option.rec αW (fun val => WalkingPair.rec αX αY val) i) ((span f g).map (𝟙 i))
simp_rw [Functor.map_id]
no goals
case mpr.refine'_4.id
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ (_ : f ≫ h = g ≫ i✝))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ IsPullback (𝟙 ((span f' g').obj i)) (Option.rec αW (fun val => WalkingPair.rec αX αY val) i)
    (Option.rec αW (fun val => WalkingPair.rec αX αY val) i) (𝟙 ((span f g).obj i))
exact IsPullback.of_horiz_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ (_ : f ≫ h = g ≫ i✝))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ 𝟙 ((span f' g').obj i) ≫ Option.rec αW (fun val => WalkingPair.rec αX αY val) i =
    Option.rec αW (fun val => WalkingPair.rec αX αY val) i ≫ 𝟙 ((span f g).obj i)
rw [Category.comp_id, Category.id_comp]
case mpr.refine'_5.mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (∀ (j : WalkingSpan),
      IsPullback ((CommSq.cocone w).ι.app j)
        ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app j) αZ
        ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)) →
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

case mpr.refine'_5.mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i →
    ∀ (j : WalkingSpan),
      IsPullback ((CommSq.cocone w).ι.app j)
        ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app j) αZ
        ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)
case mpr.refine'_5
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (∀ (j : WalkingSpan),
      IsPullback ((CommSq.cocone w).ι.app j)
        ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app j) αZ
        ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
constructor
case mpr.refine'_5.mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h✝ : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h✝ i
H : IsVanKampenColimit (PushoutCocone.mk h✝ i (_ : f ≫ h✝ = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h✝
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h :
  ∀ (j : WalkingSpan),
    IsPullback ((CommSq.cocone w).ι.app j)
      ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app j) αZ
      ((PushoutCocone.mk h✝ i (_ : f ≫ h✝ = g ≫ i)).ι.app j)
⊢ IsPullback h' αX αZ h✝ ∧ IsPullback i' αY αZ i
case mpr.refine'_5.mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (∀ (j : WalkingSpan),
      IsPullback ((CommSq.cocone w).ι.app j)
        ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app j) αZ
        ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)) →
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
intro h
no goals
case mpr.refine'_5.mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h✝ : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h✝ i
H : IsVanKampenColimit (PushoutCocone.mk h✝ i (_ : f ≫ h✝ = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h✝
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h :
  ∀ (j : WalkingSpan),
    IsPullback ((CommSq.cocone w).ι.app j)
      ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app j) αZ
      ((PushoutCocone.mk h✝ i (_ : f ≫ h✝ = g ≫ i)).ι.app j)
⊢ IsPullback h' αX αZ h✝ ∧ IsPullback i' αY αZ i
exact ⟨h WalkingCospan.left, h WalkingCospan.right⟩
case mpr.refine'_5.mpr.intro.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback ((CommSq.cocone w).ι.app none)
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app none) αZ
    ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app none)

case mpr.refine'_5.mpr.intro.some.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback ((CommSq.cocone w).ι.app (some WalkingPair.left))
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app
      (some WalkingPair.left))
    αZ ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app (some WalkingPair.left))

case mpr.refine'_5.mpr.intro.some.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback ((CommSq.cocone w).ι.app (some WalkingPair.right))
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app
      (some WalkingPair.right))
    αZ ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app (some WalkingPair.right))
case mpr.refine'_5.mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i →
    ∀ (j : WalkingSpan),
      IsPullback ((CommSq.cocone w).ι.app j)
        ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app j) αZ
        ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app j)
rintro ⟨h₁, h₂⟩ (_ | _ | _)
no goals
case mpr.refine'_5.mpr.intro.some.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback ((CommSq.cocone w).ι.app (some WalkingPair.left))
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app
      (some WalkingPair.left))
    αZ ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app (some WalkingPair.left))

case mpr.refine'_5.mpr.intro.some.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback ((CommSq.cocone w).ι.app (some WalkingPair.right))
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app
      (some WalkingPair.right))
    αZ ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app (some WalkingPair.right))
exacts [h₁, h₂]
case mpr.refine'_5.mpr.intro.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback ((CommSq.cocone w).ι.app none) αW αZ (f ≫ h)
case mpr.refine'_5.mpr.intro.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback ((CommSq.cocone w).ι.app none)
    ((NatTrans.mk fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY).app none) αZ
    ((PushoutCocone.mk h i (_ : f ≫ h = g ≫ i)).ι.app none)
dsimp
case mpr.refine'_5.mpr.intro.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback (f' ≫ PushoutCocone.inl (CommSq.cocone w)) αW αZ (f ≫ h)
case mpr.refine'_5.mpr.intro.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback ((CommSq.cocone w).ι.app none) αW αZ (f ≫ h)
rw [PushoutCocone.condition_zero]
no goals
case mpr.refine'_5.mpr.intro.none
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback (f' ≫ PushoutCocone.inl (CommSq.cocone w)) αW αZ (f ≫ h)
exact hf.paste_horiz h₁
no goals
case mpr.refine'_1
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i (_ : f ≫ h = g ≫ i))
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ Nonempty (IsColimit (CommSq.cocone w))
exact ⟨fun h => h.2, fun h => ⟨w, h⟩⟩