-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
/-- Let `adj : F ⊣ G` be an adjunction, with `F : C ⥤ D` coreflective.
Assume that `C` has finite colimits and `G` commutes to them.
If `D` has exact limits of shape `J`, then `C` also has exact limits of shape `J`. -/
lemma hasExactLimitsOfShape (adj : F ⊣ G) [F.Full] [F.Faithful]
    (J : Type u') [Category.{v'} J] [HasLimitsOfShape J C] [HasLimitsOfShape J D]
    [HasExactLimitsOfShape J D] [HasFiniteColimits C] [PreservesFiniteColimits G] :
    HasExactLimitsOfShape J C where
  preservesFiniteColimits:= ⟨fun K _ _ ↦ ⟨fun {H} ↦ by
    have : PreservesLimitsOfSize.{v', u'} G := adj.rightAdjoint_preservesLimits
    have : PreservesColimitsOfSize.{0, 0} F := adj.leftAdjoint_preservesColimits
    let e : (whiskeringRight J _ _).obj F ⋙ lim ⋙ G ≅ lim :=
      isoWhiskerLeft _ (preservesLimitNatIso G) ≪≫
        (Functor.associator _ _ _).symm ≪≫
        isoWhiskerRight (whiskeringRightObjCompIso F G) _ ≪≫
        isoWhiskerRight ((whiskeringRight J C C).mapIso (asIso adj.unit).symm) _ ≪≫
        isoWhiskerRight wiskeringRightObjIdIso _ ≪≫ lim.leftUnitor
    exact preservesColimit_of_natIso _ e⟩⟩

Proof state:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
this✝ : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
this : PreservesColimitsOfSize.{0, 0, v, v'', u, u''} F
e : (whiskeringRight J C D).obj F ⋙ lim ⋙ G ≅ lim :=
  isoWhiskerLeft ((whiskeringRight J C D).obj F) (preservesLimitNatIso G) ≪≫
    (((whiskeringRight J C D).obj F).associator ((whiskeringRight J D C).obj G) lim).symm ≪≫
      isoWhiskerRight (whiskeringRightObjCompIso F G) lim ≪≫
        isoWhiskerRight ((whiskeringRight J C C).mapIso (asIso adj.unit).symm) lim ≪≫
          isoWhiskerRight wiskeringRightObjIdIso lim ≪≫ lim.leftUnitor
⊢ PreservesColimit H lim

Tactic:
exact preservesColimit_of_natIso _ e

Result:
no goals

Proof state:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
⊢ PreservesColimit H lim

Tactic:
have : PreservesLimitsOfSize.{v', u'} G := adj.rightAdjoint_preservesLimits

Result:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
this : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
⊢ PreservesColimit H lim

Proof state:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
this : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
⊢ PreservesColimit H lim

Tactic:
have : PreservesColimitsOfSize.{0, 0} F := adj.leftAdjoint_preservesColimits

Result:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
this✝ : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
this : PreservesColimitsOfSize.{0, 0, v, v'', u, u''} F
⊢ PreservesColimit H lim

Proof state:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
this✝ : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
this : PreservesColimitsOfSize.{0, 0, v, v'', u, u''} F
⊢ PreservesColimit H lim

Tactic:
let e : (whiskeringRight J _ _).obj F ⋙ lim ⋙ G ≅ lim :=
  isoWhiskerLeft _ (preservesLimitNatIso G) ≪≫
    (Functor.associator _ _ _).symm ≪≫
    isoWhiskerRight (whiskeringRightObjCompIso F G) _ ≪≫
    isoWhiskerRight ((whiskeringRight J C C).mapIso (asIso adj.unit).symm) _ ≪≫
    isoWhiskerRight wiskeringRightObjIdIso _ ≪≫ lim.leftUnitor

Result:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
this✝ : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
this : PreservesColimitsOfSize.{0, 0, v, v'', u, u''} F
e : (whiskeringRight J C D).obj F ⋙ lim ⋙ G ≅ lim :=
  isoWhiskerLeft ((whiskeringRight J C D).obj F) (preservesLimitNatIso G) ≪≫
    (((whiskeringRight J C D).obj F).associator ((whiskeringRight J D C).obj G) lim).symm ≪≫
      isoWhiskerRight (whiskeringRightObjCompIso F G) lim ≪≫
        isoWhiskerRight ((whiskeringRight J C C).mapIso (asIso adj.unit).symm) lim ≪≫
          isoWhiskerRight wiskeringRightObjIdIso lim ≪≫ lim.leftUnitor
⊢ PreservesColimit H lim