-- Mathlib/CategoryTheory/Presentable/Basic.lean
lemma isCardinalPresentable_of_equivalence
    {C' : Type u₃} [Category.{v₃} C'] [IsCardinalPresentable X κ] (e : C ≌ C') :
    IsCardinalPresentable (e.functor.obj X) κ

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)))

Tactic:
have := preservesColimitsOfShape_of_isCardinalPresentable X κ J

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
X✝ Y✝ : C'
f : X✝ ⟶ Y✝
⊢ (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
      ((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) Y✝).hom =
    ((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) X✝).hom ≫
      (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f

Tactic:
ext ⟨g⟩

Result:
case h.up
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
X✝ Y✝ : C'
f : X✝ ⟶ Y✝
g : (coyoneda.obj (op (e.functor.obj X))).obj X✝
⊢ ((coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
        ((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) Y✝).hom)
      { down := g } =
    (((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) X✝).hom ≫
        (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f)
      { down := g }

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
iso :
  coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃} ≅ e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})

Tactic:
exact preservesColimit_of_natIso Y iso.symm

Result:
no goals

Proof state:
case h.up.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
X✝ Y✝ : C'
f : X✝ ⟶ Y✝
g : (coyoneda.obj (op (e.functor.obj X))).obj X✝
⊢ Equiv.ulift
      (((coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
          ((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) Y✝).hom)
        { down := g }) =
    Equiv.ulift
      ((((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) X✝).hom ≫
          (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f)
        { down := g })

Tactic:
simp [Adjunction.homEquiv_unit]

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
⊢ IsCardinalPresentable (e.functor.obj X) κ

Tactic:
refine ⟨fun J _ _ ↦ ⟨fun {Y} ↦ ?_⟩⟩

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ ∀ {X_1 Y : C'} (f : X_1 ⟶ Y),
    (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
        ((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) Y).hom =
      ((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) X_1).hom ≫
        (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f

Tactic:
intro _ _ f

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
X✝ Y✝ : C'
f : X✝ ⟶ Y✝
⊢ (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
      ((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) Y✝).hom =
    ((fun Z => (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) X✝).hom ≫
      (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})

Tactic:
have iso : coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁} ≅
  e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃} :=
  NatIso.ofComponents (fun Z ↦
    (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) (by
      intro _ _ f
      ext ⟨g⟩
      apply Equiv.ulift.injective
      simp [Adjunction.homEquiv_unit])

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
iso :
  coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃} ≅ e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})