[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
j : J
⊢ (coneMorphism c).Hom ≫ π F j = NatTrans.app c.π j
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (isoLimitCone t).hom ≫ NatTrans.app t.cone.π j = π F j
[PROOFSTEP]
dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ IsLimit.lift t.isLimit (cone F) ≫ NatTrans.app t.cone.π j = π F j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (isoLimitCone t).inv ≫ π F j = NatTrans.app t.cone.π j
[PROOFSTEP]
dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ lift F t.cone ≫ π F j = NatTrans.app t.cone.π j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
⊢ lift F c ≫ limMap α = lift G ((Cones.postcompose α).obj c)
[PROOFSTEP]
ext
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ (lift F c ≫ limMap α) ≫ π G j✝ = lift G ((Cones.postcompose α).obj c) ≫ π G j✝
[PROOFSTEP]
rw [assoc, limMap_π, limit.lift_π_assoc, limit.lift_π]
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ NatTrans.app c.π j✝ ≫ NatTrans.app α j✝ = NatTrans.app ((Cones.postcompose α).obj c).π j✝
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
X : C
f : X ⟶ c.pt
⊢ lift F (Cone.extend c f) = f ≫ lift F c
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
j : J
⊢ (fun s => limit.lift F ((Cones.postcompose α.inv).obj s)) s ≫
      NatTrans.app ((Cones.postcompose α.hom).obj (limit.cone F)).π j =
    NatTrans.app s.π j
[PROOFSTEP]
rw [Cones.postcompose_obj_π, NatTrans.comp_app, limit.cone_π, ← Category.assoc, limit.lift_π]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
j : J
⊢ NatTrans.app ((Cones.postcompose α.inv).obj s).π j ≫ NatTrans.app α.hom j = NatTrans.app s.π j
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
m : s.pt ⟶ ((Cones.postcompose α.hom).obj (limit.cone F)).pt
w : ∀ (j : J), m ≫ NatTrans.app ((Cones.postcompose α.hom).obj (limit.cone F)).π j = NatTrans.app s.π j
⊢ m = (fun s => limit.lift F ((Cones.postcompose α.inv).obj s)) s
[PROOFSTEP]
apply limit.hom_ext
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
m : s.pt ⟶ ((Cones.postcompose α.hom).obj (limit.cone F)).pt
w : ∀ (j : J), m ≫ NatTrans.app ((Cones.postcompose α.hom).obj (limit.cone F)).π j = NatTrans.app s.π j
⊢ ∀ (j : J), m ≫ limit.π F j = (fun s => limit.lift F ((Cones.postcompose α.inv).obj s)) s ≫ limit.π F j
[PROOFSTEP]
intro j
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
m : s.pt ⟶ ((Cones.postcompose α.hom).obj (limit.cone F)).pt
w : ∀ (j : J), m ≫ NatTrans.app ((Cones.postcompose α.hom).obj (limit.cone F)).π j = NatTrans.app s.π j
j : J
⊢ m ≫ limit.π F j = (fun s => limit.lift F ((Cones.postcompose α.inv).obj s)) s ≫ limit.π F j
[PROOFSTEP]
rw [limit.lift_π, Cones.postcompose_obj_π, NatTrans.comp_app, ← NatIso.app_inv, Iso.eq_comp_inv]
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasLimit F
α : F ≅ G
s : Cone G
m : s.pt ⟶ ((Cones.postcompose α.hom).obj (limit.cone F)).pt
w : ∀ (j : J), m ≫ NatTrans.app ((Cones.postcompose α.hom).obj (limit.cone F)).π j = NatTrans.app s.π j
j : J
⊢ (m ≫ limit.π F j) ≫ (α.app j).hom = NatTrans.app s.π j
[PROOFSTEP]
simpa using w j
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ (isoOfEquivalence e w).hom ≫ limit.π G k =
    limit.π F (e.inverse.obj k) ≫ NatTrans.app w.inv (e.inverse.obj k) ≫ G.map (NatTrans.app (Equivalence.counit e) k)
[PROOFSTEP]
simp only [HasLimit.isoOfEquivalence, IsLimit.conePointsIsoOfEquivalence_hom]
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ IsLimit.lift (limit.isLimit G)
        ((Cones.equivalenceOfReindexing (Equivalence.symm e)
                ((isoWhiskerLeft e.inverse w).symm ≪≫ Equivalence.invFunIdAssoc e G)).functor.obj
          (limit.cone F)) ≫
      limit.π G k =
    limit.π F (e.inverse.obj k) ≫ NatTrans.app w.inv (e.inverse.obj k) ≫ G.map (NatTrans.app (Equivalence.counit e) k)
[PROOFSTEP]
dsimp
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ limit.lift G
        ((Cones.postcompose (whiskerLeft e.inverse w.inv ≫ (Equivalence.invFunIdAssoc e G).hom)).obj
          (Cone.whisker e.inverse (limit.cone F))) ≫
      limit.π G k =
    limit.π F (e.inverse.obj k) ≫ NatTrans.app w.inv (e.inverse.obj k) ≫ G.map (NatTrans.app (Equivalence.counit e) k)
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ (isoOfEquivalence e w).inv ≫ limit.π F j = limit.π G (e.functor.obj j) ≫ NatTrans.app w.hom j
[PROOFSTEP]
simp only [HasLimit.isoOfEquivalence, IsLimit.conePointsIsoOfEquivalence_hom]
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ (IsLimit.conePointsIsoOfEquivalence (limit.isLimit F) (limit.isLimit G) e w).inv ≫ limit.π F j =
    limit.π G (e.functor.obj j) ≫ NatTrans.app w.hom j
[PROOFSTEP]
dsimp
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ limit.lift F ((Cones.postcompose w.hom).obj (Cone.whisker e.functor (limit.cone G))) ≫ limit.π F j =
    limit.π G (e.functor.obj j) ≫ NatTrans.app w.hom j
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
k : K
⊢ pre F E ≫ π (E ⋙ F) k = π F (E.obj k)
[PROOFSTEP]
erw [IsLimit.fac]
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
k : K
⊢ NatTrans.app (Cone.whisker E (cone F)).π k = π F (E.obj k)
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
c : Cone F
⊢ lift F c ≫ pre F E = lift (E ⋙ F) (Cone.whisker E c)
[PROOFSTEP]
ext
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
c : Cone F
j✝ : K
⊢ (lift F c ≫ pre F E) ≫ π (E ⋙ F) j✝ = lift (E ⋙ F) (Cone.whisker E c) ≫ π (E ⋙ F) j✝
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
inst✝³ : HasLimit F
E : K ⥤ J
inst✝² : HasLimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category.{v₃, u₃} L
D : L ⥤ K
inst✝ h : HasLimit (D ⋙ E ⋙ F)
⊢ pre F E ≫ pre (E ⋙ F) D = pre F (D ⋙ E)
[PROOFSTEP]
haveI : HasLimit ((D ⋙ E) ⋙ F) := h
[GOAL]
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
inst✝³ : HasLimit F
E : K ⥤ J
inst✝² : HasLimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category.{v₃, u₃} L
D : L ⥤ K
inst✝ h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
⊢ pre F E ≫ pre (E ⋙ F) D = pre F (D ⋙ E)
[PROOFSTEP]
ext j
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
inst✝³ : HasLimit F
E : K ⥤ J
inst✝² : HasLimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category.{v₃, u₃} L
D : L ⥤ K
inst✝ h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ (pre F E ≫ pre (E ⋙ F) D) ≫ π (D ⋙ E ⋙ F) j = pre F (D ⋙ E) ≫ π (D ⋙ E ⋙ F) j
[PROOFSTEP]
erw [assoc, limit.pre_π, limit.pre_π, limit.pre_π]
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
inst✝³ : HasLimit F
E : K ⥤ J
inst✝² : HasLimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category.{v₃, u₃} L
D : L ⥤ K
inst✝ h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ π F (E.obj (D.obj j)) = π F ((D ⋙ E).obj j)
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
inst✝³ : HasLimit F
E : K ⥤ J
inst✝² : HasLimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category.{v₃, u₃} L
D : L ⥤ K
inst✝ : HasLimit (D ⋙ E ⋙ F)
s : LimitCone (E ⋙ F)
t : LimitCone F
⊢ pre F E = (isoLimitCone t).hom ≫ IsLimit.lift s.isLimit (Cone.whisker E t.cone) ≫ (isoLimitCone s).inv
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
j : J
⊢ post F G ≫ π (F ⋙ G) j = G.map (π F j)
[PROOFSTEP]
erw [IsLimit.fac]
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
j : J
⊢ NatTrans.app (G.mapCone (cone F)).π j = G.map (π F j)
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
⊢ G.map (lift F c) ≫ post F G = lift (F ⋙ G) (G.mapCone c)
[PROOFSTEP]
ext
[GOAL]
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ (G.map (lift F c) ≫ post F G) ≫ π (F ⋙ G) j✝ = lift (F ⋙ G) (G.mapCone c) ≫ π (F ⋙ G) j✝
[PROOFSTEP]
rw [assoc, limit.post_π, ← G.map_comp, limit.lift_π, limit.lift_π]
[GOAL]
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ G.map (NatTrans.app c.π j✝) = NatTrans.app (G.mapCone c).π j✝
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
⊢ H.map (post F G) ≫ post (F ⋙ G) H = post F (G ⋙ H)
[PROOFSTEP]
haveI : HasLimit (F ⋙ G ⋙ H) := h
[GOAL]
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
⊢ H.map (post F G) ≫ post (F ⋙ G) H = post F (G ⋙ H)
[PROOFSTEP]
ext
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ (H.map (post F G) ≫ post (F ⋙ G) H) ≫ π ((F ⋙ G) ⋙ H) j✝ = post F (G ⋙ H) ≫ π ((F ⋙ G) ⋙ H) j✝
[PROOFSTEP]
erw [assoc, limit.post_π, ← H.map_comp, limit.post_π, limit.post_π]
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ H.map (G.map (π F j✝)) = (G ⋙ H).map (π F j✝)
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F✝ : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
⊢ G.map (pre F E) ≫ post (E ⋙ F) G = post F G ≫ pre (F ⋙ G) E
[PROOFSTEP]
haveI : HasLimit (E ⋙ F ⋙ G) := h
[GOAL]
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F✝ : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
⊢ G.map (pre F E) ≫ post (E ⋙ F) G = post F G ≫ pre (F ⋙ G) E
[PROOFSTEP]
ext
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F✝ : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j✝ : K
⊢ (G.map (pre F E) ≫ post (E ⋙ F) G) ≫ π ((E ⋙ F) ⋙ G) j✝ = (post F G ≫ pre (F ⋙ G) E) ≫ π ((E ⋙ F) ⋙ G) j✝
[PROOFSTEP]
erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
⊢ HasLimit F
[PROOFSTEP]
haveI : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimitEquivalenceComp e.symm
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
this : HasLimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasLimit F
[PROOFSTEP]
apply hasLimitOfIso (e.invFunIdAssoc F)
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ : J ⥤ C
inst✝ : HasLimitsOfShape J C
F : J ⥤ C
⊢ { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map (𝟙 F) =
    𝟙 ({ obj := fun F => limit F, map := fun {X Y} α => limMap α }.obj F)
[PROOFSTEP]
apply Limits.limit.hom_ext
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ : J ⥤ C
inst✝ : HasLimitsOfShape J C
F : J ⥤ C
⊢ ∀ (j : J),
    { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map (𝟙 F) ≫ limit.π F j =
      𝟙 ({ obj := fun F => limit F, map := fun {X Y} α => limMap α }.obj F) ≫ limit.π F j
[PROOFSTEP]
intro j
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ : J ⥤ C
inst✝ : HasLimitsOfShape J C
F : J ⥤ C
j : J
⊢ { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map (𝟙 F) ≫ limit.π F j =
    𝟙 ({ obj := fun F => limit F, map := fun {X Y} α => limMap α }.obj F) ≫ limit.π F j
[PROOFSTEP]
erw [limMap_π, Category.id_comp, Category.comp_id]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimitsOfShape J C
X✝ Y✝ Z✝ : J ⥤ C
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
⊢ { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map (α ≫ β) =
    { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map α ≫
      { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map β
[PROOFSTEP]
apply Limits.limit.hom_ext
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimitsOfShape J C
X✝ Y✝ Z✝ : J ⥤ C
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
⊢ ∀ (j : J),
    { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map (α ≫ β) ≫ limit.π Z✝ j =
      ({ obj := fun F => limit F, map := fun {X Y} α => limMap α }.map α ≫
          { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map β) ≫
        limit.π Z✝ j
[PROOFSTEP]
intro j
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimitsOfShape J C
X✝ Y✝ Z✝ : J ⥤ C
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
j : J
⊢ { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map (α ≫ β) ≫ limit.π Z✝ j =
    ({ obj := fun F => limit F, map := fun {X Y} α => limMap α }.map α ≫
        { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map β) ≫
      limit.π Z✝ j
[PROOFSTEP]
erw [assoc, IsLimit.fac, IsLimit.fac, ← assoc, IsLimit.fac, assoc]
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimitsOfShape J C
X✝ Y✝ Z✝ : J ⥤ C
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
j : J
⊢ NatTrans.app ((Cones.postcompose (α ≫ β)).obj (limit.cone X✝)).π j =
    NatTrans.app (limit.cone X✝).π j ≫ NatTrans.app α j ≫ NatTrans.app β j
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasLimitsOfShape K C
E : K ⥤ J
⊢ lim.map α ≫ pre G E = pre F E ≫ lim.map (whiskerLeft E α)
[PROOFSTEP]
ext
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasLimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ (lim.map α ≫ pre G E) ≫ π (E ⋙ G) j✝ = (pre F E ≫ lim.map (whiskerLeft E α)) ≫ π (E ⋙ G) j✝
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ : J ⥤ C
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α✝ : F✝ ⟶ G
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
⊢ pre F E₂ = pre F E₁ ≫ lim.map (whiskerRight α F)
[PROOFSTEP]
ext1
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ : J ⥤ C
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α✝ : F✝ ⟶ G
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
j✝ : K
⊢ pre F E₂ ≫ π (E₂ ⋙ F) j✝ = (pre F E₁ ≫ lim.map (whiskerRight α F)) ≫ π (E₂ ⋙ F) j✝
[PROOFSTEP]
simp [← category.assoc]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ : J ⥤ C
inst✝ : HasLimitsOfShape J C
G : J ⥤ C
α : F✝ ⟶ G
F : J ⥤ C
⊢ pre F (𝟭 J) = lim.map (leftUnitor F).inv
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasLimitsOfShape J D
H : C ⥤ D
⊢ H.map (limMap α) ≫ post G H = post F H ≫ limMap (whiskerRight α H)
[PROOFSTEP]
ext
[GOAL]
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasLimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ (H.map (limMap α) ≫ post G H) ≫ π (G ⋙ H) j✝ = (post F H ≫ limMap (whiskerRight α H)) ≫ π (G ⋙ H) j✝
[PROOFSTEP]
simp only [whiskerRight_app, limMap_π, assoc, limit.post_π_assoc, limit.post_π, ← H.map_comp]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : C
g : J ⥤ C
⊢ Function.LeftInverse (fun f => NatTrans.mk fun j => f ≫ limit.π g j) fun f => limit.lift g { pt := c, π := f }
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : C
g : J ⥤ C
⊢ Function.RightInverse (fun f => NatTrans.mk fun j => f ≫ limit.π g j) fun f => limit.lift g { pt := c, π := f }
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit G
α : F ⟶ G
inst✝ : ∀ (j : J), Mono (NatTrans.app α j)
Z : C
u v : Z ⟶ limit F
h : u ≫ limMap α = v ≫ limMap α
j : J
⊢ (u ≫ limit.π F j) ≫ NatTrans.app α j = (v ≫ limit.π F j) ≫ NatTrans.app α j
[PROOFSTEP]
simpa using h =≫ limit.π _ j
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J' C
[PROOFSTEP]
constructor
[GOAL]
case has_limit
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
⊢ autoParam (∀ (F : J' ⥤ C), HasLimit F) _auto✝
[PROOFSTEP]
intro F
[GOAL]
case has_limit
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ : J ⥤ C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
F : J' ⥤ C
⊢ HasLimit F
[PROOFSTEP]
apply hasLimitOfEquivalenceComp e
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
j : J
⊢ ι F j ≫ (coconeMorphism c).Hom = NatTrans.app c.ι j
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasColimit F
t : ColimitCocone F
j : J
⊢ ι F j ≫ (isoColimitCocone t).hom = NatTrans.app t.cocone.ι j
[PROOFSTEP]
dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasColimit F
t : ColimitCocone F
j : J
⊢ ι F j ≫ desc F t.cocone = NatTrans.app t.cocone.ι j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasColimit F
t : ColimitCocone F
j : J
⊢ NatTrans.app t.cocone.ι j ≫ (isoColimitCocone t).inv = ι F j
[PROOFSTEP]
dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasColimit F
t : ColimitCocone F
j : J
⊢ NatTrans.app t.cocone.ι j ≫ IsColimit.desc t.isColimit (cocone F) = ι F j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
X : C
f : c.pt ⟶ X
⊢ desc F (Cocone.extend c f) = desc F c ≫ f
[PROOFSTEP]
ext1
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
X : C
f : c.pt ⟶ X
j✝ : J
⊢ ι F j✝ ≫ desc F (Cocone.extend c f) = ι F j✝ ≫ desc F c ≫ f
[PROOFSTEP]
rw [← Category.assoc]
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
X : C
f : c.pt ⟶ X
j✝ : J
⊢ ι F j✝ ≫ desc F (Cocone.extend c f) = (ι F j✝ ≫ desc F c) ≫ f
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
j : J
⊢ NatTrans.app ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι j ≫
      (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s =
    NatTrans.app s.ι j
[PROOFSTEP]
rw [Cocones.precompose_obj_ι, NatTrans.comp_app, colimit.cocone_ι]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
j : J
⊢ (NatTrans.app α.hom j ≫ colimit.ι F j) ≫ (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s =
    NatTrans.app s.ι j
[PROOFSTEP]
rw [Category.assoc, colimit.ι_desc, ← NatIso.app_hom, ← Iso.eq_inv_comp]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
j : J
⊢ NatTrans.app ((Cocones.precompose α.inv).obj s).ι j = (α.app j).inv ≫ NatTrans.app s.ι j
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
m : ((Cocones.precompose α.hom).obj (colimit.cocone F)).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
m : ((Cocones.precompose α.hom).obj (colimit.cocone F)).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι j ≫ m = NatTrans.app s.ι j
⊢ ∀ (j : J), colimit.ι F j ≫ m = colimit.ι F j ≫ (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s
[PROOFSTEP]
intro j
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
m : ((Cocones.precompose α.hom).obj (colimit.cocone F)).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι j ≫ m = NatTrans.app s.ι j
j : J
⊢ colimit.ι F j ≫ m = colimit.ι F j ≫ (fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)) s
[PROOFSTEP]
rw [colimit.ι_desc, Cocones.precompose_obj_ι, NatTrans.comp_app, ← NatIso.app_inv, Iso.eq_inv_comp]
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝ : HasColimit F
α : G ≅ F
s : Cocone G
m : ((Cocones.precompose α.hom).obj (colimit.cocone F)).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app ((Cocones.precompose α.hom).obj (colimit.cocone F)).ι j ≫ m = NatTrans.app s.ι j
j : J
⊢ (α.app j).hom ≫ colimit.ι F j ≫ m = NatTrans.app s.ι j
[PROOFSTEP]
simpa using w j
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ F : J ⥤ C
inst✝¹ : HasColimit F
G : K ⥤ C
inst✝ : HasColimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ colimit.ι F j ≫ (isoOfEquivalence e w).hom =
    F.map (NatTrans.app (Equivalence.unit e) j) ≫
      NatTrans.app w.inv ((e.functor ⋙ e.inverse).obj j) ≫ colimit.ι G (e.functor.obj ((e.functor ⋙ e.inverse).obj j))
[PROOFSTEP]
simp [HasColimit.isoOfEquivalence, IsColimit.coconePointsIsoOfEquivalence_inv]
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ F : J ⥤ C
inst✝¹ : HasColimit F
G : K ⥤ C
inst✝ : HasColimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ colimit.ι G k ≫ (isoOfEquivalence e w).inv =
    G.map (NatTrans.app (Equivalence.counitInv e) k) ≫
      NatTrans.app w.hom (e.inverse.obj k) ≫ colimit.ι F (e.inverse.obj k)
[PROOFSTEP]
simp [HasColimit.isoOfEquivalence, IsColimit.coconePointsIsoOfEquivalence_inv]
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
k : K
⊢ ι (E ⋙ F) k ≫ pre F E = ι F (E.obj k)
[PROOFSTEP]
erw [IsColimit.fac]
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
k : K
⊢ NatTrans.app (Cocone.whisker E (cocone F)).ι k = ι F (E.obj k)
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
⊢ pre F E ≫ desc F c = desc (E ⋙ F) (Cocone.whisker E c)
[PROOFSTEP]
ext
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
j✝ : K
⊢ ι (E ⋙ F) j✝ ≫ pre F E ≫ desc F c = ι (E ⋙ F) j✝ ≫ desc (E ⋙ F) (Cocone.whisker E c)
[PROOFSTEP]
rw [← assoc, colimit.ι_pre]
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
j✝ : K
⊢ ι F (E.obj j✝) ≫ desc F c = ι (E ⋙ F) j✝ ≫ desc (E ⋙ F) (Cocone.whisker E c)
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
inst✝³ : HasColimit F
E : K ⥤ J
inst✝² : HasColimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category.{v₃, u₃} L
D : L ⥤ K
inst✝ h : HasColimit (D ⋙ E ⋙ F)
⊢ pre (E ⋙ F) D ≫ pre F E = pre F (D ⋙ E)
[PROOFSTEP]
ext j
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
inst✝³ : HasColimit F
E : K ⥤ J
inst✝² : HasColimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category.{v₃, u₃} L
D : L ⥤ K
inst✝ h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι (D ⋙ E ⋙ F) j ≫ pre (E ⋙ F) D ≫ pre F E = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
[PROOFSTEP]
rw [← assoc, colimit.ι_pre, colimit.ι_pre]
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
inst✝³ : HasColimit F
E : K ⥤ J
inst✝² : HasColimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category.{v₃, u₃} L
D : L ⥤ K
inst✝ h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
[PROOFSTEP]
haveI : HasColimit ((D ⋙ E) ⋙ F) := h
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
inst✝³ : HasColimit F
E : K ⥤ J
inst✝² : HasColimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category.{v₃, u₃} L
D : L ⥤ K
inst✝ h : HasColimit (D ⋙ E ⋙ F)
j : L
this : HasColimit ((D ⋙ E) ⋙ F)
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
[PROOFSTEP]
exact (colimit.ι_pre F (D ⋙ E) j).symm
[GOAL]
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
inst✝³ : HasColimit F
E : K ⥤ J
inst✝² : HasColimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category.{v₃, u₃} L
D : L ⥤ K
inst✝ : HasColimit (D ⋙ E ⋙ F)
s : ColimitCocone (E ⋙ F)
t : ColimitCocone F
⊢ pre F E = (isoColimitCocone s).hom ≫ IsColimit.desc s.isColimit (Cocone.whisker E t.cocone) ≫ (isoColimitCocone t).inv
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
j : J
⊢ ι (F ⋙ G) j ≫ post F G = G.map (ι F j)
[PROOFSTEP]
erw [IsColimit.fac]
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
j : J
⊢ NatTrans.app (G.mapCocone (cocone F)).ι j = G.map (ι F j)
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
⊢ post F G ≫ G.map (desc F c) = desc (F ⋙ G) (G.mapCocone c)
[PROOFSTEP]
ext
[GOAL]
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ ι (F ⋙ G) j✝ ≫ post F G ≫ G.map (desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)
[PROOFSTEP]
rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_desc, colimit.ι_desc]
[GOAL]
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (NatTrans.app c.ι j✝) = NatTrans.app (G.mapCocone c).ι j✝
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
⊢ post (F ⋙ G) H ≫ H.map (post F G) = post F (G ⋙ H)
[PROOFSTEP]
ext j
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ ι ((F ⋙ G) ⋙ H) j ≫ post (F ⋙ G) H ≫ H.map (post F G) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)
[PROOFSTEP]
rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_post]
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ H.map (G.map (ι F j)) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)
[PROOFSTEP]
haveI : HasColimit (F ⋙ G ⋙ H) := h
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
this : HasColimit (F ⋙ G ⋙ H)
⊢ H.map (G.map (ι F j)) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)
[PROOFSTEP]
exact (colimit.ι_post F (G ⋙ H) j).symm
[GOAL]
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F✝ : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
⊢ post (E ⋙ F) G ≫ G.map (pre F E) = pre (F ⋙ G) E ≫ post F G
[PROOFSTEP]
ext j
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F✝ : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ ι ((E ⋙ F) ⋙ G) j ≫ post (E ⋙ F) G ≫ G.map (pre F E) = ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E ≫ post F G
[PROOFSTEP]
rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_pre, ← assoc]
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F✝ : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ G.map (ι F (E.obj j)) = (ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E) ≫ post F G
[PROOFSTEP]
haveI : HasColimit (E ⋙ F ⋙ G) := h
[GOAL]
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
F✝ : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
this : HasColimit (E ⋙ F ⋙ G)
⊢ G.map (ι F (E.obj j)) = (ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E) ≫ post F G
[PROOFSTEP]
erw [colimit.ι_pre (F ⋙ G) E j, colimit.ι_post]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasColimit (e.functor ⋙ F)
⊢ HasColimit F
[PROOFSTEP]
haveI : HasColimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasColimit_equivalence_comp e.symm
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasColimit (e.functor ⋙ F)
this : HasColimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasColimit F
[PROOFSTEP]
apply hasColimitOfIso (e.invFunIdAssoc F).symm
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
j : J
⊢ ι F j ≫ colim.map α = NatTrans.app α j ≫ ι G j
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : Cocone G
⊢ colimMap α ≫ desc G c = desc F ((Cocones.precompose α).obj c)
[PROOFSTEP]
ext j
[GOAL]
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : Cocone G
j : J
⊢ ι F j ≫ colimMap α ≫ desc G c = ι F j ≫ desc F ((Cocones.precompose α).obj c)
[PROOFSTEP]
simp [← assoc, colimit.ι_map, assoc, colimit.ι_desc, colimit.ι_desc]
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
⊢ pre F E ≫ colim.map α = colim.map (whiskerLeft E α) ≫ pre G E
[PROOFSTEP]
ext
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ ι (E ⋙ F) j✝ ≫ pre F E ≫ colim.map α = ι (E ⋙ F) j✝ ≫ colim.map (whiskerLeft E α) ≫ pre G E
[PROOFSTEP]
rw [← assoc, colimit.ι_pre, colimit.ι_map, ← assoc, colimit.ι_map, assoc, colimit.ι_pre]
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ NatTrans.app α (E.obj j✝) ≫ ι G (E.obj j✝) = NatTrans.app (whiskerLeft E α) j✝ ≫ ι G (E.obj j✝)
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α✝ : F✝ ⟶ G
inst✝ : HasColimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
⊢ pre F E₁ = colim.map (whiskerRight α F) ≫ pre F E₂
[PROOFSTEP]
ext1
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α✝ : F✝ ⟶ G
inst✝ : HasColimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
j✝ : K
⊢ ι (E₁ ⋙ F) j✝ ≫ pre F E₁ = ι (E₁ ⋙ F) j✝ ≫ colim.map (whiskerRight α F) ≫ pre F E₂
[PROOFSTEP]
simp [← Category.assoc]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F✝ ⟶ G
F : J ⥤ C
⊢ pre F (𝟭 J) = colim.map (leftUnitor F).hom
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
⊢ post F H ≫ H.map (colim.map α) = colim.map (whiskerRight α H) ≫ post G H
[PROOFSTEP]
ext
[GOAL]
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ ι (F ⋙ H) j✝ ≫ post F H ≫ H.map (colim.map α) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H
[PROOFSTEP]
rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_map, H.map_comp]
[GOAL]
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ H.map (NatTrans.app α j✝) ≫ H.map (ι G j✝) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H
[PROOFSTEP]
rw [← assoc, colimit.ι_map, assoc, colimit.ι_post]
[GOAL]
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ H.map (NatTrans.app α j✝) ≫ H.map (ι G j✝) = NatTrans.app (whiskerRight α H) j✝ ≫ H.map (ι G j✝)
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
f : J ⥤ C
c : C
⊢ Function.LeftInverse (fun g => colimit.desc f { pt := c, ι := g }) fun g => NatTrans.mk fun x => colimit.ι f x ≫ g
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
f : J ⥤ C
c : C
⊢ Function.RightInverse (fun g => colimit.desc f { pt := c, ι := g }) fun g => NatTrans.mk fun x => colimit.ι f x ≫ g
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝² : HasColimit F
inst✝¹ : HasColimit G
α : F ⟶ G
inst✝ : ∀ (j : J), Epi (NatTrans.app α j)
Z : C
u v : colimit G ⟶ Z
h : colimMap α ≫ u = colimMap α ≫ v
j : J
⊢ NatTrans.app α j ≫ colimit.ι G j ≫ u = NatTrans.app α j ≫ colimit.ι G j ≫ v
[PROOFSTEP]
simpa using colimit.ι _ j ≫= h
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J' C
[PROOFSTEP]
constructor
[GOAL]
case has_colimit
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
⊢ autoParam (∀ (F : J' ⥤ C), HasColimit F) _auto✝
[PROOFSTEP]
intro F
[GOAL]
case has_colimit
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F✝ : J ⥤ C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
F : J' ⥤ C
⊢ HasColimit F
[PROOFSTEP]
apply hasColimit_of_equivalence_comp e
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : (Cone.op t).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (Cone.op t).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => (lift P (Cocone.unop s)).op) s
[PROOFSTEP]
dsimp
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : (Cone.op t).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (Cone.op t).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (lift P (Cocone.unop s)).op
[PROOFSTEP]
rw [← P.uniq s.unop m.unop]
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : (Cone.op t).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (Cone.op t).ι j ≫ m = NatTrans.app s.ι j
⊢ m = m.unop.op
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : (Cone.op t).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (Cone.op t).ι j ≫ m = NatTrans.app s.ι j
⊢ ∀ (j : J), m.unop ≫ NatTrans.app t.π j = NatTrans.app (Cocone.unop s).π j
[PROOFSTEP]
dsimp
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : (Cone.op t).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (Cone.op t).ι j ≫ m = NatTrans.app s.ι j
⊢ ∀ (j : J), m.unop ≫ NatTrans.app t.π j = (NatTrans.app s.ι (Opposite.op j)).unop
[PROOFSTEP]
intro j
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : (Cone.op t).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (Cone.op t).ι j ≫ m = NatTrans.app s.ι j
j : J
⊢ m.unop ≫ NatTrans.app t.π j = (NatTrans.app s.ι (Opposite.op j)).unop
[PROOFSTEP]
rw [← w]
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : (Cone.op t).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), NatTrans.app (Cone.op t).ι j ≫ m = NatTrans.app s.ι j
j : J
⊢ m.unop ≫ NatTrans.app t.π j = (NatTrans.app (Cone.op t).ι (Opposite.op j) ≫ m).unop
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ (Cocone.op t).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (Cocone.op t).π j = NatTrans.app s.π j
⊢ m = (fun s => (desc P (Cone.unop s)).op) s
[PROOFSTEP]
dsimp
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ (Cocone.op t).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (Cocone.op t).π j = NatTrans.app s.π j
⊢ m = (desc P (Cone.unop s)).op
[PROOFSTEP]
rw [← P.uniq s.unop m.unop]
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ (Cocone.op t).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (Cocone.op t).π j = NatTrans.app s.π j
⊢ m = m.unop.op
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ (Cocone.op t).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (Cocone.op t).π j = NatTrans.app s.π j
⊢ ∀ (j : J), NatTrans.app t.ι j ≫ m.unop = NatTrans.app (Cone.unop s).ι j
[PROOFSTEP]
dsimp
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ (Cocone.op t).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (Cocone.op t).π j = NatTrans.app s.π j
⊢ ∀ (j : J), NatTrans.app t.ι j ≫ m.unop = (NatTrans.app s.π (Opposite.op j)).unop
[PROOFSTEP]
intro j
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ (Cocone.op t).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (Cocone.op t).π j = NatTrans.app s.π j
j : J
⊢ NatTrans.app t.ι j ≫ m.unop = (NatTrans.app s.π (Opposite.op j)).unop
[PROOFSTEP]
rw [← w]
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ (Cocone.op t).pt
w : ∀ (j : Jᵒᵖ), m ≫ NatTrans.app (Cocone.op t).π j = NatTrans.app s.π j
j : J
⊢ NatTrans.app t.ι j ≫ m.unop = (m ≫ NatTrans.app (Cocone.op t).π (Opposite.op j)).unop
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : (Cone.unop t).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (Cone.unop t).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => (lift P (Cocone.op s)).unop) s
[PROOFSTEP]
dsimp
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : (Cone.unop t).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (Cone.unop t).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (lift P (Cocone.op s)).unop
[PROOFSTEP]
rw [← P.uniq s.op m.op]
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : (Cone.unop t).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (Cone.unop t).ι j ≫ m = NatTrans.app s.ι j
⊢ m = m.op.unop
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : (Cone.unop t).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (Cone.unop t).ι j ≫ m = NatTrans.app s.ι j
⊢ ∀ (j : Jᵒᵖ), m.op ≫ NatTrans.app t.π j = NatTrans.app (Cocone.op s).π j
[PROOFSTEP]
dsimp
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : (Cone.unop t).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (Cone.unop t).ι j ≫ m = NatTrans.app s.ι j
⊢ ∀ (j : Jᵒᵖ), m.op ≫ NatTrans.app t.π j = (NatTrans.app s.ι j.unop).op
[PROOFSTEP]
intro j
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : (Cone.unop t).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (Cone.unop t).ι j ≫ m = NatTrans.app s.ι j
j : Jᵒᵖ
⊢ m.op ≫ NatTrans.app t.π j = (NatTrans.app s.ι j.unop).op
[PROOFSTEP]
rw [← w]
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : (Cone.unop t).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (Cone.unop t).ι j ≫ m = NatTrans.app s.ι j
j : Jᵒᵖ
⊢ m.op ≫ NatTrans.app t.π j = (NatTrans.app (Cone.unop t).ι j.unop ≫ m).op
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ (Cocone.unop t).pt
w : ∀ (j : J), m ≫ NatTrans.app (Cocone.unop t).π j = NatTrans.app s.π j
⊢ m = (fun s => (desc P (Cone.op s)).unop) s
[PROOFSTEP]
dsimp
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ (Cocone.unop t).pt
w : ∀ (j : J), m ≫ NatTrans.app (Cocone.unop t).π j = NatTrans.app s.π j
⊢ m = (desc P (Cone.op s)).unop
[PROOFSTEP]
rw [← P.uniq s.op m.op]
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ (Cocone.unop t).pt
w : ∀ (j : J), m ≫ NatTrans.app (Cocone.unop t).π j = NatTrans.app s.π j
⊢ m = m.op.unop
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ (Cocone.unop t).pt
w : ∀ (j : J), m ≫ NatTrans.app (Cocone.unop t).π j = NatTrans.app s.π j
⊢ ∀ (j : Jᵒᵖ), NatTrans.app t.ι j ≫ m.op = NatTrans.app (Cone.op s).ι j
[PROOFSTEP]
dsimp
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ (Cocone.unop t).pt
w : ∀ (j : J), m ≫ NatTrans.app (Cocone.unop t).π j = NatTrans.app s.π j
⊢ ∀ (j : Jᵒᵖ), NatTrans.app t.ι j ≫ m.op = (NatTrans.app s.π j.unop).op
[PROOFSTEP]
intro j
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ (Cocone.unop t).pt
w : ∀ (j : J), m ≫ NatTrans.app (Cocone.unop t).π j = NatTrans.app s.π j
j : Jᵒᵖ
⊢ NatTrans.app t.ι j ≫ m.op = (NatTrans.app s.π j.unop).op
[PROOFSTEP]
rw [← w]
[GOAL]
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ (Cocone.unop t).pt
w : ∀ (j : J), m ≫ NatTrans.app (Cocone.unop t).π j = NatTrans.app s.π j
j : Jᵒᵖ
⊢ NatTrans.app t.ι j ≫ m.op = (m ≫ NatTrans.app (Cocone.unop t).π j.unop).op
[PROOFSTEP]
rfl


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ IsLimit (G.mapCone (Fan.mk P g)) ≃ IsLimit (Fan.mk (G.obj P) fun j => G.map (g j))
[PROOFSTEP]
refine' (IsLimit.postcomposeHomEquiv _ _).symm.trans (IsLimit.equivIsoLimit _)
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ (Discrete.functor fun b => f b) ⋙ G ≅ Discrete.functor fun j => G.obj (f j)
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ (Cones.postcompose ?refine'_1.hom).obj (G.mapCone (Fan.mk P g)) ≅ Fan.mk (G.obj P) fun j => G.map (g j)
[PROOFSTEP]
refine' Discrete.natIso fun j => Iso.refl (G.obj (f j.as))
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ (Cones.postcompose (Discrete.natIso fun j => Iso.refl (G.obj (f j.as))).hom).obj (G.mapCone (Fan.mk P g)) ≅
    Fan.mk (G.obj P) fun j => G.map (g j)
[PROOFSTEP]
refine' Cones.ext (Iso.refl _) fun j => by dsimp; cases j; simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
j : Discrete J
⊢ NatTrans.app
      ((Cones.postcompose (Discrete.natIso fun j => Iso.refl (G.obj (f j.as))).hom).obj (G.mapCone (Fan.mk P g))).π j =
    (Iso.refl
          ((Cones.postcompose (Discrete.natIso fun j => Iso.refl (G.obj (f j.as))).hom).obj
              (G.mapCone (Fan.mk P g))).pt).hom ≫
      NatTrans.app (Fan.mk (G.obj P) fun j => G.map (g j)).π j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
j : Discrete J
⊢ G.map (g j.as) ≫ 𝟙 (G.obj (f j.as)) = 𝟙 (G.obj P) ≫ G.map (g j.as)
[PROOFSTEP]
cases j
[GOAL]
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
as✝ : J
⊢ G.map (g { as := as✝ }.as) ≫ 𝟙 (G.obj (f { as := as✝ }.as)) = 𝟙 (G.obj P) ≫ G.map (g { as := as✝ }.as)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun j => G.obj (f j)
i : IsIso (piComparison G f)
⊢ PreservesLimit (Discrete.functor f) G
[PROOFSTEP]
apply preservesLimitOfPreservesLimitCone (productIsProduct f)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun j => G.obj (f j)
i : IsIso (piComparison G f)
⊢ IsLimit (G.mapCone (Fan.mk (∏ f) (Pi.π f)))
[PROOFSTEP]
apply (isLimitMapConeFanMkEquiv _ _ _).symm _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun j => G.obj (f j)
i : IsIso (piComparison G f)
⊢ IsLimit (Fan.mk (G.obj (∏ f)) fun j => G.map (Pi.π f j))
[PROOFSTEP]
refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (Discrete.functor fun j : J => G.obj (f j))) ?_
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun j => G.obj (f j)
i : IsIso (piComparison G f)
⊢ IsIso
    (IsLimit.lift (limit.isLimit (Discrete.functor fun j => G.obj (f j)))
      (Fan.mk (G.obj (∏ f)) fun j => G.map (Pi.π f j)))
[PROOFSTEP]
apply i
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝² : HasProduct f
inst✝¹ : HasProduct fun j => G.obj (f j)
inst✝ : PreservesLimit (Discrete.functor f) G
⊢ IsIso (piComparison G f)
[PROOFSTEP]
rw [← PreservesProduct.iso_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝² : HasProduct f
inst✝¹ : HasProduct fun j => G.obj (f j)
inst✝ : PreservesLimit (Discrete.functor f) G
⊢ IsIso (PreservesProduct.iso G f).hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ IsColimit (G.mapCocone (Cofan.mk P g)) ≃ IsColimit (Cofan.mk (G.obj P) fun j => G.map (g j))
[PROOFSTEP]
refine' (IsColimit.precomposeHomEquiv _ _).symm.trans (IsColimit.equivIsoColimit _)
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ (Discrete.functor fun j => G.obj (f j)) ≅ (Discrete.functor fun b => f b) ⋙ G
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ (Cocones.precompose ?refine'_1.hom).obj (G.mapCocone (Cofan.mk P g)) ≅ Cofan.mk (G.obj P) fun j => G.map (g j)
[PROOFSTEP]
refine' Discrete.natIso fun j => Iso.refl (G.obj (f j.as))
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ (Cocones.precompose (Discrete.natIso fun j => Iso.refl (G.obj (f j.as))).hom).obj (G.mapCocone (Cofan.mk P g)) ≅
    Cofan.mk (G.obj P) fun j => G.map (g j)
[PROOFSTEP]
refine' Cocones.ext (Iso.refl _) fun j => by dsimp; cases j; simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
j : Discrete J
⊢ NatTrans.app
        ((Cocones.precompose (Discrete.natIso fun j => Iso.refl (G.obj (f j.as))).hom).obj
            (G.mapCocone (Cofan.mk P g))).ι
        j ≫
      (Iso.refl
          ((Cocones.precompose (Discrete.natIso fun j => Iso.refl (G.obj (f j.as))).hom).obj
              (G.mapCocone (Cofan.mk P g))).pt).hom =
    NatTrans.app (Cofan.mk (G.obj P) fun j => G.map (g j)).ι j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
j : Discrete J
⊢ (𝟙 (G.obj (f j.as)) ≫ G.map (g j.as)) ≫ 𝟙 (G.obj P) = G.map (g j.as)
[PROOFSTEP]
cases j
[GOAL]
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
as✝ : J
⊢ (𝟙 (G.obj (f { as := as✝ }.as)) ≫ G.map (g { as := as✝ }.as)) ≫ 𝟙 (G.obj P) = G.map (g { as := as✝ }.as)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun j => G.obj (f j)
i : IsIso (sigmaComparison G f)
⊢ PreservesColimit (Discrete.functor f) G
[PROOFSTEP]
apply preservesColimitOfPreservesColimitCocone (coproductIsCoproduct f)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun j => G.obj (f j)
i : IsIso (sigmaComparison G f)
⊢ IsColimit (G.mapCocone (Cofan.mk (∐ f) (Sigma.ι f)))
[PROOFSTEP]
apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun j => G.obj (f j)
i : IsIso (sigmaComparison G f)
⊢ IsColimit (Cofan.mk (G.obj (∐ f)) fun j => G.map (Sigma.ι f j))
[PROOFSTEP]
refine @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (Discrete.functor fun j : J => G.obj (f j))) ?_
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun j => G.obj (f j)
i : IsIso (sigmaComparison G f)
⊢ IsIso
    (IsColimit.desc (colimit.isColimit (Discrete.functor fun j => G.obj (f j)))
      (Cofan.mk (G.obj (∐ f)) fun j => G.map (Sigma.ι f j)))
[PROOFSTEP]
apply i
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct fun j => G.obj (f j)
inst✝ : PreservesColimit (Discrete.functor f) G
⊢ IsIso (sigmaComparison G f)
[PROOFSTEP]
rw [← PreservesCoproduct.inv_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct fun j => G.obj (f j)
inst✝ : PreservesColimit (Discrete.functor f) G
⊢ IsIso (PreservesCoproduct.iso G f).inv
[PROOFSTEP]
infer_instance