-- Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
/-- Transfer preservation of colimits along an equivalence in the shape. -/
lemma preservesColimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [PreservesColimitsOfShape J F] : PreservesColimitsOfShape J' F where
  preservesColimit {K} :=
    { preserves := fun {c} t => ⟨by
        let equ := e.invFunIdAssoc (K ⋙ F)
        have := (isColimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
        apply ((IsColimit.precomposeInvEquiv equ _).symm this).ofIsoColimit
        refine Cocones.ext (Iso.refl _) fun j => ?_
        dsimp
        simp [equ, ← Functor.map_comp]⟩ }

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
⊢ IsColimit (F.mapCocone c)

Tactic:
have := (isColimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ IsColimit (F.mapCocone c)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ IsColimit (F.mapCocone c)

Tactic:
apply ((IsColimit.precomposeInvEquiv equ _).symm this).ofIsoColimit

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ (Cocones.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c))) ≅
    F.mapCocone c

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ (Cocones.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c))) ≅
    F.mapCocone c

Tactic:
refine Cocones.ext (Iso.refl _) fun j => ?_

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
j : J'
⊢ ((Cocones.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))).ι.app
        j ≫
      (Iso.refl
          ((Cocones.precompose equ.inv).obj
              (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))).pt).hom =
    (F.mapCocone c).ι.app j

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
j : J'
⊢ ((Cocones.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))).ι.app
        j ≫
      (Iso.refl
          ((Cocones.precompose equ.inv).obj
              (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))).pt).hom =
    (F.mapCocone c).ι.app j

Tactic:
dsimp

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
j : J'
⊢ (equ.inv.app j ≫ F.map (c.ι.app (e.functor.obj (e.inverse.obj j)))) ≫ 𝟙 (F.obj c.pt) = F.map (c.ι.app j)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
j : J'
⊢ (equ.inv.app j ≫ F.map (c.ι.app (e.functor.obj (e.inverse.obj j)))) ≫ 𝟙 (F.obj c.pt) = F.map (c.ι.app j)

Tactic:
simp [equ, ← Functor.map_comp]

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
⊢ IsColimit (F.mapCocone c)

Tactic:
let equ := e.invFunIdAssoc (K ⋙ F)

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
⊢ IsColimit (F.mapCocone c)