[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
