-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
/--
Pull back a `HasExactColimitsOfShape J` along a functor which preserves and reflects finite limits
and preserves colimits of shape `J`
-/
lemma HasExactColimitsOfShape.domain_of_functor {D : Type*} (J : Type*) [Category J] [Category D]
    [HasColimitsOfShape J C] [HasColimitsOfShape J D] [HasExactColimitsOfShape J D]
    (F : C ⥤ D) [PreservesFiniteLimits F] [ReflectsFiniteLimits F] [HasFiniteLimits C]
    [PreservesColimitsOfShape J F] : HasExactColimitsOfShape J C where
  preservesFiniteLimits := { preservesFiniteLimits I := { preservesLimit {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_2} J
inst✝⁹ : Category.{u_4, u_1} D
inst✝⁸ : HasColimitsOfShape J C
inst✝⁷ : HasColimitsOfShape J D
inst✝⁶ : HasExactColimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : ReflectsFiniteLimits F
inst✝³ : HasFiniteLimits C
inst✝² : PreservesColimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cone G
hc : IsLimit c
⊢ IsLimit (colim.mapCone c)

Tactic:
apply isLimitOfReflects 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_2} J
inst✝⁹ : Category.{u_4, u_1} D
inst✝⁸ : HasColimitsOfShape J C
inst✝⁷ : HasColimitsOfShape J D
inst✝⁶ : HasExactColimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : ReflectsFiniteLimits F
inst✝³ : HasFiniteLimits C
inst✝² : PreservesColimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cone G
hc : IsLimit c
⊢ IsLimit (F.mapCone (colim.mapCone 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_2} J
inst✝⁹ : Category.{u_4, u_1} D
inst✝⁸ : HasColimitsOfShape J C
inst✝⁷ : HasColimitsOfShape J D
inst✝⁶ : HasExactColimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : ReflectsFiniteLimits F
inst✝³ : HasFiniteLimits C
inst✝² : PreservesColimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cone G
hc : IsLimit c
⊢ (Cones.postcompose (isoWhiskerLeft G (preservesColimitNatIso F).symm).hom).obj
      (((whiskeringRight J C D).obj F ⋙ colim).mapCone c) ≅
    F.mapCone (colim.mapCone c)

Tactic:
exact Cones.ext ((preservesColimitNatIso F).symm.app _)
  fun i ↦ (preservesColimitNatIso F).inv.naturality _

Result:
no goals

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_2} J
inst✝⁹ : Category.{u_4, u_1} D
inst✝⁸ : HasColimitsOfShape J C
inst✝⁷ : HasColimitsOfShape J D
inst✝⁶ : HasExactColimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : ReflectsFiniteLimits F
inst✝³ : HasFiniteLimits C
inst✝² : PreservesColimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cone G
hc : IsLimit c
⊢ IsLimit (F.mapCone (colim.mapCone c))

Tactic:
refine (IsLimit.equivOfNatIsoOfIso (isoWhiskerLeft G (preservesColimitNatIso F).symm)
  ((_ ⋙ colim).mapCone c) _ ?_) (isLimitOfPreserves _ 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_2} J
inst✝⁹ : Category.{u_4, u_1} D
inst✝⁸ : HasColimitsOfShape J C
inst✝⁷ : HasColimitsOfShape J D
inst✝⁶ : HasExactColimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : ReflectsFiniteLimits F
inst✝³ : HasFiniteLimits C
inst✝² : PreservesColimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cone G
hc : IsLimit c
⊢ (Cones.postcompose (isoWhiskerLeft G (preservesColimitNatIso F).symm).hom).obj
      (((whiskeringRight J C D).obj F ⋙ colim).mapCone c) ≅
    F.mapCone (colim.mapCone c)

Proof state:
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_2} J
inst✝⁹ : Category.{u_4, u_1} D
inst✝⁸ : HasColimitsOfShape J C
inst✝⁷ : HasColimitsOfShape J D
inst✝⁶ : HasExactColimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : ReflectsFiniteLimits F
inst✝³ : HasFiniteLimits C
inst✝² : PreservesColimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cone G
hc : IsLimit c
⊢ Nonempty (IsLimit (colim.mapCone 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_2} J
inst✝⁹ : Category.{u_4, u_1} D
inst✝⁸ : HasColimitsOfShape J C
inst✝⁷ : HasColimitsOfShape J D
inst✝⁶ : HasExactColimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : ReflectsFiniteLimits F
inst✝³ : HasFiniteLimits C
inst✝² : PreservesColimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cone G
hc : IsLimit c
⊢ IsLimit (colim.mapCone c)