case intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
⊢ 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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
⊢ IsVanKampen H
obtain ⟨hc₁⟩ := (is_coprod_iff_isPushout c hc H.1).mpr H
case intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
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 intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
⊢ IsVanKampen H
introv W' hf hg hh hi w
case intro.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
case intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
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
obtain ⟨hc₂⟩ := ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen c hc)
  (BinaryCofan.mk _ pullback.fst) _ _ _ hg.w.symm pullback.condition.symm).mpr
  ⟨hg, IsPullback.of_hasPullback αY c.inr⟩
case intro.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ Nonempty (IsColimit (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
case intro.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
refine' (is_coprod_iff_isPushout _ hc₂ w).symm.trans _
case intro.intro.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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ pullback.snd ≫ BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h) =
    BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h') ≫ αZ

case intro.intro.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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
        αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)) ∧
      IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
        (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
case intro.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ Nonempty (IsColimit (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
refine' ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen _ hc₁)
  (BinaryCofan.mk _ _) pullback.snd _ _ _ hh.w.symm).trans _
case intro.intro.refine'_2.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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
        αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)) ∧
      IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
        (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)) →
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

case intro.intro.refine'_2.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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i →
    IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h'))
        pullback.snd αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)) ∧
      IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
        (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
case intro.intro.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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
        αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)) ∧
      IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
        (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
constructor
case intro.intro.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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ pullback.snd ≫ BinaryCofan.inr c ≫ i = (pullback.fst ≫ i') ≫ αZ
case intro.intro.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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ pullback.snd ≫ BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h) =
    BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h') ≫ αZ
dsimp
no goals
case intro.intro.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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ pullback.snd ≫ BinaryCofan.inr c ≫ i = (pullback.fst ≫ i') ≫ αZ
rw [← pullback.condition_assoc, Category.assoc, hi.w]
case intro.intro.refine'_2.mp.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
case intro.intro.refine'_2.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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
        αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)) ∧
      IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
        (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)) →
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
rintro ⟨hc₃, hc₄⟩
case intro.intro.refine'_2.mp.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
⊢ IsPullback i' αY αZ i
case intro.intro.refine'_2.mp.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
refine' ⟨hc₄, _⟩
case intro.intro.refine'_2.mp.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
⊢ IsPullback i' αY αZ i
case intro.intro.refine'_2.mp.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
⊢ IsPullback i' αY αZ i
let Y'' := pullback αZ i
case intro.intro.refine'_2.mp.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
⊢ IsPullback i' αY αZ i
case intro.intro.refine'_2.mp.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
⊢ IsPullback i' αY αZ i
let cmp : Y' ⟶ Y'' := pullback.lift i' αY hi.w
case intro.intro.refine'_2.mp.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
⊢ IsPullback i' αY αZ i
case intro.intro.refine'_2.mp.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
⊢ IsPullback i' αY αZ i
have e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ c.inl := by
  rw [Category.assoc, pullback.lift_snd, hg.w]
case intro.intro.refine'_2.mp.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback i' αY αZ i
case intro.intro.refine'_2.mp.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
⊢ IsPullback i' αY αZ i
have e₂ : (pullback.fst ≫ cmp : pullback αY c.inr ⟶ _) ≫ pullback.snd = pullback.snd ≫ c.inr :=
  by rw [Category.assoc, pullback.lift_snd, pullback.condition]
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
⊢ (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
rw [Category.assoc, pullback.lift_snd, hg.w]
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
⊢ (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
rw [Category.assoc, pullback.lift_snd, pullback.condition]
case 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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))) αW pullback.snd (BinaryCofan.inl c)

case 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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback (BinaryCofan.inr (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))) pullback.snd pullback.snd
    (BinaryCofan.inr c)
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))) αW pullback.snd (BinaryCofan.inl c) ∧
    IsPullback (BinaryCofan.inr (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))) pullback.snd pullback.snd
      (BinaryCofan.inr c)
