[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesLimit K F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : PreservesLimit K F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
a b : {c : Cone K} → IsLimit c → IsLimit (F.mapCone c)
⊢ { preserves := a } = { preserves := b }
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesColimit K F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : PreservesColimit K F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
a b : {c : Cocone K} → IsColimit c → IsColimit (F.mapCocone c)
⊢ { preserves := a } = { preserves := b }
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (PreservesLimitsOfShape J F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ ∀ (a b : PreservesLimitsOfShape J F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : {K : J ⥤ C} → PreservesLimit K F
⊢ PreservesLimitsOfShape.mk = PreservesLimitsOfShape.mk
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (PreservesColimitsOfShape J F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ ∀ (a b : PreservesColimitsOfShape J F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : {K : J ⥤ C} → PreservesColimit K F
⊢ PreservesColimitsOfShape.mk = PreservesColimitsOfShape.mk
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → PreservesLimitsOfShape J F
⊢ PreservesLimitsOfSize.mk = PreservesLimitsOfSize.mk
[PROOFSTEP]
congr
[GOAL]
case allEq.mk.mk.e_preservesLimitsOfShape
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → PreservesLimitsOfShape J F
⊢ a = b
[PROOFSTEP]
funext
[GOAL]
case allEq.mk.mk.e_preservesLimitsOfShape.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → PreservesLimitsOfShape J F
x✝¹ : Type w
x✝ : Category.{w', w} x✝¹
⊢ a = b
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → PreservesColimitsOfShape J F
⊢ PreservesColimitsOfSize.mk = PreservesColimitsOfSize.mk
[PROOFSTEP]
congr
[GOAL]
case allEq.mk.mk.e_preservesColimitsOfShape
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → PreservesColimitsOfShape J F
⊢ a = b
[PROOFSTEP]
funext
[GOAL]
case allEq.mk.mk.e_preservesColimitsOfShape.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → PreservesColimitsOfShape J F
x✝¹ : Type w
x✝ : Category.{w', w} x✝¹
⊢ a = b
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cone K
h : IsLimit c
⊢ ∀ (s : Cone (K ⋙ 𝟭 C)) (j : J),
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫
        NatTrans.app ((𝟭 C).mapCone c).π j =
      NatTrans.app s.π j
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cone (Functor.mk toPrefunctor✝)
h : IsLimit c
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (j : J),
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫
        NatTrans.app ((𝟭 C).mapCone c).π j =
      NatTrans.app s.π j
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit { pt := pt✝, π := NatTrans.mk app✝ }
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (j : J),
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫
        NatTrans.app ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ }).π j =
      NatTrans.app s.π j
[PROOFSTEP]
intro s j
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit { pt := pt✝, π := NatTrans.mk app✝ }
s : Cone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)
j : J
⊢ (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫
      NatTrans.app ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ }).π j =
    NatTrans.app s.π j
[PROOFSTEP]
cases s
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝¹).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝¹).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit { pt := pt✝¹, π := NatTrans.mk app✝ }
j : J
pt✝ : C
π✝ : (Functor.const J).obj pt✝ ⟶ Functor.mk toPrefunctor✝ ⋙ 𝟭 C
⊢ (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) { pt := pt✝, π := π✝ } ≫
      NatTrans.app ((𝟭 C).mapCone { pt := pt✝¹, π := NatTrans.mk app✝ }).π j =
    NatTrans.app { pt := pt✝, π := π✝ }.π j
[PROOFSTEP]
exact h.fac _ j
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cone K
h : IsLimit c
⊢ ∀ (s : Cone (K ⋙ 𝟭 C)) (m : s.pt ⟶ ((𝟭 C).mapCone c).pt),
    (∀ (j : J), m ≫ NatTrans.app ((𝟭 C).mapCone c).π j = NatTrans.app s.π j) →
      m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cone (Functor.mk toPrefunctor✝)
h : IsLimit c
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (m : s.pt ⟶ ((𝟭 C).mapCone c).pt),
    (∀ (j : J), m ≫ NatTrans.app ((𝟭 C).mapCone c).π j = NatTrans.app s.π j) →
      m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit { pt := pt✝, π := NatTrans.mk app✝ }
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (m : s.pt ⟶ ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ }).pt),
    (∀ (j : J), m ≫ NatTrans.app ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ }).π j = NatTrans.app s.π j) →
      m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
intro s m w
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit { pt := pt✝, π := NatTrans.mk app✝ }
s : Cone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)
m : s.pt ⟶ ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ }).pt
w : ∀ (j : J), m ≫ NatTrans.app ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ }).π j = NatTrans.app s.π j
⊢ m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
rcases s with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝¹ : (X : J) → ((Functor.const J).obj pt✝¹).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝¹).map f ≫ app✝¹ Y = app✝¹ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit { pt := pt✝¹, π := NatTrans.mk app✝¹ }
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝ ⋙ 𝟭 C).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝ ⋙ 𝟭 C).map f
m : { pt := pt✝, π := NatTrans.mk app✝ }.pt ⟶ ((𝟭 C).mapCone { pt := pt✝¹, π := NatTrans.mk app✝¹ }).pt
w :
  ∀ (j : J),
    m ≫ NatTrans.app ((𝟭 C).mapCone { pt := pt✝¹, π := NatTrans.mk app✝¹ }).π j =
      NatTrans.app { pt := pt✝, π := NatTrans.mk app✝ }.π j
⊢ m =
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j })
      { pt := pt✝, π := NatTrans.mk app✝ }
[PROOFSTEP]
exact h.uniq _ m w
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cocone K
h : IsColimit c
⊢ ∀ (s : Cocone (K ⋙ 𝟭 C)) (j : J),
    NatTrans.app ((𝟭 C).mapCocone c).ι j ≫
        (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
      NatTrans.app s.ι j
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cocone (Functor.mk toPrefunctor✝)
h : IsColimit c
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (j : J),
    NatTrans.app ((𝟭 C).mapCocone c).ι j ≫
        (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
      NatTrans.app s.ι j
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := NatTrans.mk app✝ }
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (j : J),
    NatTrans.app ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ }).ι j ≫
        (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
      NatTrans.app s.ι j
[PROOFSTEP]
intro s j
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := NatTrans.mk app✝ }
s : Cocone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)
j : J
⊢ NatTrans.app ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ }).ι j ≫
      (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
    NatTrans.app s.ι j
[PROOFSTEP]
cases s
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit { pt := pt✝¹, ι := NatTrans.mk app✝ }
j : J
pt✝ : C
ι✝ : Functor.mk toPrefunctor✝ ⋙ 𝟭 C ⟶ (Functor.const J).obj pt✝
⊢ NatTrans.app ((𝟭 C).mapCocone { pt := pt✝¹, ι := NatTrans.mk app✝ }).ι j ≫
      (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) { pt := pt✝, ι := ι✝ } =
    NatTrans.app { pt := pt✝, ι := ι✝ }.ι j
[PROOFSTEP]
exact h.fac _ j
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cocone K
h : IsColimit c
⊢ ∀ (s : Cocone (K ⋙ 𝟭 C)) (m : ((𝟭 C).mapCocone c).pt ⟶ s.pt),
    (∀ (j : J), NatTrans.app ((𝟭 C).mapCocone c).ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cocone (Functor.mk toPrefunctor✝)
h : IsColimit c
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (m : ((𝟭 C).mapCocone c).pt ⟶ s.pt),
    (∀ (j : J), NatTrans.app ((𝟭 C).mapCocone c).ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := NatTrans.mk app✝ }
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C))
    (m : ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ }).pt ⟶ s.pt),
    (∀ (j : J), NatTrans.app ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ }).ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
intro s m w
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := NatTrans.mk app✝ }
s : Cocone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)
m : ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ }).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ }).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
rcases s with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝¹ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝¹ Y = app✝¹ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit { pt := pt✝¹, ι := NatTrans.mk app✝¹ }
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝ ⋙ 𝟭 C).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝ ⋙ 𝟭 C).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
m : ((𝟭 C).mapCocone { pt := pt✝¹, ι := NatTrans.mk app✝¹ }).pt ⟶ { pt := pt✝, ι := NatTrans.mk app✝ }.pt
w :
  ∀ (j : J),
    NatTrans.app ((𝟭 C).mapCocone { pt := pt✝¹, ι := NatTrans.mk app✝¹ }).ι j ≫ m =
      NatTrans.app { pt := pt✝, ι := NatTrans.mk app✝ }.ι j
