[GOAL]
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
⊢ (X_1 : C) → (coyoneda.obj X).obj X_1 ⟶ ((Functor.const C).obj PUnit).obj X_1
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
Y : C
⊢ NatTrans.app (colimitCocone X).ι Y ≫ (fun s x => NatTrans.app s.ι X.unop (𝟙 X.unop)) s = NatTrans.app s.ι Y
[PROOFSTEP]
funext f
[GOAL]
case h
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
Y : C
f : (coyoneda.obj X).obj Y
⊢ (NatTrans.app (colimitCocone X).ι Y ≫ (fun s x => NatTrans.app s.ι X.unop (𝟙 X.unop)) s) f = NatTrans.app s.ι Y f
[PROOFSTEP]
convert congr_fun (s.w f).symm (𝟙 (unop X))
[GOAL]
case h.e'_3.h
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
Y : C
f : (coyoneda.obj X).obj Y
e_1✝ : s.pt = ((Functor.const C).obj s.pt).obj X.unop
⊢ NatTrans.app s.ι Y f = ((coyoneda.obj X).map f ≫ NatTrans.app s.ι Y) (𝟙 X.unop)
[PROOFSTEP]
simp only [coyoneda_obj_obj, Functor.const_obj_obj, types_comp_apply, coyoneda_obj_map, Category.id_comp]
[GOAL]
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
m : (colimitCocone X).pt ⟶ s.pt
w : ∀ (j : C), NatTrans.app (colimitCocone X).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s x => NatTrans.app s.ι X.unop (𝟙 X.unop)) s
[PROOFSTEP]
apply funext
[GOAL]
case h
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
m : (colimitCocone X).pt ⟶ s.pt
w : ∀ (j : C), NatTrans.app (colimitCocone X).ι j ≫ m = NatTrans.app s.ι j
⊢ ∀ (x : (colimitCocone X).pt), m x = (fun s x => NatTrans.app s.ι X.unop (𝟙 X.unop)) s x
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case h.unit
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
m : (colimitCocone X).pt ⟶ s.pt
w : ∀ (j : C), NatTrans.app (colimitCocone X).ι j ≫ m = NatTrans.app s.ι j
⊢ m PUnit.unit = (fun s x => NatTrans.app s.ι X.unop (𝟙 X.unop)) s PUnit.unit
[PROOFSTEP]
dsimp
[GOAL]
case h.unit
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
m : (colimitCocone X).pt ⟶ s.pt
w : ∀ (j : C), NatTrans.app (colimitCocone X).ι j ≫ m = NatTrans.app s.ι j
⊢ m PUnit.unit = NatTrans.app s.ι X.unop (𝟙 X.unop)
[PROOFSTEP]
rw [← w]
[GOAL]
case h.unit
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
m : (colimitCocone X).pt ⟶ s.pt
w : ∀ (j : C), NatTrans.app (colimitCocone X).ι j ≫ m = NatTrans.app s.ι j
⊢ m PUnit.unit = (NatTrans.app (colimitCocone X).ι X.unop ≫ m) (𝟙 X.unop)
[PROOFSTEP]
simp
[GOAL]
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
⊢ colimit (coyoneda.obj X) ≅ PUnit
[PROOFSTEP]
apply
  colimit.isoColimitCocone
    { cocone := _
      isColimit := colimitCoconeIsColimit X }
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : C
J : Type v
𝒥 : Category.{v, v} J
K : J ⥤ Cᵒᵖ
c : Cone K
t : IsLimit c
s : Cone (K ⋙ yoneda.obj X)
m : s.pt ⟶ ((yoneda.obj X).mapCone c).pt
w : ∀ (j : J), m ≫ NatTrans.app ((yoneda.obj X).mapCone c).π j = NatTrans.app s.π j
x : s.pt
⊢ m x = (fun s x => (IsLimit.lift t { pt := op X, π := NatTrans.mk fun j => (NatTrans.app s.π j x).op }).unop) s x
[PROOFSTEP]
refine' Quiver.Hom.op_inj (t.uniq ⟨op X, _, _⟩ _ fun j => _)
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (X : C) {J : Type v} (𝒥 : Category.{v, v} J) {K : J ⥤ Cᵒᵖ} {c : Cone K},
    IsLimit c →
      ∀ (s : Cone (K ⋙ yoneda.obj X)) (x : s.pt) (j₁ j₂ : J) (α : j₁ ⟶ j₂),
        ((Functor.const J).obj (op X)).map α ≫ (fun j => (NatTrans.app s.π j x).op) j₂ =
          (fun j => (NatTrans.app s.π j x).op) j₁ ≫ K.map α
