-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
lemma HasExactColimitsOfShape.of_codomain_equivalence (J : Type*) [Category J] {D : Type*}
    [Category D] (e : C ≌ D) [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] :
    haveI : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
    HasExactColimitsOfShape 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✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
⊢ HasExactColimitsOfShape J D

Tactic:
haveI : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_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✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
⊢ HasExactColimitsOfShape 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✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
⊢ HasExactColimitsOfShape 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✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ PreservesLimit K colim

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✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.congrRight.inverse ⋙ colim ⋙ e.functor ≅ colim

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✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.symm.congrRight.functor.obj (e.congrRight.inverse ⋙ colim ⋙ e.functor) ≅ e.symm.congrRight.functor.obj colim

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✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ PreservesLimit K colim

Tactic:
refine preservesLimit_of_natIso K (?_ : e.congrRight.inverse ⋙ colim ⋙ e.functor ≅ colim)

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✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.congrRight.inverse ⋙ colim ⋙ e.functor ≅ colim

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✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.symm.congrRight.functor.obj (e.congrRight.inverse ⋙ colim ⋙ e.functor) ≅ e.symm.congrRight.functor.obj colim

Tactic:
exact isoWhiskerLeft (_ ⋙ colim) e.unitIso.symm ≪≫ (preservesColimitNatIso e.inverse).symm

Result:
no goals