J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X✝ Y : C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
⊢ IsVanKampenColimit c
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsVanKampenColimit c
let X := F.obj ⟨WalkingPair.left⟩
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X✝ Y✝ : C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
⊢ IsVanKampenColimit c
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X✝ Y : C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
⊢ IsVanKampenColimit c
let Y := F.obj ⟨WalkingPair.right⟩
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X✝ Y✝ : C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
Y X : C
this : F = pair X Y
⊢ IsVanKampenColimit c
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X✝ Y✝ : C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
this : F = pair X Y
⊢ IsVanKampenColimit c
clear_value X Y
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X✝ Y✝ : C
inst✝ : FinitaryExtensive C
Y X : C
c : Cocone (pair X Y)
hc : IsColimit c
⊢ IsVanKampenColimit c
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X✝ Y✝ : C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
Y X : C
this : F = pair X Y
⊢ IsVanKampenColimit c
subst this
no goals
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X✝ Y✝ : C
inst✝ : FinitaryExtensive C
Y X : C
c : Cocone (pair X Y)
hc : IsColimit c
⊢ IsVanKampenColimit c
exact FinitaryExtensive.van_kampen' c hc
case h_obj
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X✝ Y✝ : C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
⊢ ∀ (X_1 : Discrete WalkingPair), F.obj X_1 = (pair X Y).obj X_1

case h_map
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X✝ Y✝ : C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
⊢ ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1), HEq (F.map f) ((pair X Y).map f)
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X✝ Y✝ : C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
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
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
⊢ ∀ (X_1 : Discrete WalkingPair), F.obj X_1 = (pair X Y).obj X_1
rintro ⟨⟨⟩⟩ <;> rfl
no goals
case h_map
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X✝ Y✝ : C
inst✝ : FinitaryExtensive C
F : Discrete WalkingPair ⥤ C
c : Cocone F
hc : IsColimit c
X : C := F.obj { as := WalkingPair.left }
Y : C := F.obj { as := WalkingPair.right }
⊢ ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1), HEq (F.map f) ((pair X Y).map f)
rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp