[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
⊢ IsLimit d
[PROOFSTEP]
let d' : Cone K := (h (F.mapCone d) hd).toLiftableCone.liftedCone
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
⊢ IsLimit d
[PROOFSTEP]
let i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).toLiftableCone.validLift
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
⊢ IsLimit d
[PROOFSTEP]
let hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
⊢ IsLimit d
[PROOFSTEP]
let f : d ⟶ d' := hd'.liftConeMorphism d
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := IsLimit.liftConeMorphism hd' d
⊢ IsLimit d
[PROOFSTEP]
have : (Cones.functoriality K F).map f = i.inv := (hd.ofIsoLimit i.symm).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✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := IsLimit.liftConeMorphism hd' d
this : (Cones.functoriality K F).map f = i.inv
⊢ IsLimit d
[PROOFSTEP]
haveI : IsIso ((Cones.functoriality K F).map f) := by
  rw [this]
  infer_instance
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := IsLimit.liftConeMorphism hd' d
this : (Cones.functoriality K F).map f = i.inv
⊢ IsIso ((Cones.functoriality K F).map f)
[PROOFSTEP]
rw [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 : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := IsLimit.liftConeMorphism hd' d
this : (Cones.functoriality K F).map f = i.inv
⊢ IsIso i.inv
[PROOFSTEP]
infer_instance
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := IsLimit.liftConeMorphism hd' d
this✝ : (Cones.functoriality K F).map f = i.inv
this : IsIso ((Cones.functoriality K F).map f)
⊢ IsLimit d
[PROOFSTEP]
haveI : IsIso f := isIso_of_reflects_iso f (Cones.functoriality 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✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := IsLimit.liftConeMorphism hd' d
this✝¹ : (Cones.functoriality K F).map f = i.inv
this✝ : IsIso ((Cones.functoriality K F).map f)
this : IsIso f
⊢ IsLimit d
[PROOFSTEP]
exact IsLimit.ofIsoLimit hd' (asIso f).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✝ K : J ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
l : Cone (K ⋙ F)
hl : IsLimit l
X : C
i : F.obj X ≅ l.pt
Y Z : J
f : Y ⟶ Z
⊢ F.map (((Functor.const J).obj X).map f ≫ (fun j => F.preimage (i.hom ≫ NatTrans.app l.π j)) Z) =
    F.map ((fun j => F.preimage (i.hom ≫ NatTrans.app l.π j)) Y ≫ K.map f)
[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✝ K : J ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
l : Cone (K ⋙ F)
hl : IsLimit l
X : C
i : F.obj X ≅ l.pt
Y Z : J
f : Y ⟶ Z
⊢ F.map (𝟙 X ≫ F.preimage (i.hom ≫ NatTrans.app l.π Z)) = F.map (F.preimage (i.hom ≫ NatTrans.app l.π Y) ≫ K.map f)
[PROOFSTEP]
simpa using (l.w f).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✝ K : J ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
l : Cone (K ⋙ F)
hl : IsLimit l
X : C
i : F.obj X ≅ l.pt
j : J
⊢ NatTrans.app (F.mapCone { pt := X, π := NatTrans.mk fun j => F.preimage (i.hom ≫ NatTrans.app l.π j) }).π j =
    i.hom ≫ NatTrans.app l.π j
[PROOFSTEP]
simp only [Functor.image_preimage, Functor.mapCone_π_app]
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
⊢ IsColimit d
[PROOFSTEP]
let d' : Cocone K := (h (F.mapCocone d) hd).toLiftableCocone.liftedCocone
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
⊢ IsColimit d
[PROOFSTEP]
let i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).toLiftableCocone.validLift
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
⊢ IsColimit d
[PROOFSTEP]
let hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
⊢ IsColimit d
[PROOFSTEP]
let f : d' ⟶ d := hd'.descCoconeMorphism d
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := IsColimit.descCoconeMorphism hd' d
⊢ IsColimit d
[PROOFSTEP]
have : (Cocones.functoriality K F).map f = i.hom := (hd.ofIsoColimit i.symm).uniq_cocone_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✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := IsColimit.descCoconeMorphism hd' d
this : (Cocones.functoriality K F).map f = i.hom
⊢ IsColimit d
[PROOFSTEP]
haveI : IsIso ((Cocones.functoriality K F).map f) := by
  rw [this]
  infer_instance
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := IsColimit.descCoconeMorphism hd' d
this : (Cocones.functoriality K F).map f = i.hom
⊢ IsIso ((Cocones.functoriality K F).map f)
[PROOFSTEP]
rw [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 : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := IsColimit.descCoconeMorphism hd' d
this : (Cocones.functoriality K F).map f = i.hom
⊢ IsIso i.hom
[PROOFSTEP]
infer_instance
[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
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := IsColimit.descCoconeMorphism hd' d
this✝ : (Cocones.functoriality K F).map f = i.hom
this : IsIso ((Cocones.functoriality K F).map f)
⊢ IsColimit d
[PROOFSTEP]
haveI := isIso_of_reflects_iso f (Cocones.functoriality 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✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := IsColimit.descCoconeMorphism hd' d
this✝¹ : (Cocones.functoriality K F).map f = i.hom
this✝ : IsIso ((Cocones.functoriality K F).map f)
this : IsIso f
⊢ IsColimit d
[PROOFSTEP]
exact IsColimit.ofIsoColimit hd' (asIso 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 : J ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
l : Cocone (K ⋙ F)
hl : IsColimit l
X : C
i : F.obj X ≅ l.pt
Y Z : J
f : Y ⟶ Z
⊢ F.map (K.map f ≫ (fun j => F.preimage (NatTrans.app l.ι j ≫ i.inv)) Z) =
    F.map ((fun j => F.preimage (NatTrans.app l.ι j ≫ i.inv)) Y ≫ ((Functor.const J).obj X).map f)
[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✝ K : J ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
l : Cocone (K ⋙ F)
hl : IsColimit l
X : C
i : F.obj X ≅ l.pt
Y Z : J
f : Y ⟶ Z
⊢ F.map (K.map f ≫ F.preimage (NatTrans.app l.ι Z ≫ i.inv)) = F.map (F.preimage (NatTrans.app l.ι Y ≫ i.inv) ≫ 𝟙 X)
[PROOFSTEP]
simpa [← cancel_mono i.hom] using l.w 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 : J ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
l : Cocone (K ⋙ F)
hl : IsColimit l
X : C
i : F.obj X ≅ l.pt
j : J
⊢ NatTrans.app (F.mapCocone { pt := X, ι := NatTrans.mk fun j => F.preimage (NatTrans.app l.ι j ≫ i.inv) }).ι j ≫
      i.hom =
    NatTrans.app l.ι j
[PROOFSTEP]
simp
[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✝ : CreatesLimit K₁ F
src✝ : ReflectsLimit K₂ F := reflectsLimitOfIsoDiagram F h
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : (fun x => IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj c)) t :=
  ↑(IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ NatTrans.app
      ((Cones.postcompose (isoWhiskerRight h F).hom).obj ((Cones.postcompose (isoWhiskerRight h F).inv).obj c)).π j =
    (Iso.refl
          ((Cones.postcompose (isoWhiskerRight h F).hom).obj
              ((Cones.postcompose (isoWhiskerRight h F).inv).obj c)).pt).hom ≫
      NatTrans.app 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 K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesLimit K₁ F
src✝ : ReflectsLimit K₂ F := reflectsLimitOfIsoDiagram F h
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : (fun x => IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj c)) t :=
  ↑(IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ (NatTrans.app c.π j ≫ F.map (NatTrans.app h.inv j)) ≫ F.map (NatTrans.app h.hom j) = 𝟙 c.pt ≫ NatTrans.app c.π j
[PROOFSTEP]
rw [Category.assoc, ← F.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✝ : CreatesLimit K₁ F
src✝ : ReflectsLimit K₂ F := reflectsLimitOfIsoDiagram F h
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : (fun x => IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj c)) t :=
  ↑(IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ NatTrans.app c.π j ≫ F.map (NatTrans.app h.inv j ≫ NatTrans.app h.hom j) = 𝟙 c.pt ≫ NatTrans.app c.π j
[PROOFSTEP]
simp
[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 G : C ⥤ D
h : F ≅ G
inst✝ : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
⊢ G.mapCone (liftLimit (↑(IsLimit.postcomposeInvEquiv (isoWhiskerLeft K h) c).symm t)) ≅ c
[PROOFSTEP]
refine' (IsLimit.mapConeEquiv h _).uniqueUpToIso 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 G : C ⥤ D
h : F ≅ G
inst✝ : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
⊢ IsLimit (F.mapCone (liftLimit (↑(IsLimit.postcomposeInvEquiv (isoWhiskerLeft K h) c).symm t)))
[PROOFSTEP]
apply IsLimit.ofIsoLimit _ (liftedLimitMapsToOriginal _).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
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
⊢ IsLimit ((Cones.postcompose (isoWhiskerLeft K h).inv).obj c)
[PROOFSTEP]
apply (IsLimit.postcomposeInvEquiv _ _).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✝ : CreatesColimit K₁ F
src✝ : ReflectsColimit K₂ F := reflectsColimitOfIsoDiagram F h
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : (fun x => IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj c)) t :=
  ↑(IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ NatTrans.app
        ((Cocones.precompose (isoWhiskerRight h F).inv).obj ((Cocones.precompose (isoWhiskerRight h F).hom).obj c)).ι
        j ≫
      (Iso.refl
          ((Cocones.precompose (isoWhiskerRight h F).inv).obj
              ((Cocones.precompose (isoWhiskerRight h F).hom).obj c)).pt).hom =
    NatTrans.app 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 K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesColimit K₁ F
src✝ : ReflectsColimit K₂ F := reflectsColimitOfIsoDiagram F h
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : (fun x => IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj c)) t :=
  ↑(IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ (F.map (NatTrans.app h.inv j) ≫ F.map (NatTrans.app h.hom j) ≫ NatTrans.app c.ι j) ≫ 𝟙 c.pt = NatTrans.app c.ι j
[PROOFSTEP]
rw [← F.map_comp_assoc]
[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✝ : CreatesColimit K₁ F
src✝ : ReflectsColimit K₂ F := reflectsColimitOfIsoDiagram F h
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : (fun x => IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj c)) t :=
  ↑(IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ (F.map (NatTrans.app h.inv j ≫ NatTrans.app h.hom j) ≫ NatTrans.app c.ι j) ≫ 𝟙 c.pt = NatTrans.app c.ι j
[PROOFSTEP]
simp
[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 G : C ⥤ D
h : F ≅ G
inst✝ : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ G.mapCocone (liftColimit (↑(IsColimit.precomposeHomEquiv (isoWhiskerLeft K h) c).symm t)) ≅ c
[PROOFSTEP]
refine' (IsColimit.mapCoconeEquiv h _).uniqueUpToIso 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 G : C ⥤ D
h : F ≅ G
inst✝ : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ IsColimit (F.mapCocone (liftColimit (↑(IsColimit.precomposeHomEquiv (isoWhiskerLeft K h) c).symm t)))
[PROOFSTEP]
apply IsColimit.ofIsoColimit _ (liftedColimitMapsToOriginal _).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
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ IsColimit ((Cocones.precompose (isoWhiskerLeft K h).hom).obj c)
[PROOFSTEP]
apply (IsColimit.precomposeHomEquiv _ _).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 : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : CreatesLimit K F
inst✝ : CreatesLimit (K ⋙ F) G
c : Cone (K ⋙ F ⋙ G)
t : IsLimit c
⊢ LiftableCone K (F ⋙ G) c
[PROOFSTEP]
let c' : Cone ((K ⋙ F) ⋙ G) := 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
inst✝¹ : CreatesLimit K F
inst✝ : CreatesLimit (K ⋙ F) G
c : Cone (K ⋙ F ⋙ G)
t : IsLimit c
c' : Cone ((K ⋙ F) ⋙ G) := c
⊢ LiftableCone K (F ⋙ G) c
[PROOFSTEP]
let t' : IsLimit c' := 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
inst✝¹ : CreatesLimit K F
inst✝ : CreatesLimit (K ⋙ F) G
c : Cone (K ⋙ F ⋙ G)
t : IsLimit c
c' : Cone ((K ⋙ F) ⋙ G) := c
t' : IsLimit c' := t
⊢ LiftableCone K (F ⋙ G) c
[PROOFSTEP]
exact
  { liftedCone := liftLimit (liftedLimitIsLimit t')
    validLift :=
      (Cones.functoriality (K ⋙ F) G).mapIso (liftedLimitMapsToOriginal (liftedLimitIsLimit t')) ≪≫
        liftedLimitMapsToOriginal t' }
