-- Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
/-- Transfer preservation of limits along an equivalence in the shape. -/
lemma preservesLimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [PreservesLimitsOfShape J F] : PreservesLimitsOfShape J' F where
  preservesLimit {K} :=
    { preserves := fun {c} t => ⟨by
        let equ := e.invFunIdAssoc (K ⋙ F)
        have := (isLimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
        apply ((IsLimit.postcomposeHomEquiv equ _).symm this).ofIsoLimit
        refine Cones.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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
⊢ (Cones.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c))) ≅ F.mapCone c

Tactic:
refine Cones.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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
j : J'
⊢ ((Cones.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))).π.app j =
    (Iso.refl
          ((Cones.postcompose equ.hom).obj
              (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))).pt).hom ≫
      (F.mapCone 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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
j : J'
⊢ ((Cones.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))).π.app j =
    (Iso.refl
          ((Cones.postcompose equ.hom).obj
              (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))).pt).hom ≫
      (F.mapCone 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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
j : J'
⊢ F.map (c.π.app (e.functor.obj (e.inverse.obj j))) ≫ equ.hom.app 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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
⊢ IsLimit (F.mapCone c)

Tactic:
have := (isLimitOfPreserves 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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
⊢ IsLimit (F.mapCone 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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
⊢ IsLimit (F.mapCone 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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
⊢ IsLimit (F.mapCone 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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
⊢ IsLimit (F.mapCone c)

Tactic:
apply ((IsLimit.postcomposeHomEquiv equ _).symm this).ofIsoLimit

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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
⊢ (Cones.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c))) ≅ F.mapCone 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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
j : J'
⊢ F.map (c.π.app (e.functor.obj (e.inverse.obj j))) ≫ equ.hom.app j = 𝟙 (F.obj c.pt) ≫ F.map (c.π.app j)

Tactic:
simp [equ, ← Functor.map_comp]

Result:
no goals