constructor
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback ((g' ≫ cmp) ≫ pullback.fst) αW αZ (BinaryCofan.inl c ≫ i)
case 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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))) αW pullback.snd (BinaryCofan.inl c)
apply IsPullback.of_right _ e₁ (IsPullback.of_hasPullback _ _)
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback (f' ≫ h') αW αZ (f ≫ 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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback ((g' ≫ cmp) ≫ pullback.fst) αW αZ (BinaryCofan.inl c ≫ i)
rw [Category.assoc, pullback.lift_fst, ← H.w, ← w.w]
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback (f' ≫ h') αW αZ (f ≫ h)
exact hf.paste_horiz hc₄
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback ((pullback.fst ≫ cmp) ≫ pullback.fst) pullback.snd αZ (BinaryCofan.inr c ≫ i)
case 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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback (BinaryCofan.inr (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))) pullback.snd pullback.snd
    (BinaryCofan.inr c)
apply IsPullback.of_right _ e₂ (IsPullback.of_hasPullback _ _)
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback (pullback.fst ≫ i') pullback.snd αZ (BinaryCofan.inr c ≫ i)
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback ((pullback.fst ≫ cmp) ≫ pullback.fst) pullback.snd αZ (BinaryCofan.inr c ≫ i)
rw [Category.assoc, pullback.lift_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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
⊢ IsPullback (pullback.fst ≫ i') pullback.snd αZ (BinaryCofan.inr c ≫ i)
exact hc₃
case intro.intro.refine'_2.mp.intro.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
⊢ IsPullback i' (cmp ≫ pullback.snd) (𝟙 Z' ≫ αZ) i
case intro.intro.refine'_2.mp.intro.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
⊢ IsPullback i' αY αZ i
rw [← Category.id_comp αZ, ← show cmp ≫ pullback.snd = αY from pullback.lift_snd _ _ _]
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
⊢ IsPullback i' cmp (𝟙 Z') pullback.fst
case intro.intro.refine'_2.mp.intro.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
⊢ IsPullback i' (cmp ≫ pullback.snd) (𝟙 Z' ≫ αZ) i
apply IsPullback.paste_vert _ (IsPullback.of_hasPullback αZ i)
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
this : cmp = (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom
⊢ IsPullback i' cmp (𝟙 Z') pullback.fst
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
⊢ IsPullback i' cmp (𝟙 Z') pullback.fst
have : cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom := by
  apply BinaryCofan.IsColimit.hom_ext hc₂
  exacts [(hc₂.comp_coconePointUniqueUpToIso_hom hc₄ ⟨WalkingPair.left⟩).symm,
    (hc₂.comp_coconePointUniqueUpToIso_hom hc₄ ⟨WalkingPair.right⟩).symm]
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
this : cmp = (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom
⊢ IsPullback i' (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom (𝟙 Z') pullback.fst
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
this : cmp = (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom
⊢ IsPullback i' cmp (𝟙 Z') pullback.fst
rw [this]
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
this : cmp = (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom
⊢ IsPullback i' (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom (𝟙 Z') pullback.fst
exact IsPullback.of_vert_isIso ⟨by rw [← this, Category.comp_id, pullback.lift_fst]⟩
case 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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
⊢ BinaryCofan.inl (BinaryCofan.mk g' pullback.fst) ≫ cmp =
    BinaryCofan.inl (BinaryCofan.mk g' pullback.fst) ≫ (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom

case 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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
⊢ BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ cmp =
    BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
⊢ cmp = (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom
apply BinaryCofan.IsColimit.hom_ext hc₂
no goals
case 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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
⊢ BinaryCofan.inl (BinaryCofan.mk g' pullback.fst) ≫ cmp =
    BinaryCofan.inl (BinaryCofan.mk g' pullback.fst) ≫ (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom

case 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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
⊢ BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ cmp =
    BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom
exacts [(hc₂.comp_coconePointUniqueUpToIso_hom hc₄ ⟨WalkingPair.left⟩).symm,
  (hc₂.comp_coconePointUniqueUpToIso_hom hc₄ ⟨WalkingPair.right⟩).symm]
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ :
  IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
    αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
hc₄✝ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
    (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY (_ : i' ≫ αZ = αY ≫ i)
e₁ : (g' ≫ cmp) ≫ pullback.snd = αW ≫ BinaryCofan.inl c
e₂ : (pullback.fst ≫ cmp) ≫ pullback.snd = pullback.snd ≫ BinaryCofan.inr c
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst ≫ cmp))
this : cmp = (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom
⊢ i' ≫ 𝟙 Z' = (IsColimit.coconePointUniqueUpToIso hc₂ hc₄).hom ≫ pullback.fst
rw [← this, Category.comp_id, pullback.lift_fst]
case intro.intro.refine'_2.mpr.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ : IsPullback h' αX αZ h
hc₄ : IsPullback i' αY αZ i
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
      αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)) ∧
    IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
      (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
case intro.intro.refine'_2.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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i →
    IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h'))
        pullback.snd αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)) ∧
      IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
        (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
rintro ⟨hc₃, hc₄⟩
no goals
case intro.intro.refine'_2.mpr.intro
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✝
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f (BinaryCofan.inl c) h i
hc₁ : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY (BinaryCofan.inl c)
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' pullback.fst)
hc₃ : IsPullback h' αX αZ h
hc₄ : IsPullback i' αY αZ i
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) pullback.snd
      αZ (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h)) ∧
    IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' pullback.fst) ≫ i') h')) αX αZ
      (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ i) h))
exact ⟨(IsPullback.of_hasPullback αY c.inr).paste_horiz hc₄, hc₃⟩