case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
⊢ IsVanKampenColimit c →
    ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
        αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
          (Nonempty (IsColimit c') ↔
            IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
              IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))

case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
⊢ (∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
        αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
          (Nonempty (IsColimit c') ↔
            IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
              IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))) →
    IsVanKampenColimit c
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
⊢ IsVanKampenColimit c ↔
    ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
        αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
          (Nonempty (IsColimit c') ↔
            IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
              IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
constructor
case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ Nonempty (IsColimit c') ↔
    IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
⊢ IsVanKampenColimit c →
    ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
        αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
          (Nonempty (IsColimit c') ↔
            IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
              IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
introv H hαX hαY
case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)) ↔
    IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ Nonempty (IsColimit c') ↔
    IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
rw [H c' (mapPair αX αY) f (by ext ⟨⟨⟩⟩ <;> dsimp <;> assumption) (mapPair_equifibered _)]
case mp.mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)) →
    IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)

case mp.mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c) →
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)
case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)) ↔
    IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
constructor
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ mapPair αX αY ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
ext ⟨⟨⟩⟩ <;> dsimp <;> assumption
case mp.mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H✝ : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H : ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
case mp.mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)) →
    IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
intro H
no goals
case mp.mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H✝ : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H : ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
exact ⟨H _, H _⟩
case mp.mpr.mk.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H✝ : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
⊢ IsPullback (c'.ι.app { as := WalkingPair.left }) ((mapPair αX αY).app { as := WalkingPair.left }) f
    (c.ι.app { as := WalkingPair.left })

case mp.mpr.mk.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H✝ : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
⊢ IsPullback (c'.ι.app { as := WalkingPair.right }) ((mapPair αX αY).app { as := WalkingPair.right }) f
    (c.ι.app { as := WalkingPair.right })
case mp.mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c) →
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)
rintro H ⟨⟨⟩⟩
no goals
case mp.mpr.mk.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H✝ : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
⊢ IsPullback (c'.ι.app { as := WalkingPair.left }) ((mapPair αX αY).app { as := WalkingPair.left }) f
    (c.ι.app { as := WalkingPair.left })

case mp.mpr.mk.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H✝ : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hαY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
⊢ IsPullback (c'.ι.app { as := WalkingPair.right }) ((mapPair αX αY).app { as := WalkingPair.right }) f
    (c.ι.app { as := WalkingPair.right })
exacts [H.1, H.2]
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
⊢ (∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
        αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
          (Nonempty (IsColimit c') ↔
            IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
              IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))) →
    IsVanKampenColimit c
introv H F' hα h
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
let X' := F'.obj ⟨WalkingPair.left⟩
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
let Y' := F'.obj ⟨WalkingPair.right⟩
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
Y' X' : C
this : F' = pair X' Y'
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
this : F' = pair X' Y'
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
clear_value X' Y'
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
c' : Cocone (pair X' Y')
α : pair X' Y' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
Y' X' : C
this : F' = pair X' Y'
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
subst this
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
c' : Cocone (pair X' Y')
α : pair X' Y' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
change BinaryCofan X' Y' at c'
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
⊢ IsPullback (BinaryCofan.inl c') (α.app { as := WalkingPair.left })
        (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inl c) ∧
      IsPullback (BinaryCofan.inr c') (α.app { as := WalkingPair.right })
        (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inr c) ↔
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
rw [H c' _ _ _ (NatTrans.congr_app hα ⟨WalkingPair.left⟩)
    (NatTrans.congr_app hα ⟨WalkingPair.right⟩)]
case mpr.mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
⊢ IsPullback (BinaryCofan.inl c') (α.app { as := WalkingPair.left })
        (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inl c) ∧
      IsPullback (BinaryCofan.inr c') (α.app { as := WalkingPair.right })
        (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inr c) →
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

case mpr.mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) →
    IsPullback (BinaryCofan.inl c') (α.app { as := WalkingPair.left })
        (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inl c) ∧
      IsPullback (BinaryCofan.inr c') (α.app { as := WalkingPair.right })
        (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inr c)
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
⊢ IsPullback (BinaryCofan.inl c') (α.app { as := WalkingPair.left })
        (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inl c) ∧
      IsPullback (BinaryCofan.inr c') (α.app { as := WalkingPair.right })
        (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inr c) ↔
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
constructor
case h_obj
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ ∀ (X : Discrete WalkingPair), F'.obj X = (pair X' Y').obj X

case h_map
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ ∀ (X Y : Discrete WalkingPair) (f : X ⟶ Y), HEq (F'.map f) ((pair X' Y').map f)
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ F' = pair X' Y'
apply Functor.hext
no goals
case h_obj
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ ∀ (X : Discrete WalkingPair), F'.obj X = (pair X' Y').obj X
rintro ⟨⟨⟩⟩ <;> rfl
no goals
case h_map
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ ∀ (X Y : Discrete WalkingPair) (f : X ⟶ Y), HEq (F'.map f) ((pair X' Y').map f)
rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp
case mpr.mp.mk.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H✝ :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
H :
  IsPullback (BinaryCofan.inl c') (α.app { as := WalkingPair.left })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inl c) ∧
    IsPullback (BinaryCofan.inr c') (α.app { as := WalkingPair.right })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inr c)
⊢ IsPullback (c'.ι.app { as := WalkingPair.left }) (α.app { as := WalkingPair.left }) f
    (c.ι.app { as := WalkingPair.left })

case mpr.mp.mk.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H✝ :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
H :
  IsPullback (BinaryCofan.inl c') (α.app { as := WalkingPair.left })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inl c) ∧
    IsPullback (BinaryCofan.inr c') (α.app { as := WalkingPair.right })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inr c)
⊢ IsPullback (c'.ι.app { as := WalkingPair.right }) (α.app { as := WalkingPair.right }) f
    (c.ι.app { as := WalkingPair.right })
case mpr.mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
⊢ IsPullback (BinaryCofan.inl c') (α.app { as := WalkingPair.left })
        (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inl c) ∧
      IsPullback (BinaryCofan.inr c') (α.app { as := WalkingPair.right })
        (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inr c) →
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
rintro H ⟨⟨⟩⟩
no goals
case mpr.mp.mk.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H✝ :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
H :
  IsPullback (BinaryCofan.inl c') (α.app { as := WalkingPair.left })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inl c) ∧
    IsPullback (BinaryCofan.inr c') (α.app { as := WalkingPair.right })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inr c)
⊢ IsPullback (c'.ι.app { as := WalkingPair.left }) (α.app { as := WalkingPair.left }) f
    (c.ι.app { as := WalkingPair.left })

case mpr.mp.mk.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H✝ :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
H :
  IsPullback (BinaryCofan.inl c') (α.app { as := WalkingPair.left })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inl c) ∧
    IsPullback (BinaryCofan.inr c') (α.app { as := WalkingPair.right })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inr c)
⊢ IsPullback (c'.ι.app { as := WalkingPair.right }) (α.app { as := WalkingPair.right }) f
    (c.ι.app { as := WalkingPair.right })
exacts [H.1, H.2]
case mpr.mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H✝ :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
H : ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ IsPullback (BinaryCofan.inl c') (α.app { as := WalkingPair.left })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inl c) ∧
    IsPullback (BinaryCofan.inr c') (α.app { as := WalkingPair.right })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inr c)
case mpr.mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) →
    IsPullback (BinaryCofan.inl c') (α.app { as := WalkingPair.left })
        (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inl c) ∧
      IsPullback (BinaryCofan.inr c') (α.app { as := WalkingPair.right })
        (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inr c)
intro H
no goals
case mpr.mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X Y : C
c : BinaryCofan X Y
H✝ :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
H : ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ IsPullback (BinaryCofan.inl c') (α.app { as := WalkingPair.left })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inl c) ∧
    IsPullback (BinaryCofan.inr c') (α.app { as := WalkingPair.right })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) (BinaryCofan.inr c)
exact ⟨H _, H _⟩