[PROOFSTEP]
intro X _ _ _ _ _ s _ _ _ α
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
X : C
J✝ : Type v
𝒥✝ : Category.{v, v} J✝
K✝ : J✝ ⥤ Cᵒᵖ
c✝ : Cone K✝
t✝ : IsLimit c✝
s : Cone (K✝ ⋙ yoneda.obj X)
x✝ : s.pt
j₁✝ j₂✝ : J✝
α : j₁✝ ⟶ j₂✝
⊢ ((Functor.const J✝).obj (op X)).map α ≫ (fun j => (NatTrans.app s.π j x✝).op) j₂✝ =
    (fun j => (NatTrans.app s.π j x✝).op) j₁✝ ≫ K✝.map α
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
X : C
J✝ : Type v
𝒥✝ : Category.{v, v} J✝
K✝ : J✝ ⥤ Cᵒᵖ
c✝ : Cone K✝
t✝ : IsLimit c✝
s : Cone (K✝ ⋙ yoneda.obj X)
x✝ : s.pt
j₁✝ j₂✝ : J✝
α : j₁✝ ⟶ j₂✝
⊢ 𝟙 (op X) ≫ (NatTrans.app s.π j₂✝ x✝).op = (NatTrans.app s.π j₁✝ x✝).op ≫ K✝.map α
[PROOFSTEP]
simp [← s.w α]
  -- See library note [dsimp, simp]
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
X : C
J : Type v
𝒥 : Category.{v, v} J
K : J ⥤ Cᵒᵖ
c : Cone K
t : IsLimit c
s : Cone (K ⋙ yoneda.obj X)
m : s.pt ⟶ ((yoneda.obj X).mapCone c).pt
w : ∀ (j : J), m ≫ NatTrans.app ((yoneda.obj X).mapCone c).π j = NatTrans.app s.π j
x : s.pt
j : J
⊢ (m x).op ≫ NatTrans.app c.π j = NatTrans.app { pt := op X, π := NatTrans.mk fun j => (NatTrans.app s.π j x).op }.π j
[PROOFSTEP]
exact Quiver.Hom.unop_inj (congrFun (w j) x)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
J : Type v
𝒥 : Category.{v, v} J
K : J ⥤ C
c : Cone K
t : IsLimit c
s : Cone (K ⋙ coyoneda.obj X)
x : s.pt
j₁ j₂ : J
α : j₁ ⟶ j₂
⊢ ((Functor.const J).obj X.unop).map α ≫ (fun j => NatTrans.app s.π j x) j₂ =
    (fun j => NatTrans.app s.π j x) j₁ ≫ K.map α
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
J : Type v
𝒥 : Category.{v, v} J
K : J ⥤ C
c : Cone K
t : IsLimit c
s : Cone (K ⋙ coyoneda.obj X)
x : s.pt
j₁ j₂ : J
α : j₁ ⟶ j₂
⊢ 𝟙 X.unop ≫ NatTrans.app s.π j₂ x = NatTrans.app s.π j₁ x ≫ K.map α
[PROOFSTEP]
simp [← s.w α]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
J : Type v
𝒥 : Category.{v, v} J
K : J ⥤ C
c : Cone K
t : IsLimit c
s : Cone (K ⋙ coyoneda.obj X)
m : s.pt ⟶ ((coyoneda.obj X).mapCone c).pt
w : ∀ (j : J), m ≫ NatTrans.app ((coyoneda.obj X).mapCone c).π j = NatTrans.app s.π j
x : s.pt
⊢ m x = (fun s x => IsLimit.lift t { pt := X.unop, π := NatTrans.mk fun j => NatTrans.app s.π j x }) s x
[PROOFSTEP]
refine' t.uniq ⟨unop X, _⟩ _ fun j => _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
J : Type v
𝒥 : Category.{v, v} J
K : J ⥤ C
c : Cone K
t : IsLimit c
s : Cone (K ⋙ coyoneda.obj X)
m : s.pt ⟶ ((coyoneda.obj X).mapCone c).pt
w : ∀ (j : J), m ≫ NatTrans.app ((coyoneda.obj X).mapCone c).π j = NatTrans.app s.π j
x : s.pt
j : J
⊢ m x ≫ NatTrans.app c.π j = NatTrans.app { pt := X.unop, π := NatTrans.mk fun j => NatTrans.app s.π j x }.π j
[PROOFSTEP]
exact congrFun (w j) x
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ m = (fun s => (IsLimit.lift (t s.pt.unop) (s' s) PUnit.unit).op) s
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ m.unop = ((fun s => (IsLimit.lift (t s.pt.unop) (s' s) PUnit.unit).op) s).unop
[PROOFSTEP]
suffices (fun _ : PUnit => m.unop) = (t s.pt.unop).lift (s' s) by apply congr_fun this PUnit.unit
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
this : (fun x => m.unop) = IsLimit.lift (t s.pt.unop) (s' s)
⊢ m.unop = ((fun s => (IsLimit.lift (t s.pt.unop) (s' s) PUnit.unit).op) s).unop
[PROOFSTEP]
apply congr_fun this PUnit.unit
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ (fun x => m.unop) = IsLimit.lift (t s.pt.unop) (s' s)
[PROOFSTEP]
apply (t _).uniq (s' s) _ fun j => _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ ∀ (j : J), (fun x => m.unop) ≫ NatTrans.app ((yoneda.obj s.pt.unop).mapCone c).π j = NatTrans.app (s' s).π j
[PROOFSTEP]
intro j
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
j : J
⊢ (fun x => m.unop) ≫ NatTrans.app ((yoneda.obj s.pt.unop).mapCone c).π j = NatTrans.app (s' s).π j
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
j : J
x✝ : (s' s).pt
⊢ ((fun x => m.unop) ≫ NatTrans.app ((yoneda.obj s.pt.unop).mapCone c).π j) x✝ = NatTrans.app (s' s).π j x✝
[PROOFSTEP]
exact Quiver.Hom.op_inj (w j)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
c : Cone K
t : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ coyoneda.obj (op s.pt)) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => NatTrans.app s.π j }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ m = (fun s => IsLimit.lift (t (op s.pt)) (s' s) PUnit.unit) s
[PROOFSTEP]
suffices (fun _ : PUnit => m) = (t _).lift (s' s) by apply congr_fun this PUnit.unit
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
c : Cone K
t : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ coyoneda.obj (op s.pt)) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => NatTrans.app s.π j }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
this : (fun x => m) = IsLimit.lift (t (op s.pt)) (s' s)
⊢ m = (fun s => IsLimit.lift (t (op s.pt)) (s' s) PUnit.unit) s
[PROOFSTEP]
apply congr_fun this PUnit.unit
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
c : Cone K
t : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ coyoneda.obj (op s.pt)) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => NatTrans.app s.π j }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ (fun x => m) = IsLimit.lift (t (op s.pt)) (s' s)
[PROOFSTEP]
apply (t _).uniq (s' s) _ fun j => _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
c : Cone K
t : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ coyoneda.obj (op s.pt)) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => NatTrans.app s.π j }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ ∀ (j : J), (fun x => m) ≫ NatTrans.app ((coyoneda.obj (op s.pt)).mapCone c).π j = NatTrans.app (s' s).π j
[PROOFSTEP]
intro j
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
c : Cone K
t : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ coyoneda.obj (op s.pt)) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => NatTrans.app s.π j }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
j : J
⊢ (fun x => m) ≫ NatTrans.app ((coyoneda.obj (op s.pt)).mapCone c).π j = NatTrans.app (s' s).π j
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
c : Cone K
t : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ coyoneda.obj (op s.pt)) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => NatTrans.app s.π j }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
j : J
x✝ : (s' s).pt
⊢ ((fun x => m) ≫ NatTrans.app ((coyoneda.obj (op s.pt)).mapCone c).π j) x✝ = NatTrans.app (s' s).π j x✝
[PROOFSTEP]
exact w j
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
⊢ PreservesLimits yoneda
[PROOFSTEP]
apply preservesLimitsOfEvaluation
[GOAL]
case x
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
⊢ (k : Dᵒᵖ) → PreservesLimitsOfSize.{u, u, u, u, u, u + 1} (yoneda ⋙ (evaluation Dᵒᵖ (Type u)).obj k)
[PROOFSTEP]
intro K
[GOAL]
case x
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
K : Dᵒᵖ
⊢ PreservesLimitsOfSize.{u, u, u, u, u, u + 1} (yoneda ⋙ (evaluation Dᵒᵖ (Type u)).obj K)
[PROOFSTEP]
change PreservesLimits (coyoneda.obj K)
[GOAL]
case x
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
K : Dᵒᵖ
⊢ PreservesLimits (coyoneda.obj K)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
⊢ PreservesLimits coyoneda
[PROOFSTEP]
apply preservesLimitsOfEvaluation
[GOAL]
case x
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
⊢ (k : D) → PreservesLimitsOfSize.{u, u, u, u, u, u + 1} (coyoneda ⋙ (evaluation D (Type u)).obj k)
[PROOFSTEP]
intro K
[GOAL]
case x
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
K : D
⊢ PreservesLimitsOfSize.{u, u, u, u, u, u + 1} (coyoneda ⋙ (evaluation D (Type u)).obj K)
[PROOFSTEP]
change PreservesLimits (yoneda.obj K)
[GOAL]
case x
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
K : D
⊢ PreservesLimits (yoneda.obj K)
[PROOFSTEP]
infer_instance


[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]


[GOAL]
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ ((Functor.const J).obj
            { left := c₁.pt, right := c₂.pt,
              hom := IsLimit.lift (isLimitOfPreserves R t₂) (limitAuxiliaryCone F c₁) }).map
        t ≫
      (fun j => CommaMorphism.mk (NatTrans.app c₁.π j) (NatTrans.app c₂.π j)) j₂ =
    (fun j => CommaMorphism.mk (NatTrans.app c₁.π j) (NatTrans.app c₂.π j)) j₁ ≫ F.map t
[PROOFSTEP]
ext
[GOAL]
case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (((Functor.const J).obj
              { left := c₁.pt, right := c₂.pt,
                hom := IsLimit.lift (isLimitOfPreserves R t₂) (limitAuxiliaryCone F c₁) }).map
          t ≫
        (fun j => CommaMorphism.mk (NatTrans.app c₁.π j) (NatTrans.app c₂.π j)) j₂).left =
    ((fun j => CommaMorphism.mk (NatTrans.app c₁.π j) (NatTrans.app c₂.π j)) j₁ ≫ F.map t).left
[PROOFSTEP]
simp [← c₁.w t]
[GOAL]
case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (((Functor.const J).obj
              { left := c₁.pt, right := c₂.pt,
                hom := IsLimit.lift (isLimitOfPreserves R t₂) (limitAuxiliaryCone F c₁) }).map
          t ≫
        (fun j => CommaMorphism.mk (NatTrans.app c₁.π j) (NatTrans.app c₂.π j)) j₂).right =
    ((fun j => CommaMorphism.mk (NatTrans.app c₁.π j) (NatTrans.app c₂.π j)) j₁ ≫ F.map t).right
[PROOFSTEP]
simp [← c₂.w t]
[GOAL]
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
t₁ : IsLimit c₁
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
s : Cone F
j : J
⊢ (L.map (IsLimit.lift t₁ ((fst L R).mapCone s)) ≫ (coneOfPreserves F c₁ t₂).pt.hom) ≫ NatTrans.app (R.mapCone c₂).π j =
    (s.pt.hom ≫ R.map (IsLimit.lift t₂ ((snd L R).mapCone s))) ≫ NatTrans.app (R.mapCone c₂).π j
[PROOFSTEP]
rw [coneOfPreserves_pt_hom, assoc, assoc, (isLimitOfPreserves R t₂).fac, limitAuxiliaryCone_π_app, ← L.map_comp_assoc,
  t₁.fac, R.mapCone_π_app, ← R.map_comp, t₂.fac]
[GOAL]
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
t₁ : IsLimit c₁
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
s : Cone F
j : J
⊢ L.map (NatTrans.app ((fst L R).mapCone s).π j) ≫ (F.obj j).hom =
    s.pt.hom ≫ R.map (NatTrans.app ((snd L R).mapCone s).π j)
[PROOFSTEP]
exact (s.π.app j).w
[GOAL]
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
t₁ : IsLimit c₁
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
s : Cone F
m : s.pt ⟶ (coneOfPreserves F c₁ t₂).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfPreserves F c₁ t₂).π j = NatTrans.app s.π j
⊢ m = (fun s => CommaMorphism.mk (IsLimit.lift t₁ ((fst L R).mapCone s)) (IsLimit.lift t₂ ((snd L R).mapCone s))) s
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case left
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
t₁ : IsLimit c₁
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
s : Cone F
m : s.pt ⟶ (coneOfPreserves F c₁ t₂).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfPreserves F c₁ t₂).π j = NatTrans.app s.π j
⊢ m.left =
    ((fun s => CommaMorphism.mk (IsLimit.lift t₁ ((fst L R).mapCone s)) (IsLimit.lift t₂ ((snd L R).mapCone s))) s).left
[PROOFSTEP]
exact t₁.uniq ((fst L R).mapCone s) _ (fun j => by simp [← w])
[GOAL]
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
t₁ : IsLimit c₁
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
s : Cone F
m : s.pt ⟶ (coneOfPreserves F c₁ t₂).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfPreserves F c₁ t₂).π j = NatTrans.app s.π j
j : J
⊢ m.left ≫ NatTrans.app c₁.π j = NatTrans.app ((fst L R).mapCone s).π j
[PROOFSTEP]
simp [← w]
[GOAL]
case right
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
t₁ : IsLimit c₁
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
s : Cone F
m : s.pt ⟶ (coneOfPreserves F c₁ t₂).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfPreserves F c₁ t₂).π j = NatTrans.app s.π j
⊢ m.right =
    ((fun s => CommaMorphism.mk (IsLimit.lift t₁ ((fst L R).mapCone s)) (IsLimit.lift t₂ ((snd L R).mapCone s)))
        s).right
[PROOFSTEP]
exact t₂.uniq ((snd L R).mapCone s) _ (fun j => by simp [← w])
[GOAL]
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
t₁ : IsLimit c₁
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
s : Cone F
m : s.pt ⟶ (coneOfPreserves F c₁ t₂).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfPreserves F c₁ t₂).π j = NatTrans.app s.π j
j : J
⊢ m.right ≫ NatTrans.app c₂.π j = NatTrans.app ((snd L R).mapCone s).π j
[PROOFSTEP]
simp [← w]
[GOAL]
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ F.map t ≫ (fun j => CommaMorphism.mk (NatTrans.app c₁.ι j) (NatTrans.app c₂.ι j)) j₂ =
    (fun j => CommaMorphism.mk (NatTrans.app c₁.ι j) (NatTrans.app c₂.ι j)) j₁ ≫
      ((Functor.const J).obj
            { left := c₁.pt, right := c₂.pt,
              hom := IsColimit.desc (isColimitOfPreserves L t₁) (colimitAuxiliaryCocone F c₂) }).map
        t
[PROOFSTEP]
ext
[GOAL]
case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (F.map t ≫ (fun j => CommaMorphism.mk (NatTrans.app c₁.ι j) (NatTrans.app c₂.ι j)) j₂).left =
    ((fun j => CommaMorphism.mk (NatTrans.app c₁.ι j) (NatTrans.app c₂.ι j)) j₁ ≫
        ((Functor.const J).obj
              { left := c₁.pt, right := c₂.pt,
                hom := IsColimit.desc (isColimitOfPreserves L t₁) (colimitAuxiliaryCocone F c₂) }).map
          t).left
[PROOFSTEP]
simp [← c₁.w t]
[GOAL]
case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (F.map t ≫ (fun j => CommaMorphism.mk (NatTrans.app c₁.ι j) (NatTrans.app c₂.ι j)) j₂).right =
    ((fun j => CommaMorphism.mk (NatTrans.app c₁.ι j) (NatTrans.app c₂.ι j)) j₁ ≫
        ((Functor.const J).obj
              { left := c₁.pt, right := c₂.pt,
                hom := IsColimit.desc (isColimitOfPreserves L t₁) (colimitAuxiliaryCocone F c₂) }).map
          t).right
[PROOFSTEP]
simp [← c₂.w t]
[GOAL]
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
j : J
⊢ NatTrans.app (L.mapCocone c₁).ι j ≫ L.map (IsColimit.desc t₁ ((fst L R).mapCocone s)) ≫ s.pt.hom =
    NatTrans.app (L.mapCocone c₁).ι j ≫
      (coconeOfPreserves F t₁ c₂).pt.hom ≫ R.map (IsColimit.desc t₂ ((snd L R).mapCocone s))
[PROOFSTEP]
rw [coconeOfPreserves_pt_hom, (isColimitOfPreserves L t₁).fac_assoc, colimitAuxiliaryCocone_ι_app, assoc, ← R.map_comp,
  t₂.fac, L.mapCocone_ι_app, ← L.map_comp_assoc, t₁.fac]
[GOAL]
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
j : J
⊢ L.map (NatTrans.app ((fst L R).mapCocone s).ι j) ≫ s.pt.hom =
    (F.obj j).hom ≫ R.map (NatTrans.app ((snd L R).mapCocone s).ι j)
[PROOFSTEP]
exact (s.ι.app j).w
[GOAL]
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
m : (coconeOfPreserves F t₁ c₂).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfPreserves F t₁ c₂).ι j ≫ m = NatTrans.app s.ι j
⊢ m =
    (fun s => CommaMorphism.mk (IsColimit.desc t₁ ((fst L R).mapCocone s)) (IsColimit.desc t₂ ((snd L R).mapCocone s)))
      s
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case left
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
m : (coconeOfPreserves F t₁ c₂).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfPreserves F t₁ c₂).ι j ≫ m = NatTrans.app s.ι j
⊢ m.left =
    ((fun s => CommaMorphism.mk (IsColimit.desc t₁ ((fst L R).mapCocone s)) (IsColimit.desc t₂ ((snd L R).mapCocone s)))
        s).left
[PROOFSTEP]
exact t₁.uniq ((fst L R).mapCocone s) _ (fun j => by simp [← w])
[GOAL]
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
m : (coconeOfPreserves F t₁ c₂).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfPreserves F t₁ c₂).ι j ≫ m = NatTrans.app s.ι j
j : J
⊢ NatTrans.app c₁.ι j ≫ m.left = NatTrans.app ((fst L R).mapCocone s).ι j
[PROOFSTEP]
simp [← w]
[GOAL]
case right
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
m : (coconeOfPreserves F t₁ c₂).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfPreserves F t₁ c₂).ι j ≫ m = NatTrans.app s.ι j
⊢ m.right =
    ((fun s => CommaMorphism.mk (IsColimit.desc t₁ ((fst L R).mapCocone s)) (IsColimit.desc t₂ ((snd L R).mapCocone s)))
        s).right
[PROOFSTEP]
exact t₂.uniq ((snd L R).mapCocone s) _ (fun j => by simp [← w])
[GOAL]
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v, u₁} A
B : Type u₂
inst✝² : Category.{v, u₂} B
T : Type u₃
inst✝¹ : Category.{v, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
m : (coconeOfPreserves F t₁ c₂).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfPreserves F t₁ c₂).ι j ≫ m = NatTrans.app s.ι j
j : J
⊢ NatTrans.app c₂.ι j ≫ m.right = NatTrans.app ((snd L R).mapCocone s).ι j
[PROOFSTEP]
simp [← w]
[GOAL]
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v, u₁} A
B : Type u₂
inst✝¹ : Category.{v, u₂} B
T : Type u₃
inst✝ : Category.{v, u₃} T
F : J ⥤ Arrow T
i₁ : HasLimit (F ⋙ leftFunc)
i₂ : HasLimit (F ⋙ rightFunc)
⊢ HasLimit F
[PROOFSTEP]
haveI : HasLimit (F ⋙ Comma.fst _ _) := i₁
[GOAL]
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v, u₁} A
B : Type u₂
inst✝¹ : Category.{v, u₂} B
T : Type u₃
inst✝ : Category.{v, u₃} T
F : J ⥤ Arrow T
i₁ : HasLimit (F ⋙ leftFunc)
i₂ : HasLimit (F ⋙ rightFunc)
this : HasLimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
⊢ HasLimit F
[PROOFSTEP]
haveI : HasLimit (F ⋙ Comma.snd _ _) := i₂
[GOAL]
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v, u₁} A
B : Type u₂
inst✝¹ : Category.{v, u₂} B
T : Type u₃
inst✝ : Category.{v, u₃} T
F : J ⥤ Arrow T
i₁ : HasLimit (F ⋙ leftFunc)
i₂ : HasLimit (F ⋙ rightFunc)
this✝ : HasLimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
this : HasLimit (F ⋙ Comma.snd (𝟭 T) (𝟭 T))
⊢ HasLimit F
[PROOFSTEP]
apply Comma.hasLimit
[GOAL]
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v, u₁} A
B : Type u₂
inst✝¹ : Category.{v, u₂} B
T : Type u₃
inst✝ : Category.{v, u₃} T
F : J ⥤ Arrow T
i₁ : HasColimit (F ⋙ leftFunc)
i₂ : HasColimit (F ⋙ rightFunc)
⊢ HasColimit F
[PROOFSTEP]
haveI : HasColimit (F ⋙ Comma.fst _ _) := i₁
[GOAL]
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v, u₁} A
B : Type u₂
inst✝¹ : Category.{v, u₂} B
T : Type u₃
inst✝ : Category.{v, u₃} T
F : J ⥤ Arrow T
i₁ : HasColimit (F ⋙ leftFunc)
i₂ : HasColimit (F ⋙ rightFunc)
this : HasColimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
⊢ HasColimit F
[PROOFSTEP]
haveI : HasColimit (F ⋙ Comma.snd _ _) := i₂
[GOAL]
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v, u₁} A
B : Type u₂
inst✝¹ : Category.{v, u₂} B
T : Type u₃
inst✝ : Category.{v, u₃} T
F : J ⥤ Arrow T
i₁ : HasColimit (F ⋙ leftFunc)
i₂ : HasColimit (F ⋙ rightFunc)
this✝ : HasColimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
this : HasColimit (F ⋙ Comma.snd (𝟭 T) (𝟭 T))
⊢ HasColimit F
[PROOFSTEP]
apply Comma.hasColimit
[GOAL]
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v, u₁} A
B : Type u₂
inst✝¹ : Category.{v, u₂} B
T : Type u₃
inst✝ : Category.{v, u₃} T
X : T
G : A ⥤ T
F : J ⥤ StructuredArrow X G
i₁ : HasLimit (F ⋙ proj X G)
i₂ : PreservesLimit (F ⋙ proj X G) G
⊢ HasLimit F
[PROOFSTEP]
haveI : HasLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G) := i₁
[GOAL]
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v, u₁} A
B : Type u₂
inst✝¹ : Category.{v, u₂} B
T : Type u₃
inst✝ : Category.{v, u₃} T
X : T
G : A ⥤ T
F : J ⥤ StructuredArrow X G
i₁ : HasLimit (F ⋙ proj X G)
i₂ : PreservesLimit (F ⋙ proj X G) G
this : HasLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G)
⊢ HasLimit F
[PROOFSTEP]
haveI : PreservesLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G) _ := i₂
[GOAL]
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v, u₁} A
B : Type u₂
inst✝¹ : Category.{v, u₂} B
T : Type u₃
inst✝ : Category.{v, u₃} T
X : T
G : A ⥤ T
F : J ⥤ StructuredArrow X G
i₁ : HasLimit (F ⋙ proj X G)
i₂ : PreservesLimit (F ⋙ proj X G) G
this✝ : HasLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G)
this : PreservesLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G) G
⊢ HasLimit F
[PROOFSTEP]
apply Comma.hasLimit
[GOAL]
J✝ : Type w
inst✝⁵ : Category.{w', w} J✝
A : Type u₁
inst✝⁴ : Category.{v, u₁} A
B : Type u₂
inst✝³ : Category.{v, u₂} B
T : Type u₃
inst✝² : Category.{v, u₃} T
X : T
G : A ⥤ T
F : J✝ ⥤ StructuredArrow X G
inst✝¹ : HasLimits A
inst✝ : PreservesLimits G
J : Type v
hJ : Category.{v, v} J
⊢ HasLimitsOfShape J (StructuredArrow X G)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v, u₁} A
B : Type u₂
inst✝¹ : Category.{v, u₂} B
T : Type u₃
inst✝ : Category.{v, u₃} T
G : A ⥤ T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
⊢ HasColimit F
[PROOFSTEP]
haveI : HasColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) := i₁
[GOAL]
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v, u₁} A
B : Type u₂
inst✝¹ : Category.{v, u₂} B
T : Type u₃
inst✝ : Category.{v, u₃} T
G : A ⥤ T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
this : HasColimit (F ⋙ Comma.fst G (Functor.fromPUnit X))
⊢ HasColimit F
[PROOFSTEP]
haveI : PreservesColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) _ := i₂
[GOAL]
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v, u₁} A
B : Type u₂
inst✝¹ : Category.{v, u₂} B
T : Type u₃
inst✝ : Category.{v, u₃} T
G : A ⥤ T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
this✝ : HasColimit (F ⋙ Comma.fst G (Functor.fromPUnit X))
this : PreservesColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) G
⊢ HasColimit F
[PROOFSTEP]
apply Comma.hasColimit


[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
⊢ ∀ ⦃X Y : K⦄ (f : X ⟶ Y),
    (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).map f ≫
        (fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k) Y =
      (fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k) X ≫
        ((Functor.const K).obj (colimit.cocone ((curry.obj F).obj j)).1).map f
[PROOFSTEP]
intro k k' f
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k k' : K
f : k ⟶ k'
⊢ (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).map f ≫
      (fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k) k' =
    (fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k) k ≫
      ((Functor.const K).obj (colimit.cocone ((curry.obj F).obj j)).1).map f
[PROOFSTEP]
simp only [Functor.comp_obj, lim_obj, colimit.cocone_x, Functor.const_obj_obj, Functor.comp_map, lim_map,
  curry_obj_obj_obj, Prod.swap_obj, limMap_π_assoc, curry_obj_map_app, Prod.swap_map, Functor.const_obj_map,
  Category.comp_id]
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k k' : K
f : k ⟶ k'
⊢ limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ F.map (𝟙 j, f) ≫ colimit.ι ((curry.obj F).obj j) k' =
    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k
[PROOFSTEP]
rw [map_id_left_eq_curry_map, colimit.w]
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj (colimit.cocone (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)).1).map f ≫
        (fun j =>
            colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
              { pt := (colimit.cocone ((curry.obj F).obj j)).1,
                ι :=
                  NatTrans.mk fun k =>
                    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k })
          Y =
      (fun j =>
            colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
              { pt := (colimit.cocone ((curry.obj F).obj j)).1,
                ι :=
                  NatTrans.mk fun k =>
                    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k })
          X ≫
        (curry.obj F ⋙ colim).map f