⊢ m =
    (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j })
      { pt := pt✝, ι := NatTrans.mk app✝ }
[PROOFSTEP]
exact h.uniq _ m w
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
apply IsLimit.postcomposeInvEquiv (isoWhiskerRight h F : _) _ _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
⊢ IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c))
[PROOFSTEP]
have := (IsLimit.postcomposeInvEquiv h c).symm t
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : (fun x => IsLimit ((Cones.postcompose h.inv).obj c)) t
⊢ IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c))
[PROOFSTEP]
apply IsLimit.ofIsoLimit (isLimitOfPreserves F this)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : (fun x => IsLimit ((Cones.postcompose h.inv).obj c)) t
⊢ F.mapCone ((Cones.postcompose h.inv).obj c) ≅ (Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c)
[PROOFSTEP]
refine' Cones.ext (Iso.refl _)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
let equ := e.invFunIdAssoc (K ⋙ F)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
have := (isLimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsLimit (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c)))
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
apply ((IsLimit.postcomposeHomEquiv equ _).symm this).ofIsoLimit
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsLimit (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c)))
⊢ (Cones.postcompose equ.hom).obj (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c))) ≅
    F.mapCone c
[PROOFSTEP]
refine' Cones.ext (Iso.refl _) fun j => _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsLimit (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c)))
j : J'
⊢ NatTrans.app
      ((Cones.postcompose equ.hom).obj
          (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c)))).π
      j =
    (Iso.refl
          ((Cones.postcompose equ.hom).obj
              (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c)))).pt).hom ≫
      NatTrans.app (F.mapCone c).π j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsLimit (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c)))
j : J'
⊢ F.map (NatTrans.app c.π (e.functor.obj (e.inverse.obj j))) ≫
      NatTrans.app (Equivalence.invFunIdAssoc e (K ⋙ F)).hom j =
    𝟙 (F.obj c.pt) ≫ F.map (NatTrans.app c.π j)
[PROOFSTEP]
simp [← Functor.map_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
apply IsColimit.precomposeHomEquiv (isoWhiskerRight h F : _) _ _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
⊢ IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c))
[PROOFSTEP]
have := (IsColimit.precomposeHomEquiv h c).symm t
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : (fun x => IsColimit ((Cocones.precompose h.hom).obj c)) t
⊢ IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c))
[PROOFSTEP]
apply IsColimit.ofIsoColimit (isColimitOfPreserves F this)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : (fun x => IsColimit ((Cocones.precompose h.hom).obj c)) t
⊢ F.mapCocone ((Cocones.precompose h.hom).obj c) ≅ (Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c)
[PROOFSTEP]
refine' Cocones.ext (Iso.refl _)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
let equ := e.invFunIdAssoc (K ⋙ F)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
have := (isColimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsColimit (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
apply ((IsColimit.precomposeInvEquiv equ _).symm this).ofIsoColimit
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsColimit (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ (Cocones.precompose equ.inv).obj
      (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c))) ≅
    F.mapCocone c
[PROOFSTEP]
refine' Cocones.ext (Iso.refl _) fun j => _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsColimit (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c)))
j : J'
⊢ NatTrans.app
        ((Cocones.precompose equ.inv).obj
            (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c)))).ι
        j ≫
      (Iso.refl
          ((Cocones.precompose equ.inv).obj
              (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c)))).pt).hom =
    NatTrans.app (F.mapCocone c).ι j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsColimit (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c)))
j : J'
⊢ (NatTrans.app (Equivalence.invFunIdAssoc e (K ⋙ F)).inv j ≫
        F.map (NatTrans.app c.ι (e.functor.obj (e.inverse.obj j)))) ≫
      𝟙 (F.obj c.pt) =
    F.map (NatTrans.app c.ι j)
