-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
/-- Let `adj : F ⊣ G` be an adjunction, with `G : D ⥤ C` reflective.
Assume that `D` has finite limits and `F` commutes to them.
If `C` has exact colimits of shape `J`, then `D` also has exact colimits of shape `J`. -/
lemma hasExactColimitsOfShape (adj : F ⊣ G) [G.Full] [G.Faithful]
    (J : Type u') [Category.{v'} J] [HasColimitsOfShape J C] [HasColimitsOfShape J D]
    [HasExactColimitsOfShape J C] [HasFiniteLimits D] [PreservesFiniteLimits F] :
    HasExactColimitsOfShape J D where
  preservesFiniteLimits := ⟨fun K _ _ ↦ ⟨fun {H} ↦ by
    have : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
    have : PreservesColimitsOfSize.{v', u'} F := adj.leftAdjoint_preservesColimits
    let e : (whiskeringRight J D C).obj G ⋙ colim ⋙ F ≅ colim :=
      isoWhiskerLeft _ (preservesColimitNatIso F) ≪≫ (Functor.associator _ _ _).symm ≪≫
        isoWhiskerRight (whiskeringRightObjCompIso G F) _ ≪≫
        isoWhiskerRight ((whiskeringRight J D D).mapIso (asIso adj.counit)) _ ≪≫
        isoWhiskerRight wiskeringRightObjIdIso _ ≪≫ colim.leftUnitor
    exact preservesLimit_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✝⁷ : G.Full
inst✝⁶ : G.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasColimitsOfShape J C
inst✝³ : HasColimitsOfShape J D
inst✝² : HasExactColimitsOfShape J C
inst✝¹ : HasFiniteLimits D
inst✝ : PreservesFiniteLimits F
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ D
⊢ PreservesLimit H colim

Tactic:
have : PreservesLimitsOfSize.{0, 0} 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✝⁷ : G.Full
inst✝⁶ : G.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasColimitsOfShape J C
inst✝³ : HasColimitsOfShape J D
inst✝² : HasExactColimitsOfShape J C
inst✝¹ : HasFiniteLimits D
inst✝ : PreservesFiniteLimits F
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ D
this : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
⊢ PreservesLimit H colim

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✝⁷ : G.Full
inst✝⁶ : G.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasColimitsOfShape J C
inst✝³ : HasColimitsOfShape J D
inst✝² : HasExactColimitsOfShape J C
inst✝¹ : HasFiniteLimits D
inst✝ : PreservesFiniteLimits F
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ D
this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
this : PreservesColimitsOfSize.{v', u', v, v'', u, u''} F
⊢ PreservesLimit H colim

Tactic:
let e : (whiskeringRight J D C).obj G ⋙ colim ⋙ F ≅ colim :=
  isoWhiskerLeft _ (preservesColimitNatIso F) ≪≫ (Functor.associator _ _ _).symm ≪≫
    isoWhiskerRight (whiskeringRightObjCompIso G F) _ ≪≫
    isoWhiskerRight ((whiskeringRight J D D).mapIso (asIso adj.counit)) _ ≪≫
    isoWhiskerRight wiskeringRightObjIdIso _ ≪≫ colim.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✝⁷ : G.Full
inst✝⁶ : G.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasColimitsOfShape J C
inst✝³ : HasColimitsOfShape J D
inst✝² : HasExactColimitsOfShape J C
inst✝¹ : HasFiniteLimits D
inst✝ : PreservesFiniteLimits F
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ D
this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
this : PreservesColimitsOfSize.{v', u', v, v'', u, u''} F
e : (whiskeringRight J D C).obj G ⋙ colim ⋙ F ≅ colim :=
  isoWhiskerLeft ((whiskeringRight J D C).obj G) (preservesColimitNatIso F) ≪≫
    (((whiskeringRight J D C).obj G).associator ((whiskeringRight J C D).obj F) colim).symm ≪≫
      isoWhiskerRight (whiskeringRightObjCompIso G F) colim ≪≫
        isoWhiskerRight ((whiskeringRight J D D).mapIso (asIso adj.counit)) colim ≪≫
          isoWhiskerRight wiskeringRightObjIdIso colim ≪≫ colim.leftUnitor
⊢ PreservesLimit H colim

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✝⁷ : G.Full
inst✝⁶ : G.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasColimitsOfShape J C
inst✝³ : HasColimitsOfShape J D
inst✝² : HasExactColimitsOfShape J C
inst✝¹ : HasFiniteLimits D
inst✝ : PreservesFiniteLimits F
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ D
this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
this : PreservesColimitsOfSize.{v', u', v, v'', u, u''} F
e : (whiskeringRight J D C).obj G ⋙ colim ⋙ F ≅ colim :=
  isoWhiskerLeft ((whiskeringRight J D C).obj G) (preservesColimitNatIso F) ≪≫
    (((whiskeringRight J D C).obj G).associator ((whiskeringRight J C D).obj F) colim).symm ≪≫
      isoWhiskerRight (whiskeringRightObjCompIso G F) colim ≪≫
        isoWhiskerRight ((whiskeringRight J D D).mapIso (asIso adj.counit)) colim ≪≫
          isoWhiskerRight wiskeringRightObjIdIso colim ≪≫ colim.leftUnitor
⊢ PreservesLimit H colim

Tactic:
exact preservesLimit_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✝⁷ : G.Full
inst✝⁶ : G.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasColimitsOfShape J C
inst✝³ : HasColimitsOfShape J D
inst✝² : HasExactColimitsOfShape J C
inst✝¹ : HasFiniteLimits D
inst✝ : PreservesFiniteLimits F
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ D
this : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
⊢ PreservesLimit H colim

Tactic:
have : PreservesColimitsOfSize.{v', u'} 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✝⁷ : G.Full
inst✝⁶ : G.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasColimitsOfShape J C
inst✝³ : HasColimitsOfShape J D
inst✝² : HasExactColimitsOfShape J C
inst✝¹ : HasFiniteLimits D
inst✝ : PreservesFiniteLimits F
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ D
this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
this : PreservesColimitsOfSize.{v', u', v, v'', u, u''} F
⊢ PreservesLimit H colim