J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
t' : Cocone F := colimitCocone F
⊢ t.ι.app i xi = t.ι.app j xj ↔ ∃ k f g, F.map f xi = F.map g xj
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
⊢ t.ι.app i xi = t.ι.app j xj ↔ ∃ k f g, F.map f xi = F.map g xj
let t' := colimitCocone.{v, u} F
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
t' : Cocone F := colimitCocone F
e : t' ≅ t := IsColimit.uniqueUpToIso (colimitCoconeIsColimit F) ht
⊢ t.ι.app i xi = t.ι.app j xj ↔ ∃ k f g, F.map f xi = F.map g xj
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
t' : Cocone F := colimitCocone F
⊢ t.ι.app i xi = t.ι.app j xj ↔ ∃ k f g, F.map f xi = F.map g xj
let e : t' ≅ t := IsColimit.uniqueUpToIso (colimitCoconeIsColimit F) ht
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
t' : Cocone F := colimitCocone F
e : t' ≅ t := IsColimit.uniqueUpToIso (colimitCoconeIsColimit F) ht
e' : t'.pt ≅ t.pt := (Cocones.forget F).mapIso e
⊢ t.ι.app i xi = t.ι.app j xj ↔ ∃ k f g, F.map f xi = F.map g xj
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
t' : Cocone F := colimitCocone F
e : t' ≅ t := IsColimit.uniqueUpToIso (colimitCoconeIsColimit F) ht
⊢ t.ι.app i xi = t.ι.app j xj ↔ ∃ k f g, F.map f xi = F.map g xj
let e' : t'.pt ≅ t.pt := (Cocones.forget _).mapIso e
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
t' : Cocone F := colimitCocone F
e : t' ≅ t := IsColimit.uniqueUpToIso (colimitCoconeIsColimit F) ht
e' : t'.pt ≅ t.pt := (Cocones.forget F).mapIso e
⊢ t.ι.app i xi = t.ι.app j xj ↔ (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
t' : Cocone F := colimitCocone F
e : t' ≅ t := IsColimit.uniqueUpToIso (colimitCoconeIsColimit F) ht
e' : t'.pt ≅ t.pt := (Cocones.forget F).mapIso e
⊢ t.ι.app i xi = t.ι.app j xj ↔ ∃ k f g, F.map f xi = F.map g xj
refine' Iff.trans _ (colimit_eq_iff_aux.{v, u} F)
no goals
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
t' : Cocone F := colimitCocone F
e : t' ≅ t := IsColimit.uniqueUpToIso (colimitCoconeIsColimit F) ht
e' : t'.pt ≅ t.pt := (Cocones.forget F).mapIso e
⊢ t.ι.app i xi = t.ι.app j xj ↔ (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj
exact @Equiv.apply_eq_iff_eq _ _ e'.toEquiv ((colimitCocone.{v, u} F).ι.app i xi)
  ((colimitCocone.{v, u} F).ι.app j xj)