[PROOFSTEP]
simp [← Functor.map_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsLimit K F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : ReflectsLimit K F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
a b : {c : Cone K} → IsLimit (F.mapCone c) → IsLimit c
⊢ { reflects := a } = { reflects := b }
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsColimit K F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : ReflectsColimit K F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
a b : {c : Cocone K} → IsColimit (F.mapCocone c) → IsColimit c
⊢ { reflects := a } = { reflects := b }
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (ReflectsLimitsOfShape J F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ ∀ (a b : ReflectsLimitsOfShape J F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : {K : J ⥤ C} → ReflectsLimit K F
⊢ ReflectsLimitsOfShape.mk = ReflectsLimitsOfShape.mk
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (ReflectsColimitsOfShape J F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ ∀ (a b : ReflectsColimitsOfShape J F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : {K : J ⥤ C} → ReflectsColimit K F
⊢ ReflectsColimitsOfShape.mk = ReflectsColimitsOfShape.mk
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → ReflectsLimitsOfShape J F
⊢ ReflectsLimitsOfSize.mk = ReflectsLimitsOfSize.mk
[PROOFSTEP]
congr
[GOAL]
case allEq.mk.mk.e_reflectsLimitsOfShape
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → ReflectsLimitsOfShape J F
⊢ a = b
[PROOFSTEP]
funext
[GOAL]
case allEq.mk.mk.e_reflectsLimitsOfShape.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → ReflectsLimitsOfShape J F
x✝¹ : Type w
x✝ : Category.{w', w} x✝¹
⊢ a = b
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → ReflectsColimitsOfShape J F
⊢ ReflectsColimitsOfSize.mk = ReflectsColimitsOfSize.mk
[PROOFSTEP]
congr
[GOAL]
case allEq.mk.mk.e_reflectsColimitsOfShape
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → ReflectsColimitsOfShape J F
⊢ a = b
[PROOFSTEP]
funext
[GOAL]
case allEq.mk.mk.e_reflectsColimitsOfShape.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → ReflectsColimitsOfShape J F
x✝¹ : Type w
x✝ : Category.{w', w} x✝¹
⊢ a = b
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cone K
h : IsLimit ((𝟭 C).mapCone c)
⊢ ∀ (s : Cone K) (j : J),
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫ NatTrans.app c.π j =
      NatTrans.app s.π j
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cone (Functor.mk toPrefunctor✝)
h : IsLimit ((𝟭 C).mapCone c)
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝)) (j : J),
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫ NatTrans.app c.π j =
      NatTrans.app s.π j
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ })
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝)) (j : J),
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫
        NatTrans.app { pt := pt✝, π := NatTrans.mk app✝ }.π j =
      NatTrans.app s.π j
[PROOFSTEP]
intro s j
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ })
s : Cone (Functor.mk toPrefunctor✝)
j : J
⊢ (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫
      NatTrans.app { pt := pt✝, π := NatTrans.mk app✝ }.π j =
    NatTrans.app s.π j
[PROOFSTEP]
cases s
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝¹).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝¹).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝¹, π := NatTrans.mk app✝ })
j : J
pt✝ : C
π✝ : (Functor.const J).obj pt✝ ⟶ Functor.mk toPrefunctor✝
⊢ (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) { pt := pt✝, π := π✝ } ≫
      NatTrans.app { pt := pt✝¹, π := NatTrans.mk app✝ }.π j =
    NatTrans.app { pt := pt✝, π := π✝ }.π j
[PROOFSTEP]
exact h.fac _ j
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cone K
h : IsLimit ((𝟭 C).mapCone c)
⊢ ∀ (s : Cone K) (m : s.pt ⟶ c.pt),
    (∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j) →
      m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cone (Functor.mk toPrefunctor✝)
h : IsLimit ((𝟭 C).mapCone c)
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝)) (m : s.pt ⟶ c.pt),
    (∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j) →
      m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ })
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝)) (m : s.pt ⟶ { pt := pt✝, π := NatTrans.mk app✝ }.pt),
    (∀ (j : J), m ≫ NatTrans.app { pt := pt✝, π := NatTrans.mk app✝ }.π j = NatTrans.app s.π j) →
      m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
