J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
⊢ (fun x => { down := ∃ j y, t.ι.app j y = x }) = fun x => { down := True }
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
⊢ ∃ j y, t.ι.app j y = x
suffices (fun x : t.pt => ULift.up (∃ j y, t.ι.app j y = x)) = fun _ => ULift.up.{max v u} True by
  have := congr_fun this x
  simpa using congr_arg ULift.down this
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
⊢ ∀ (j : J), (t.ι.app j ≫ fun x => { down := ∃ j y, t.ι.app j y = x }) = t.ι.app j ≫ fun x => { down := True }
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
⊢ (fun x => { down := ∃ j y, t.ι.app j y = x }) = fun x => { down := True }
refine' h.hom_ext _
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
j : J
⊢ (t.ι.app j ≫ fun x => { down := ∃ j y, t.ι.app j y = x }) = t.ι.app j ≫ fun x => { down := True }
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
⊢ ∀ (j : J), (t.ι.app j ≫ fun x => { down := ∃ j y, t.ι.app j y = x }) = t.ι.app j ≫ fun x => { down := True }
intro j
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
j : J
y : F.obj j
⊢ (t.ι.app j ≫ fun x => { down := ∃ j y, t.ι.app j y = x }) y = (t.ι.app j ≫ fun x => { down := True }) y
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
j : J
⊢ (t.ι.app j ≫ fun x => { down := ∃ j y, t.ι.app j y = x }) = t.ι.app j ≫ fun x => { down := True }
funext y
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
j : J
y : F.obj j
⊢ ∃ j_1 y_1, t.ι.app j_1 y_1 = t.ι.app j y
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
j : J
y : F.obj j
⊢ (t.ι.app j ≫ fun x => { down := ∃ j y, t.ι.app j y = x }) y = (t.ι.app j ≫ fun x => { down := True }) y
simp only [Functor.const_obj_obj, types_comp_apply, ULift.up_inj, eq_iff_iff, iff_true]
no goals
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
j : J
y : F.obj j
⊢ ∃ j_1 y_1, t.ι.app j_1 y_1 = t.ι.app j y
exact ⟨j, y, rfl⟩
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
this✝ : (fun x => { down := ∃ j y, t.ι.app j y = x }) = fun x => { down := True }
this : { down := ∃ j y, t.ι.app j y = x } = { down := True }
⊢ ∃ j y, t.ι.app j y = x
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
this : (fun x => { down := ∃ j y, t.ι.app j y = x }) = fun x => { down := True }
⊢ ∃ j y, t.ι.app j y = x
have := congr_fun this x
no goals
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
this✝ : (fun x => { down := ∃ j y, t.ι.app j y = x }) = fun x => { down := True }
this : { down := ∃ j y, t.ι.app j y = x } = { down := True }
⊢ ∃ j y, t.ι.app j y = x
simpa using congr_arg ULift.down this