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