-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
lemma HasExactLimitsOfShape.of_codomain_equivalence (J : Type*) [Category J] {D : Type*}
    [Category D] (e : C ≌ D) [HasLimitsOfShape J C] [HasExactLimitsOfShape J C] :
    haveI : HasLimitsOfShape J D := Adjunction.hasLimitsOfShape_of_equivalence e.inverse
    HasExactLimitsOfShape J D

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{u_3, u_1} J
D : Type u_2
inst✝² : Category.{u_4, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim

Tactic:
apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{u_3, u_1} J
D : Type u_2
inst✝² : Category.{u_4, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.symm.congrRight.functor.obj (e.congrRight.inverse ⋙ lim ⋙ e.functor) ≅ e.symm.congrRight.functor.obj lim

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{u_3, u_1} J
D : Type u_2
inst✝² : Category.{u_4, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.symm.congrRight.functor.obj (e.congrRight.inverse ⋙ lim ⋙ e.functor) ≅ e.symm.congrRight.functor.obj lim

Tactic:
exact isoWhiskerLeft (_ ⋙ lim) e.unitIso.symm ≪≫ (preservesLimitNatIso e.inverse).symm

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{u_3, u_1} J
D : Type u_2
inst✝² : Category.{u_4, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
⊢ HasExactLimitsOfShape J D

Tactic:
refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{u_3, u_1} J
D : Type u_2
inst✝² : Category.{u_4, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ PreservesColimit K lim

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{u_3, u_1} J
D : Type u_2
inst✝² : Category.{u_4, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ PreservesColimit K lim

Tactic:
refine preservesColimit_of_natIso K (?_ : e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim)

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{u_3, u_1} J
D : Type u_2
inst✝² : Category.{u_4, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{u_3, u_1} J
D : Type u_2
inst✝² : Category.{u_4, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
⊢ HasExactLimitsOfShape J D

Tactic:
haveI : HasLimitsOfShape J D := Adjunction.hasLimitsOfShape_of_equivalence e.inverse

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{u_3, u_1} J
D : Type u_2
inst✝² : Category.{u_4, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
⊢ HasExactLimitsOfShape J D