intro s m w
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ })
s : Cone (Functor.mk toPrefunctor✝)
m : s.pt ⟶ { pt := pt✝, π := NatTrans.mk app✝ }.pt
w : ∀ (j : J), m ≫ NatTrans.app { pt := pt✝, π := NatTrans.mk app✝ }.π j = NatTrans.app s.π j
⊢ m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
rcases s with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝¹ : (X : J) → ((Functor.const J).obj pt✝¹).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝¹).map f ≫ app✝¹ Y = app✝¹ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝¹, π := NatTrans.mk app✝¹ })
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
m : { pt := pt✝, π := NatTrans.mk app✝ }.pt ⟶ { pt := pt✝¹, π := NatTrans.mk app✝¹ }.pt
w :
  ∀ (j : J),
    m ≫ NatTrans.app { pt := pt✝¹, π := NatTrans.mk app✝¹ }.π j = NatTrans.app { pt := pt✝, π := NatTrans.mk app✝ }.π j
⊢ m =
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j })
      { pt := pt✝, π := NatTrans.mk app✝ }
[PROOFSTEP]
exact h.uniq _ m w
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
h : IsColimit ((𝟭 C).mapCocone c)
⊢ ∀ (s : Cocone K) (j : J),
    NatTrans.app c.ι j ≫ (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
      NatTrans.app s.ι j
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cocone (Functor.mk toPrefunctor✝)
h : IsColimit ((𝟭 C).mapCocone c)
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝)) (j : J),
    NatTrans.app c.ι j ≫ (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
      NatTrans.app s.ι j
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ })
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝)) (j : J),
    NatTrans.app { pt := pt✝, ι := NatTrans.mk app✝ }.ι j ≫
        (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
      NatTrans.app s.ι j
[PROOFSTEP]
intro s j
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ })
s : Cocone (Functor.mk toPrefunctor✝)
j : J
⊢ NatTrans.app { pt := pt✝, ι := NatTrans.mk app✝ }.ι j ≫
      (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
    NatTrans.app s.ι j
[PROOFSTEP]
cases s
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝¹, ι := NatTrans.mk app✝ })
j : J
pt✝ : C
ι✝ : Functor.mk toPrefunctor✝ ⟶ (Functor.const J).obj pt✝
⊢ NatTrans.app { pt := pt✝¹, ι := NatTrans.mk app✝ }.ι j ≫
      (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) { pt := pt✝, ι := ι✝ } =
    NatTrans.app { pt := pt✝, ι := ι✝ }.ι j
[PROOFSTEP]
exact h.fac _ j
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
h : IsColimit ((𝟭 C).mapCocone c)
⊢ ∀ (s : Cocone K) (m : c.pt ⟶ s.pt),
    (∀ (j : J), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cocone (Functor.mk toPrefunctor✝)
h : IsColimit ((𝟭 C).mapCocone c)
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝)) (m : c.pt ⟶ s.pt),
    (∀ (j : J), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ })
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝)) (m : { pt := pt✝, ι := NatTrans.mk app✝ }.pt ⟶ s.pt),
    (∀ (j : J), NatTrans.app { pt := pt✝, ι := NatTrans.mk app✝ }.ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
intro s m w
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ })
s : Cocone (Functor.mk toPrefunctor✝)
m : { pt := pt✝, ι := NatTrans.mk app✝ }.pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app { pt := pt✝, ι := NatTrans.mk app✝ }.ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
rcases s with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝¹ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝¹ Y = app✝¹ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝¹, ι := NatTrans.mk app✝¹ })
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
m : { pt := pt✝¹, ι := NatTrans.mk app✝¹ }.pt ⟶ { pt := pt✝, ι := NatTrans.mk app✝ }.pt
w :
  ∀ (j : J),
    NatTrans.app { pt := pt✝¹, ι := NatTrans.mk app✝¹ }.ι j ≫ m = NatTrans.app { pt := pt✝, ι := NatTrans.mk app✝ }.ι j
⊢ m =
    (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j })
      { pt := pt✝, ι := NatTrans.mk app✝ }
