[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (Shrink ↑(Functor.sections F))).map f ≫
      (fun j u => ↑(↑(equivShrink ↑(Functor.sections F)).symm u) j) j' =
    (fun j u => ↑(↑(equivShrink ↑(Functor.sections F)).symm u) j) j ≫ F.map f
[PROOFSTEP]
funext x
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
j j' : J
f : j ⟶ j'
x : ((Functor.const J).obj (Shrink ↑(Functor.sections F))).obj j
⊢ (((Functor.const J).obj (Shrink ↑(Functor.sections F))).map f ≫
        (fun j u => ↑(↑(equivShrink ↑(Functor.sections F)).symm u) j) j')
      x =
    ((fun j u => ↑(↑(equivShrink ↑(Functor.sections F)).symm u) j) j ≫ F.map f) x
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
x y : (limitCone F).pt
w : ↑(equivShrink ↑(Functor.sections F)).symm x = ↑(equivShrink ↑(Functor.sections F)).symm y
⊢ x = y
[PROOFSTEP]
aesop
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ NatTrans.app (limitCone F).π j = NatTrans.app x✝¹.π j
⊢ x✝ =
    (fun s v =>
        ↑(equivShrink ↑(Functor.sections F))
          { val := fun j => NatTrans.app s.π j v,
            property := (_ : ∀ {j j' : J} (f : j ⟶ j'), (NatTrans.app s.π j ≫ F.map f) v = NatTrans.app s.π j' v) })
      x✝¹
[PROOFSTEP]
ext x j
[GOAL]
case h.w.a.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ NatTrans.app (limitCone F).π j = NatTrans.app x✝¹.π j
x : x✝¹.pt
j : J
⊢ ↑(↑(equivShrink ↑(Functor.sections F)).symm (x✝ x)) j =
    ↑(↑(equivShrink ↑(Functor.sections F)).symm
          ((fun s v =>
              ↑(equivShrink ↑(Functor.sections F))
                { val := fun j => NatTrans.app s.π j v,
                  property :=
                    (_ : ∀ {j j' : J} (f : j ⟶ j'), (NatTrans.app s.π j ≫ F.map f) v = NatTrans.app s.π j' v) })
            x✝¹ x))
      j
[PROOFSTEP]
simpa using congr_fun (w j) x
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj ↑(Functor.sections F)).map f ≫ (fun j u => ↑u j) j' = (fun j u => ↑u j) j ≫ F.map f
[PROOFSTEP]
funext x
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j j' : J
f : j ⟶ j'
x : ((Functor.const J).obj ↑(Functor.sections F)).obj j
⊢ (((Functor.const J).obj ↑(Functor.sections F)).map f ≫ (fun j u => ↑u j) j') x = ((fun j u => ↑u j) j ≫ F.map f) x
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ NatTrans.app (limitCone F).π j = NatTrans.app x✝¹.π j
⊢ x✝ =
    (fun s v =>
        { val := fun j => NatTrans.app s.π j v,
          property := (_ : ∀ {j j' : J} (f : j ⟶ j'), (NatTrans.app s.π j ≫ F.map f) v = NatTrans.app s.π j' v) })
      x✝¹
[PROOFSTEP]
funext x
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ NatTrans.app (limitCone F).π j = NatTrans.app x✝¹.π j
x : x✝¹.pt
⊢ x✝ x =
    (fun s v =>
        { val := fun j => NatTrans.app s.π j v,
          property := (_ : ∀ {j j' : J} (f : j ⟶ j'), (NatTrans.app s.π j ≫ F.map f) v = NatTrans.app s.π j' v) })
      x✝¹ x
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case h.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ NatTrans.app (limitCone F).π j = NatTrans.app x✝¹.π j
x : x✝¹.pt
⊢ ↑(x✝ x) =
    ↑((fun s v =>
          { val := fun j => NatTrans.app s.π j v,
            property := (_ : ∀ {j j' : J} (f : j ⟶ j'), (NatTrans.app s.π j ≫ F.map f) v = NatTrans.app s.π j' v) })
        x✝¹ x)
[PROOFSTEP]
funext j
[GOAL]
case h.a.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ NatTrans.app (limitCone F).π j = NatTrans.app x✝¹.π j
x : x✝¹.pt
j : J
⊢ ↑(x✝ x) j =
    ↑((fun s v =>
            { val := fun j => NatTrans.app s.π j v,
              property := (_ : ∀ {j j' : J} (f : j ⟶ j'), (NatTrans.app s.π j ≫ F.map f) v = NatTrans.app s.π j' v) })
          x✝¹ x)
      j
[PROOFSTEP]
exact congr_fun (w j) x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
c : Cone F
t : IsLimit c
j : J
x : c.pt
⊢ ↑(↑(isLimitEquivSections t) x) j = NatTrans.app c.π j x
[PROOFSTEP]
simp [isLimitEquivSections, IsLimit.conePointUniqueUpToIso]
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
c : Cone F
t : IsLimit c
x : ↑(Functor.sections F)
j : J
⊢ NatTrans.app c.π j (↑(isLimitEquivSections t).symm x) = ↑x j
[PROOFSTEP]
obtain ⟨x, rfl⟩ := (isLimitEquivSections.{v, u} t).surjective x
[GOAL]
case intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
c : Cone F
t : IsLimit c
j : J
x : c.pt
⊢ NatTrans.app c.π j (↑(isLimitEquivSections t).symm (↑(isLimitEquivSections t) x)) = ↑(↑(isLimitEquivSections t) x) j
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
x : limit F
j : J
⊢ ↑(↑(limitEquivSections F) x) j = limit.π F j x
[PROOFSTEP]
simp [limitEquivSections, isLimitEquivSections, IsLimit.conePointUniqueUpToIso]
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
x : (j : J) → F.obj j
h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j'
j : J
⊢ limit.π F j (mk F x h) = x j
[PROOFSTEP]
dsimp [Limit.mk]
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
x : (j : J) → F.obj j
h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j'
j : J
⊢ limit.π F j
      (↑(limitEquivSections F).symm { val := x, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), F.map f (x j) = x j') }) =
    x j
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
⊢ x = y
[PROOFSTEP]
apply (limitEquivSections.{v, u} F).injective
[GOAL]
case a
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
⊢ ↑(limitEquivSections F) x = ↑(limitEquivSections F) y
[PROOFSTEP]
ext j
[GOAL]
case a.a.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : UnivLE.{v, u}
F : J ⥤ Type u
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
j : J
⊢ ↑(↑(limitEquivSections F) x) j = ↑(↑(limitEquivSections F) y) j
[PROOFSTEP]
simp [w j]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
s : Cocone F
x✝² x✝¹ : (j : J) × F.obj j
j : J
x : F.obj j
j' : J
x' : F.obj j'
x✝ : Quot.Rel F { fst := j, snd := x } { fst := j', snd := x' }
f : { fst := j, snd := x }.fst ⟶ { fst := j', snd := x' }.fst
hf : { fst := j', snd := x' }.snd = F.map f { fst := j, snd := x }.snd
⊢ (fun p => NatTrans.app s.ι p.fst p.snd) { fst := j, snd := x } =
    (fun p => NatTrans.app s.ι p.fst p.snd) { fst := j', snd := x' }
[PROOFSTEP]
dsimp at hf 
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
s : Cocone F
x✝² x✝¹ : (j : J) × F.obj j
j : J
x : F.obj j
j' : J
x' : F.obj j'
x✝ : Quot.Rel F { fst := j, snd := x } { fst := j', snd := x' }
f : { fst := j, snd := x }.fst ⟶ { fst := j', snd := x' }.fst
hf : x' = F.map f x
⊢ (fun p => NatTrans.app s.ι p.fst p.snd) { fst := j, snd := x } =
    (fun p => NatTrans.app s.ι p.fst p.snd) { fst := j', snd := x' }
[PROOFSTEP]
rw [hf]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
s : Cocone F
x✝² x✝¹ : (j : J) × F.obj j
j : J
x : F.obj j
j' : J
x' : F.obj j'
x✝ : Quot.Rel F { fst := j, snd := x } { fst := j', snd := x' }
f : { fst := j, snd := x }.fst ⟶ { fst := j', snd := x' }.fst
hf : x' = F.map f x
⊢ (fun p => NatTrans.app s.ι p.fst p.snd) { fst := j, snd := x } =
    (fun p => NatTrans.app s.ι p.fst p.snd) { fst := j', snd := F.map f x }
[PROOFSTEP]
exact (congr_fun (Cocone.w s f) x).symm
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
⊢ m =
    (fun s =>
        Quot.lift (fun p => NatTrans.app s.ι p.fst p.snd)
          (_ :
            ∀ (x x_1 : (j : J) × F.obj j),
              Quot.Rel F x x_1 →
                (fun p => NatTrans.app s.ι p.fst p.snd) x = (fun p => NatTrans.app s.ι p.fst p.snd) x_1))
      s
[PROOFSTEP]
funext x
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : (colimitCocone F).pt
⊢ m x =
    (fun s =>
        Quot.lift (fun p => NatTrans.app s.ι p.fst p.snd)
          (_ :
            ∀ (x x_1 : (j : J) × F.obj j),
              Quot.Rel F x x_1 →
                (fun p => NatTrans.app s.ι p.fst p.snd) x = (fun p => NatTrans.app s.ι p.fst p.snd) x_1))
      s x
[PROOFSTEP]
induction' x using Quot.ind with x
[GOAL]
case h.mk
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), NatTrans.app (colimitCocone F).ι j ≫ m = NatTrans.app s.ι j
x : (j : J) × F.obj j
⊢ m (Quot.mk (Quot.Rel F) x) =
    (fun s =>
        Quot.lift (fun p => NatTrans.app s.ι p.fst p.snd)
          (_ :
            ∀ (x x_1 : (j : J) × F.obj j),
              Quot.Rel F x x_1 →
                (fun p => NatTrans.app s.ι p.fst p.snd) x = (fun p => NatTrans.app s.ι p.fst p.snd) x_1))
      s (Quot.mk (Quot.Rel F) x)
[PROOFSTEP]
exact congr_fun (hm x.1) x.2
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j : J
x : F.obj j
⊢ ↑(colimitEquivQuot F) (colimit.ι F j x) = Quot.mk (Quot.Rel F) { fst := j, snd := x }
[PROOFSTEP]
apply (colimitEquivQuot F).symm.injective
[GOAL]
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j : J
x : F.obj j
⊢ ↑(colimitEquivQuot F).symm (↑(colimitEquivQuot F) (colimit.ι F j x)) =
    ↑(colimitEquivQuot F).symm (Quot.mk (Quot.Rel F) { fst := j, snd := x })
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j j' : J
x : F.obj j
x' : F.obj j'
f : j ⟶ j'
w : F.map f x = x'
⊢ colimit.ι F j x = colimit.ι F j' x'
[PROOFSTEP]
rw [← w, Colimit.w_apply.{v, u}]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j j' : J
x : F.obj j
x' : F.obj j'
j'' : J
f : j ⟶ j''
f' : j' ⟶ j''
w : F.map f x = F.map f' x'
⊢ colimit.ι F j x = colimit.ι F j' x'
[PROOFSTEP]
rw [← colimit.w _ f, ← colimit.w _ f']
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j j' : J
x : F.obj j
x' : F.obj j'
j'' : J
f : j ⟶ j''
f' : j' ⟶ j''
w : F.map f x = F.map f' x'
⊢ (F.map f ≫ colimit.ι F j'') x = (F.map f' ≫ colimit.ι F j'') x'
[PROOFSTEP]
rw [types_comp_apply, types_comp_apply, w]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j j' : J
x : F.obj j
x' : F.obj j'
w : colimit.ι F j x = colimit.ι F j' x'
⊢ EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := x' }
[PROOFSTEP]
apply Quot.eq.1
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j j' : J
x : F.obj j
x' : F.obj j'
w : colimit.ι F j x = colimit.ι F j' x'
⊢ Quot.mk (Quot.Rel F) { fst := j, snd := x } = Quot.mk (Quot.Rel F) { fst := j', snd := x' }
[PROOFSTEP]
simpa using congr_arg (colimitEquivQuot.{v, u} F) w
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
⊢ ∃ j y, NatTrans.app t.ι j y = x
[PROOFSTEP]
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
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
this : (fun x => { down := ∃ j y, NatTrans.app t.ι j y = x }) = fun x => { down := True }
⊢ ∃ j y, NatTrans.app t.ι j y = x
[PROOFSTEP]
have := congr_fun this x
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
this✝ : (fun x => { down := ∃ j y, NatTrans.app t.ι j y = x }) = fun x => { down := True }
this : { down := ∃ j y, NatTrans.app t.ι j y = x } = { down := True }
⊢ ∃ j y, NatTrans.app t.ι j y = x
[PROOFSTEP]
simpa using congr_arg ULift.down this
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
⊢ (fun x => { down := ∃ j y, NatTrans.app t.ι j y = x }) = fun x => { down := True }
[PROOFSTEP]
refine' h.hom_ext _
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
⊢ ∀ (j : J),
    (NatTrans.app t.ι j ≫ fun x => { down := ∃ j y, NatTrans.app t.ι j y = x }) =
      NatTrans.app t.ι j ≫ fun x => { down := True }
[PROOFSTEP]
intro j
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
h : IsColimit t
x : t.pt
j : J
⊢ (NatTrans.app t.ι j ≫ fun x => { down := ∃ j y, NatTrans.app t.ι j y = x }) =
    NatTrans.app t.ι j ≫ fun x => { down := True }
[PROOFSTEP]
funext y
[GOAL]
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
⊢ (NatTrans.app t.ι j ≫ fun x => { down := ∃ j y, NatTrans.app t.ι j y = x }) y =
    (NatTrans.app t.ι j ≫ fun x => { down := True }) y
[PROOFSTEP]
simp only [Functor.const_obj_obj, types_comp_apply, ULift.up_inj, eq_iff_iff, iff_true]
[GOAL]
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, NatTrans.app t.ι j_1 y_1 = NatTrans.app t.ι j y
[PROOFSTEP]
exact ⟨j, y, rfl⟩
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x : colimit F
⊢ ∃ j y, colimit.ι F j y = x
[PROOFSTEP]
exact jointly_surjective.{v, u} F (colimit.isColimit F) x
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : Quot.Rel F x y
f : x.fst ⟶ y.fst
h : y.snd = F.map f x.snd
⊢ F.map f x.snd = F.map (𝟙 y.fst) y.snd
[PROOFSTEP]
rw [← h, FunctorToTypes.map_id_apply]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ EqvGen (Quot.Rel F) x y
[PROOFSTEP]
refine' EqvGen.trans _ ⟨k, F.map f x.2⟩ _ _ _
[GOAL]
case refine'_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ EqvGen (Quot.Rel F) x { fst := k, snd := F.map f x.snd }
[PROOFSTEP]
exact (EqvGen.rel _ _ ⟨f, rfl⟩)
[GOAL]
case refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ EqvGen (Quot.Rel F) { fst := k, snd := F.map f x.snd } y
[PROOFSTEP]
exact (EqvGen.symm _ _ (EqvGen.rel _ _ ⟨g, h⟩))
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
⊢ IsColimit t
[PROOFSTEP]
apply IsColimit.ofIsoColimit (colimit.isColimit F)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
⊢ colimit.cocone F ≅ t
[PROOFSTEP]
refine' Cocones.ext (Equiv.toIso (Equiv.ofBijective _ _)) _
[GOAL]
case refine'_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
⊢ (colimit.cocone F).pt → t.pt
[PROOFSTEP]
exact colimit.desc F t
[GOAL]
case refine'_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
⊢ Function.Bijective (colimit.desc F t)
[PROOFSTEP]
constructor
[GOAL]
case refine'_2.left
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
⊢ Function.Injective (colimit.desc F t)
[PROOFSTEP]
show Function.Injective _
[GOAL]
case refine'_2.left
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
⊢ Function.Injective (colimit.desc F t)
[PROOFSTEP]
intro a b h
[GOAL]
case refine'_2.left
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
a b : (colimit.cocone F).pt
h : colimit.desc F t a = colimit.desc F t b
⊢ a = b
[PROOFSTEP]
rcases jointly_surjective.{v, u} F (colimit.isColimit F) a with ⟨i, xi, rfl⟩
[GOAL]
case refine'_2.left.intro.intro
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
b : (colimit.cocone F).pt
i : J
xi : F.obj i
h : colimit.desc F t (NatTrans.app (colimit.cocone F).ι i xi) = colimit.desc F t b
⊢ NatTrans.app (colimit.cocone F).ι i xi = b
[PROOFSTEP]
rcases jointly_surjective.{v, u} F (colimit.isColimit F) b with ⟨j, xj, rfl⟩
[GOAL]
case refine'_2.left.intro.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
i : J
xi : F.obj i
j : J
xj : F.obj j
h :
  colimit.desc F t (NatTrans.app (colimit.cocone F).ι i xi) = colimit.desc F t (NatTrans.app (colimit.cocone F).ι j xj)
⊢ NatTrans.app (colimit.cocone F).ι i xi = NatTrans.app (colimit.cocone F).ι j xj
[PROOFSTEP]
replace h : (colimit.ι F i ≫ colimit.desc F t) xi = (colimit.ι F j ≫ colimit.desc F t) xj := h
[GOAL]
case refine'_2.left.intro.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
i : J
xi : F.obj i
j : J
xj : F.obj j
h : (colimit.ι F i ≫ colimit.desc F t) xi = (colimit.ι F j ≫ colimit.desc F t) xj
⊢ NatTrans.app (colimit.cocone F).ι i xi = NatTrans.app (colimit.cocone F).ι j xj
[PROOFSTEP]
rw [colimit.ι_desc, colimit.ι_desc] at h 
[GOAL]
case refine'_2.left.intro.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
i : J
xi : F.obj i
j : J
xj : F.obj j
h : NatTrans.app t.ι i xi = NatTrans.app t.ι j xj
⊢ NatTrans.app (colimit.cocone F).ι i xi = NatTrans.app (colimit.cocone F).ι j xj
[PROOFSTEP]
rcases hinj i j xi xj h with ⟨k, f, g, h'⟩
[GOAL]
case refine'_2.left.intro.intro.intro.intro.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
i : J
xi : F.obj i
j : J
xj : F.obj j
h : NatTrans.app t.ι i xi = NatTrans.app t.ι j xj
k : J
f : i ⟶ k
g : j ⟶ k
h' : F.map f xi = F.map g xj
⊢ NatTrans.app (colimit.cocone F).ι i xi = NatTrans.app (colimit.cocone F).ι j xj
[PROOFSTEP]
change colimit.ι F i xi = colimit.ι F j xj
[GOAL]
case refine'_2.left.intro.intro.intro.intro.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
i : J
xi : F.obj i
j : J
xj : F.obj j
h : NatTrans.app t.ι i xi = NatTrans.app t.ι j xj
k : J
f : i ⟶ k
g : j ⟶ k
h' : F.map f xi = F.map g xj
⊢ colimit.ι F i xi = colimit.ι F j xj
[PROOFSTEP]
rw [← colimit.w F f, ← colimit.w F g]
[GOAL]
case refine'_2.left.intro.intro.intro.intro.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
i : J
xi : F.obj i
j : J
xj : F.obj j
h : NatTrans.app t.ι i xi = NatTrans.app t.ι j xj
k : J
f : i ⟶ k
g : j ⟶ k
h' : F.map f xi = F.map g xj
⊢ (F.map f ≫ colimit.ι F k) xi = (F.map g ≫ colimit.ι F k) xj
[PROOFSTEP]
change colimit.ι F k (F.map f xi) = colimit.ι F k (F.map g xj)
[GOAL]
case refine'_2.left.intro.intro.intro.intro.intro.intro.intro
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
i : J
xi : F.obj i
j : J
xj : F.obj j
h : NatTrans.app t.ι i xi = NatTrans.app t.ι j xj
k : J
f : i ⟶ k
g : j ⟶ k
h' : F.map f xi = F.map g xj
⊢ colimit.ι F k (F.map f xi) = colimit.ι F k (F.map g xj)
[PROOFSTEP]
rw [h']
[GOAL]
case refine'_2.right
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
⊢ Function.Surjective (colimit.desc F t)
[PROOFSTEP]
show Function.Surjective _
[GOAL]
case refine'_2.right
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
⊢ Function.Surjective (colimit.desc F t)
[PROOFSTEP]
intro x
[GOAL]
case refine'_2.right
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
x : t.pt
⊢ ∃ a, colimit.desc F t a = x
[PROOFSTEP]
rcases hsurj x with ⟨i, xi, rfl⟩
[GOAL]
case refine'_2.right.intro.intro
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
i : J
xi : F.obj i
⊢ ∃ a, colimit.desc F t a = NatTrans.app t.ι i xi
[PROOFSTEP]
use colimit.ι F i xi
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
i : J
xi : F.obj i
⊢ colimit.desc F t (colimit.ι F i xi) = NatTrans.app t.ι i xi
[PROOFSTEP]
apply Colimit.ι_desc_apply.{v, u}
[GOAL]
case refine'_3
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
⊢ ∀ (j : J),
    NatTrans.app (colimit.cocone F).ι j ≫
        (Equiv.toIso
            (Equiv.ofBijective (colimit.desc F t)
              (_ : Function.Injective (colimit.desc F t) ∧ Function.Surjective (colimit.desc F t)))).hom =
      NatTrans.app t.ι j
[PROOFSTEP]
intro j
[GOAL]
case refine'_3
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = NatTrans.app t.ι i xi
hinj :
  ∀ (i j : J) (xi : F.obj i) (xj : F.obj j),
    NatTrans.app t.ι i xi = NatTrans.app t.ι j xj → ∃ k f g, F.map f xi = F.map g xj
j : J
⊢ NatTrans.app (colimit.cocone F).ι j ≫
      (Equiv.toIso
          (Equiv.ofBijective (colimit.desc F t)
            (_ : Function.Injective (colimit.desc F t) ∧ Function.Surjective (colimit.desc F t)))).hom =
    NatTrans.app t.ι j
[PROOFSTEP]
apply colimit.ι_desc
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map (f ≫ fl ≫ n) x.snd = F.map (fl ≫ n) (F.map f x.snd)
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map (fl ≫ n) (F.map f x.snd) = F.map (fl ≫ n) (F.map g y.snd)
[PROOFSTEP]
rw [h]
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map (fl ≫ n) (F.map g y.snd) = F.map ((g ≫ fl) ≫ n) y.snd
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map ((g ≫ fl) ≫ n) y.snd = F.map ((f' ≫ gl) ≫ n) y.snd
[PROOFSTEP]
rw [hn]
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map ((f' ≫ gl) ≫ n) y.snd = F.map (gl ≫ n) (F.map f' y.snd)
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map (gl ≫ n) (F.map f' y.snd) = F.map (gl ≫ n) (F.map g' z.snd)
[PROOFSTEP]
rw [h']
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map (gl ≫ n) (F.map g' z.snd) = F.map (g' ≫ gl ≫ n) z.snd
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
⊢ FilteredColimit.Rel F = EqvGen (Quot.Rel F)
[PROOFSTEP]
ext ⟨j, x⟩ ⟨j', y⟩
[GOAL]
case h.mk.h.mk.a
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F { fst := j, snd := x } { fst := j', snd := y } ↔
    EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := y }
[PROOFSTEP]
constructor
[GOAL]
case h.mk.h.mk.a.mp
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F { fst := j, snd := x } { fst := j', snd := y } →
    EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := y }
[PROOFSTEP]
apply eqvGen_quot_rel_of_rel
[GOAL]
case h.mk.h.mk.a.mpr
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := y } →
    FilteredColimit.Rel F { fst := j, snd := x } { fst := j', snd := y }
[PROOFSTEP]
rw [← (FilteredColimit.rel_equiv F).eqvGen_iff]
[GOAL]
case h.mk.h.mk.a.mpr
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := y } →
    EqvGen (FilteredColimit.Rel F) { fst := j, snd := x } { fst := j', snd := y }
[PROOFSTEP]
exact EqvGen.mono (rel_of_quot_rel F)
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
i j : J
xi : F.obj i
xj : F.obj j
⊢ NatTrans.app (colimitCocone F).ι i xi = NatTrans.app (colimitCocone F).ι j xj ↔
    FilteredColimit.Rel F { fst := i, snd := xi } { fst := j, snd := xj }
[PROOFSTEP]
change Quot.mk _ _ = Quot.mk _ _ ↔ _
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ TypeMax
inst✝ : IsFilteredOrEmpty J
i j : J
xi : F.obj i
xj : F.obj j
⊢ Quot.mk (Quot.Rel F) { fst := i, snd := xi } = Quot.mk (Quot.Rel F) { fst := j, snd := xj } ↔
    FilteredColimit.Rel F { fst := i, snd := xi } { fst := j, snd := xj }
[PROOFSTEP]
rw [Quot.eq, FilteredColimit.rel_eq_eqvGen_quot_rel]
[GOAL]
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
⊢ NatTrans.app t.ι i xi = NatTrans.app t.ι j xj ↔ ∃ k f g, F.map f xi = F.map g xj
[PROOFSTEP]
let t' := colimitCocone.{v, u} F
[GOAL]
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
⊢ NatTrans.app t.ι i xi = NatTrans.app t.ι j xj ↔ ∃ k f g, F.map f xi = F.map g xj
[PROOFSTEP]
let e : t' ≅ t := IsColimit.uniqueUpToIso (colimitCoconeIsColimit F) ht
[GOAL]
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
⊢ NatTrans.app t.ι i xi = NatTrans.app t.ι j xj ↔ ∃ k f g, F.map f xi = F.map g xj
[PROOFSTEP]
let e' : t'.pt ≅ t.pt := (Cocones.forget _).mapIso e
[GOAL]
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
⊢ NatTrans.app t.ι i xi = NatTrans.app t.ι j xj ↔ ∃ k f g, F.map f xi = F.map g xj
[PROOFSTEP]
refine' Iff.trans _ (colimit_eq_iff_aux.{v, u} F)
[GOAL]
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
⊢ NatTrans.app t.ι i xi = NatTrans.app t.ι j xj ↔
    NatTrans.app (colimitCocone F).ι i xi = NatTrans.app (colimitCocone F).ι j xj
[PROOFSTEP]
exact @Equiv.apply_eq_iff_eq _ _ e'.toEquiv ((colimitCocone.{v, u} F).ι.app i xi) ((colimitCocone.{v, u} F).ι.app j xj)
[GOAL]
J : Type v
inst✝ : SmallCategory J
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f
[PROOFSTEP]
funext x
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ (lift F' ≫ F'.m) x = ι f x
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = _
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ (F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => f x_1 = ↑x) (_ : ↑x ∈ Set.range f)) = ι f x
[PROOFSTEP]
rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ ↑x = ι f x
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
α β : Type u
f : α ⟶ β
⊢ ∀ {X Y : Type u} (f : X ⟶ Y), HasImage f
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
α β : Type u
f✝ : α ⟶ β
f g : Arrow (Type u)
st : f ⟶ g
x : (monoFactorisation f.hom).I
⊢ Comma.hom g (CommaMorphism.left st (Classical.choose (_ : ↑x ∈ Set.range f.hom))) = CommaMorphism.right st ↑x
[PROOFSTEP]
have p := st.w
[GOAL]
J : Type v
inst✝ : SmallCategory J
α β : Type u
f✝ : α ⟶ β
f g : Arrow (Type u)
st : f ⟶ g
x : (monoFactorisation f.hom).I
p : (𝟭 (Type u)).map st.left ≫ g.hom = f.hom ≫ (𝟭 (Type u)).map st.right
⊢ Comma.hom g (CommaMorphism.left st (Classical.choose (_ : ↑x ∈ Set.range f.hom))) = CommaMorphism.right st ↑x
[PROOFSTEP]
replace p := congr_fun p (Classical.choose x.2)
[GOAL]
J : Type v
inst✝ : SmallCategory J
α β : Type u
f✝ : α ⟶ β
f g : Arrow (Type u)
st : f ⟶ g
x : (monoFactorisation f.hom).I
p :
  ((𝟭 (Type u)).map st.left ≫ g.hom) (Classical.choose (_ : ↑x ∈ Set.range f.hom)) =
    (f.hom ≫ (𝟭 (Type u)).map st.right) (Classical.choose (_ : ↑x ∈ Set.range f.hom))
⊢ Comma.hom g (CommaMorphism.left st (Classical.choose (_ : ↑x ∈ Set.range f.hom))) = CommaMorphism.right st ↑x
[PROOFSTEP]
simp only [Functor.id_obj, Functor.id_map, types_comp_apply] at p 
[GOAL]
J : Type v
inst✝ : SmallCategory J
α β : Type u
f✝ : α ⟶ β
f g : Arrow (Type u)
st : f ⟶ g
x : (monoFactorisation f.hom).I
p :
  Comma.hom g (CommaMorphism.left st (Classical.choose (_ : ∃ x_1, (fun x_2 => Comma.hom f x_2 = ↑x) x_1))) =
    CommaMorphism.right st (Comma.hom f (Classical.choose (_ : ∃ x_1, (fun x_2 => Comma.hom f x_2 = ↑x) x_1)))
⊢ Comma.hom g (CommaMorphism.left st (Classical.choose (_ : ↑x ∈ Set.range f.hom))) = CommaMorphism.right st ↑x
[PROOFSTEP]
erw [p, Classical.choose_spec x.2]