[PROOFSTEP]
intro j j' f
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (colimit.cocone (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)).1).map f ≫
      (fun j =>
          colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
            { pt := (colimit.cocone ((curry.obj F).obj j)).1,
              ι :=
                NatTrans.mk fun k =>
                  limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k })
        j' =
    (fun j =>
          colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
            { pt := (colimit.cocone ((curry.obj F).obj j)).1,
              ι :=
                NatTrans.mk fun k =>
                  limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k })
        j ≫
      (curry.obj F ⋙ colim).map f
[PROOFSTEP]
dsimp
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j j' : J
f : j ⟶ j'
⊢ 𝟙 (colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)) ≫
      colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
        { pt := colimit ((curry.obj F).obj j'),
          ι :=
            NatTrans.mk fun k =>
              limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((curry.obj F).obj j') k } =
    colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
        { pt := colimit ((curry.obj F).obj j),
          ι :=
            NatTrans.mk fun k =>
              limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k } ≫
      colimMap ((curry.obj F).map f)
[PROOFSTEP]
ext k
[GOAL]
case w
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j j' : J
f : j ⟶ j'
k : K
⊢ colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k ≫
      𝟙 (colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)) ≫
        colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
          { pt := colimit ((curry.obj F).obj j'),
            ι :=
              NatTrans.mk fun k =>
                limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((curry.obj F).obj j') k } =
    colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k ≫
      colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
          { pt := colimit ((curry.obj F).obj j),
            ι :=
              NatTrans.mk fun k =>
                limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k } ≫
        colimMap ((curry.obj F).map f)
[PROOFSTEP]
simp only [Functor.comp_obj, lim_obj, Category.id_comp, colimit.ι_desc, colimit.ι_desc_assoc, Category.assoc,
  ι_colimMap, curry_obj_obj_obj, curry_obj_map_app]
[GOAL]
case w
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j j' : J
f : j ⟶ j'
k : K
⊢ limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((curry.obj F).obj j') k =
    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ F.map (f, 𝟙 k) ≫ colimit.ι ((curry.obj F).obj j') k
[PROOFSTEP]
rw [map_id_right_eq_curry_swap_map, limit.w_assoc]
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k ≫ colimitLimitToLimitColimit F ≫ limit.π (curry.obj F ⋙ colim) j =
    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k
[PROOFSTEP]
dsimp [colimitLimitToLimitColimit]
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k ≫
      limit.lift (curry.obj F ⋙ colim)
          { pt := colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim),
            π :=
              NatTrans.mk fun j =>
                colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
                  { pt := colimit ((curry.obj F).obj j),
                    ι :=
                      NatTrans.mk fun k =>
                        limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k } } ≫
        limit.π (curry.obj F ⋙ colim) j =
    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F✝ : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ limit.π (curry.obj F ⋙ colim) j (colimitLimitToLimitColimit F (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f)) =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)
[PROOFSTEP]
dsimp [colimitLimitToLimitColimit]
[GOAL]
J K : Type v
inst✝⁴ : SmallCategory J
inst✝³ : SmallCategory K
C : Type u
inst✝² : Category.{v, u} C
F✝ : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ limit.π (curry.obj F ⋙ colim) j
      (limit.lift (curry.obj F ⋙ colim)
        { pt := colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim),
          π :=
            NatTrans.mk fun j =>
              colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
                { pt := colimit ((curry.obj F).obj j),
                  ι :=
                    NatTrans.mk fun k =>
                      limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k } }
        (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f)) =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
⊢ (colim.map (limitIsoSwapCompLim G).hom ≫
        colimitLimitToLimitColimit (uncurry.obj G) ≫ lim.map (whiskerRight (currying.unitIso.app G).inv colim)) ≫
      NatTrans.app (limit.cone (G ⋙ colim)).π j =
    NatTrans.app (colim.mapCone (limit.cone G)).π j
[PROOFSTEP]
dsimp
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
⊢ (colimMap (limitIsoSwapCompLim G).hom ≫
        colimitLimitToLimitColimit (uncurry.obj G) ≫
          limMap (whiskerRight (NatTrans.app currying.unitIso.inv G) colim)) ≫
      limit.π (G ⋙ colim) j =
    colimMap (limit.π G j)
[PROOFSTEP]
ext1 k
[GOAL]
case w
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
k : K
⊢ colimit.ι (limit G) k ≫
      (colimMap (limitIsoSwapCompLim G).hom ≫
          colimitLimitToLimitColimit (uncurry.obj G) ≫
            limMap (whiskerRight (NatTrans.app currying.unitIso.inv G) colim)) ≫
        limit.π (G ⋙ colim) j =
    colimit.ι (limit G) k ≫ colimMap (limit.π G j)
[PROOFSTEP]
simp only [Category.assoc, limMap_π, Functor.comp_obj, colim_obj, whiskerRight_app, colim_map, ι_colimMap_assoc,
  lim_obj, limitIsoSwapCompLim_hom_app, ι_colimitLimitToLimitColimit_π_assoc, curry_obj_obj_obj, Prod.swap_obj,
  uncurry_obj_obj, ι_colimMap, currying_unitIso_inv_app_app_app, Category.id_comp, limMap_π_assoc, Functor.flip_obj_obj,
  flipIsoCurrySwapUncurry_hom_app_app]
[GOAL]
case w
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
k : K
⊢ (limitObjIsoLimitCompEvaluation G k).hom ≫ limit.π ((Functor.flip G).obj k) j ≫ colimit.ι (G.obj j) k =
    NatTrans.app (limit.π G j) k ≫ colimit.ι (G.obj j) k
[PROOFSTEP]
erw [limitObjIsoLimitCompEvaluation_hom_π_assoc]