[PROOFSTEP]
exact h.uniq _ m w
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesLimit K (F ⋙ G)
inst✝ : ReflectsLimit (K ⋙ F) G
c✝ : Cone K
h : IsLimit c✝
⊢ IsLimit (F.mapCone c✝)
[PROOFSTEP]
apply isLimitOfReflects G
[GOAL]
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesLimit K (F ⋙ G)
inst✝ : ReflectsLimit (K ⋙ F) G
c✝ : Cone K
h : IsLimit c✝
⊢ IsLimit (G.mapCone (F.mapCone c✝))
[PROOFSTEP]
apply isLimitOfPreserves (F ⋙ G) h
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ IsLimit c
[PROOFSTEP]
apply IsLimit.postcomposeInvEquiv h c (isLimitOfReflects F _)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ IsLimit (F.mapCone ((Cones.postcompose h.inv).obj c))
[PROOFSTEP]
apply ((IsLimit.postcomposeInvEquiv (isoWhiskerRight h F : _) _).symm t).ofIsoLimit _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ (Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c) ≅ F.mapCone ((Cones.postcompose h.inv).obj c)
[PROOFSTEP]
exact Cones.ext (Iso.refl _)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit c
[PROOFSTEP]
apply IsLimit.ofWhiskerEquivalence e
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (Cone.whisker e.functor c)
[PROOFSTEP]
apply isLimitOfReflects F
[GOAL]
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (F.mapCone (Cone.whisker e.functor c))
[PROOFSTEP]
apply IsLimit.ofIsoLimit _ (Functor.mapConeWhisker _).symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (Cone.whisker e.functor (F.mapCone c))
[PROOFSTEP]
exact IsLimit.whiskerEquivalence t _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsLimit c
[PROOFSTEP]
suffices IsIso (IsLimit.lift (limit.isLimit F) c) from by apply IsLimit.ofPointIso (limit.isLimit F)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso (IsLimit.lift (limit.isLimit F) c)
⊢ IsLimit c
[PROOFSTEP]
apply IsLimit.ofPointIso (limit.isLimit F)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso (IsLimit.lift (limit.isLimit F) c)
[PROOFSTEP]
change IsIso ((Cones.forget _).map ((limit.isLimit F).liftConeMorphism c))
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso ((Cones.forget F).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
[PROOFSTEP]
suffices IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c) from by apply (Cones.forget F).map_isIso _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c)
⊢ IsIso ((Cones.forget F).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
[PROOFSTEP]
apply (Cones.forget F).map_isIso _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c)
[PROOFSTEP]
suffices IsIso (Prefunctor.map (Cones.functoriality F G).toPrefunctor (IsLimit.liftConeMorphism (limit.isLimit F) c))
  from by apply isIso_of_reflects_iso _ (Cones.functoriality F G)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso ((Cones.functoriality F G).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
⊢ IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c)
[PROOFSTEP]
apply isIso_of_reflects_iso _ (Cones.functoriality F G)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso ((Cones.functoriality F G).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
[PROOFSTEP]
refine' t.hom_isIso (isLimitOfPreserves G (limit.isLimit F)) _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesColimit K (F ⋙ G)
inst✝ : ReflectsColimit (K ⋙ F) G
c : Cocone K
h : IsColimit c
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
apply isColimitOfReflects G
[GOAL]
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesColimit K (F ⋙ G)
inst✝ : ReflectsColimit (K ⋙ F) G
c : Cocone K
h : IsColimit c
⊢ IsColimit (G.mapCocone (F.mapCocone c))
[PROOFSTEP]
apply isColimitOfPreserves (F ⋙ G) h
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ IsColimit c
[PROOFSTEP]
apply IsColimit.precomposeHomEquiv h c (isColimitOfReflects F _)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ IsColimit (F.mapCocone ((Cocones.precompose h.hom).obj c))
[PROOFSTEP]
apply ((IsColimit.precomposeHomEquiv (isoWhiskerRight h F : _) _).symm t).ofIsoColimit _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ (Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c) ≅ F.mapCocone ((Cocones.precompose h.hom).obj c)
[PROOFSTEP]
exact Cocones.ext (Iso.refl _)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit c
[PROOFSTEP]
apply IsColimit.ofWhiskerEquivalence e
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (Cocone.whisker e.functor c)
[PROOFSTEP]
apply isColimitOfReflects F
[GOAL]
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (F.mapCocone (Cocone.whisker e.functor c))
[PROOFSTEP]
apply IsColimit.ofIsoColimit _ (Functor.mapCoconeWhisker _).symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (Cocone.whisker e.functor (F.mapCocone c))
[PROOFSTEP]
exact IsColimit.whiskerEquivalence t _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsColimit c
[PROOFSTEP]
suffices IsIso (IsColimit.desc (colimit.isColimit F) c) from by apply IsColimit.ofPointIso (colimit.isColimit F)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso (IsColimit.desc (colimit.isColimit F) c)
⊢ IsColimit c
[PROOFSTEP]
apply IsColimit.ofPointIso (colimit.isColimit F)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso (IsColimit.desc (colimit.isColimit F) c)
[PROOFSTEP]
change IsIso ((Cocones.forget _).map ((colimit.isColimit F).descCoconeMorphism c))
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso ((Cocones.forget F).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
[PROOFSTEP]
suffices IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c) from by apply (Cocones.forget F).map_isIso _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c)
⊢ IsIso ((Cocones.forget F).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
[PROOFSTEP]
apply (Cocones.forget F).map_isIso _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c)
[PROOFSTEP]
suffices
  IsIso (Prefunctor.map (Cocones.functoriality F G).toPrefunctor (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
  from by apply isIso_of_reflects_iso _ (Cocones.functoriality F G)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso ((Cocones.functoriality F G).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
⊢ IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c)
[PROOFSTEP]
apply isIso_of_reflects_iso _ (Cocones.functoriality F G)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso ((Cocones.functoriality F G).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
[PROOFSTEP]
refine' (isColimitOfPreserves G (colimit.isColimit F)).hom_isIso t _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ ∀ (s : Cone K) (m : s ⟶ c),
    m = (Cones.functoriality K F).preimage (IsLimit.liftConeMorphism t ((Cones.functoriality K F).obj s))
[PROOFSTEP]
apply fun s m => (Cones.functoriality K F).map_injective _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ ∀ (s : Cone K) (m : s ⟶ c),
    (Cones.functoriality K F).map m =
      (Cones.functoriality K F).map
        ((Cones.functoriality K F).preimage (IsLimit.liftConeMorphism t ((Cones.functoriality K F).obj s)))
[PROOFSTEP]
intro s m
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
s : Cone K
m : s ⟶ c
⊢ (Cones.functoriality K F).map m =
    (Cones.functoriality K F).map
      ((Cones.functoriality K F).preimage (IsLimit.liftConeMorphism t ((Cones.functoriality K F).obj s)))
[PROOFSTEP]
rw [Functor.image_preimage]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
s : Cone K
m : s ⟶ c
⊢ (Cones.functoriality K F).map m = IsLimit.liftConeMorphism t ((Cones.functoriality K F).obj s)
[PROOFSTEP]
apply t.uniq_cone_morphism
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
⊢ ∀ (s : Cocone K) (m : c ⟶ s),
    m = (Cocones.functoriality K F).preimage (IsColimit.descCoconeMorphism t ((Cocones.functoriality K F).obj s))
[PROOFSTEP]
apply fun s m => (Cocones.functoriality K F).map_injective _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
⊢ ∀ (s : Cocone K) (m : c ⟶ s),
    (Cocones.functoriality K F).map m =
      (Cocones.functoriality K F).map
        ((Cocones.functoriality K F).preimage (IsColimit.descCoconeMorphism t ((Cocones.functoriality K F).obj s)))
[PROOFSTEP]
intro s m
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
s : Cocone K
m : c ⟶ s
⊢ (Cocones.functoriality K F).map m =
    (Cocones.functoriality K F).map
      ((Cocones.functoriality K F).preimage (IsColimit.descCoconeMorphism t ((Cocones.functoriality K F).obj s)))
[PROOFSTEP]
rw [Functor.image_preimage]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
s : Cocone K
m : c ⟶ s
⊢ (Cocones.functoriality K F).map m = IsColimit.descCoconeMorphism t ((Cocones.functoriality K F).obj s)
[PROOFSTEP]
apply t.uniq_cocone_morphism
