J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c'') ↔ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
⊢ IsVanKampenColimit c'
intro F' c'' α f h hα
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
⊢ Nonempty (IsColimit c'') ↔ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c'') ↔ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
have : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι := by
  ext j
  exact e.inv.2 j
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
⊢ (∀ (j : J), IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.Hom) (c.ι.app j)) ↔
    ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
⊢ Nonempty (IsColimit c'') ↔ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
rw [H c'' α (f ≫ e.inv.1) (by rw [Functor.map_comp, ← reassoc_of% h, this]) hα]
case h
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
⊢ ∀ (a : J),
    IsPullback (c''.ι.app a) (α.app a) (f ≫ e.inv.Hom) (c.ι.app a) ↔ IsPullback (c''.ι.app a) (α.app a) f (c'.ι.app a)
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
⊢ (∀ (j : J), IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.Hom) (c.ι.app j)) ↔
    ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
apply forall_congr'
case h
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.Hom) (c.ι.app j) ↔ IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
case h
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
⊢ ∀ (a : J),
    IsPullback (c''.ι.app a) (α.app a) (f ≫ e.inv.Hom) (c.ι.app a) ↔ IsPullback (c''.ι.app a) (α.app a) f (c'.ι.app a)
intro j
case h
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.Hom) (c.ι.app j) ↔
    IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
case h
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.Hom) (c.ι.app j) ↔ IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
conv_lhs => rw [← Category.comp_id (α.app j)]
case h
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this✝ : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
j : J
this : IsIso e.inv.Hom
⊢ IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.Hom) (c.ι.app j) ↔
    IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
case h
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.Hom) (c.ι.app j) ↔
    IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
haveI : IsIso e.inv.Hom := Functor.map_isIso (Cocones.forget _) e.inv
no goals
case h
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this✝ : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
j : J
this : IsIso e.inv.Hom
⊢ IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.Hom) (c.ι.app j) ↔
    IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
exact (IsPullback.of_vert_isIso ⟨by simp⟩).paste_vert_iff (NatTrans.congr_app h j).symm
case w.h
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
j : J
⊢ (c'.ι ≫ (Functor.const J).map e.inv.Hom).app j = c.ι.app j
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
⊢ c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
ext j
no goals
case w.h
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
j : J
⊢ (c'.ι ≫ (Functor.const J).map e.inv.Hom).app j = c.ι.app j
exact e.inv.2 j
no goals
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
⊢ α ≫ c.ι = c''.ι ≫ (Functor.const J).map (f ≫ e.inv.Hom)
rw [Functor.map_comp, ← reassoc_of% h, this]
no goals
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
D : Type u''
inst✝ : Category D
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this✝ : c'.ι ≫ (Functor.const J).map e.inv.Hom = c.ι
j : J
this : IsIso e.inv.Hom
⊢ c'.ι.app j ≫ e.inv.Hom = 𝟙 (F.obj j) ≫ c.ι.app j
simp