case refine'_1
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ mapPair (initial.to X) (𝟙 Y) ≫ c.ι =
    (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (Functor.const (Discrete WalkingPair)).map (BinaryCofan.inr c)

case refine'_2
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsPullback (initial.to ((pair X Y).obj { as := WalkingPair.left }))
    (initial.to ((pair X Y).obj { as := WalkingPair.right })) (BinaryCofan.inl c) (BinaryCofan.inr c)
refine' ((h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr _
    (mapPair_equifibered _)).mp ⟨_⟩ ⟨WalkingPair.left⟩).flip
case refine'_1.w.h.mk.left
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ initial.to X ≫ BinaryCofan.inl c = initial.to Y ≫ BinaryCofan.inr c
case refine'_1
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ mapPair (initial.to X) (𝟙 Y) ≫ c.ι =
    (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (Functor.const (Discrete WalkingPair)).map (BinaryCofan.inr c)
ext ⟨⟨⟩⟩ <;> dsimp
no goals
case refine'_1.w.h.mk.left
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ initial.to X ≫ BinaryCofan.inl c = initial.to Y ≫ BinaryCofan.inr c
simp
no goals
case refine'_2
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))
exact ((BinaryCofan.isColimit_iff_isIso_inr initialIsInitial _).mpr (by
  dsimp
  infer_instance)).some
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsIso (𝟙 Y)
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsIso (BinaryCofan.inr (BinaryCofan.mk (initial.to Y) (𝟙 Y)))
dsimp
no goals
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsIso (𝟙 Y)
infer_instance