-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
/--
Pull back a `HasExactLimitsOfShape J` along a functor which preserves and reflects finite colimits
and preserves limits of shape `J`
-/
lemma HasExactLimitsOfShape.domain_of_functor {D : Type*} (J : Type*) [Category D] [Category J]
    [HasLimitsOfShape J C] [HasLimitsOfShape J D] [HasExactLimitsOfShape J D]
    (F : C ⥤ D) [PreservesFiniteColimits F] [ReflectsFiniteColimits F] [HasFiniteColimits C]
    [PreservesLimitsOfShape J F] : HasExactLimitsOfShape J C where
  preservesFiniteColimits := { preservesFiniteColimits I := { preservesColimit {G} := {
    preserves {c} hc

Proof state:
case val
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
⊢ IsColimit (lim.mapCocone c)

Tactic:
apply isColimitOfReflects F

Result:
case val.t
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
⊢ IsColimit (F.mapCocone (lim.mapCocone c))

Proof state:
case val.t
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
⊢ IsColimit (F.mapCocone (lim.mapCocone c))

Tactic:
refine (IsColimit.equivOfNatIsoOfIso (isoWhiskerLeft G (preservesLimitNatIso F).symm)
  ((_ ⋙ lim).mapCocone c) _ ?_) (isColimitOfPreserves _ hc)

Result:
case val.t
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
⊢ (Cocones.precompose (isoWhiskerLeft G (preservesLimitNatIso F).symm).inv).obj
      (((whiskeringRight J C D).obj F ⋙ lim).mapCocone c) ≅
    F.mapCocone (lim.mapCocone c)

Proof state:
case val.t
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
i : I
⊢ limMap (whiskerRight (c.ι.app i) F) ≫ (preservesLimitIso F c.pt).inv =
    (preservesLimitIso F (G.obj i)).inv ≫ F.map (limMap (c.ι.app i))

Tactic:
exact (preservesLimitNatIso F).inv.naturality _

Result:
no goals

Proof state:
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
⊢ Nonempty (IsColimit (lim.mapCocone c))

Tactic:
constructor

Result:
case val
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
⊢ IsColimit (lim.mapCocone c)

Proof state:
case val.t
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
i : I
⊢ (preservesLimitIso F (G.obj i)).hom ≫ limMap (whiskerRight (c.ι.app i) F) ≫ (preservesLimitIso F c.pt).inv =
    F.map (limMap (c.ι.app i))

Tactic:
rw [← Iso.eq_inv_comp]

Result:
case val.t
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
i : I
⊢ limMap (whiskerRight (c.ι.app i) F) ≫ (preservesLimitIso F c.pt).inv =
    (preservesLimitIso F (G.obj i)).inv ≫ F.map (limMap (c.ι.app i))

Proof state:
case val.t
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
i : I
⊢ ((Cocones.precompose (isoWhiskerLeft G (preservesLimitNatIso F).symm).inv).obj
              (((whiskeringRight J C D).obj F ⋙ lim).mapCocone c)).ι.app
        i ≫
      ((preservesLimitNatIso F).symm.app c.pt).hom =
    (F.mapCocone (lim.mapCocone c)).ι.app i

Tactic:
simp only [Functor.comp_obj, lim_obj, Functor.mapCocone_pt, isoWhiskerLeft_inv, Iso.symm_inv,
  Cocones.precompose_obj_pt, whiskeringRight_obj_obj, Functor.const_obj_obj,
  Cocones.precompose_obj_ι, NatTrans.comp_app, whiskerLeft_app, preservesLimitNatIso_hom_app,
  Functor.mapCocone_ι_app, Functor.comp_map, whiskeringRight_obj_map, lim_map, Iso.app_hom,
  Iso.symm_hom, preservesLimitNatIso_inv_app, Category.assoc]

Result:
case val.t
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
i : I
⊢ (preservesLimitIso F (G.obj i)).hom ≫ limMap (whiskerRight (c.ι.app i) F) ≫ (preservesLimitIso F c.pt).inv =
    F.map (limMap (c.ι.app i))