-- Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean
lemma equiv_shift {a : M} [HasSmallLocalizedShiftedHom.{w} W M X Y]
    [HasSmallLocalizedShiftedHom.{w} W M Y Y]
    (f : SmallShiftedHom.{w} W X Y a) (n a' : M) (h : a + n = a') :
    equiv W L (f.shift n a' h) = (L.commShiftIso n).hom.app X ≫ (equiv W L f)⟦n⟧' ≫
      (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)

Proof state:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ (equiv W L) (f.shift n a' h) =
    (L.commShiftIso n).hom.app X ≫
      (shiftFunctor D n).map ((equiv W L) f) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)

Tactic:
dsimp [equiv]

Result:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ ((L.commShiftIso a').app Y).homToEquiv ((SmallHom.equiv W L) (f.shift n a' h)) =
    (L.commShiftIso n).hom.app X ≫
      (shiftFunctor D n).map (((L.commShiftIso a).app Y).homToEquiv ((SmallHom.equiv W L) f)) ≫
        (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)

Proof state:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ ((L.commShiftIso n).hom.app X ≫
        (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
          (shiftFunctor D n).map ((L.commShiftIso a).hom.app Y) ≫
            (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (L.commShiftIso a').inv.app Y) ≫
      ((L.commShiftIso a').app Y).hom =
    (L.commShiftIso n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f ≫ ((L.commShiftIso a).app Y).hom) ≫
        (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)

Tactic:
simp only [Functor.comp_obj, Iso.app_hom, assoc, Iso.inv_hom_id_app, comp_id, Functor.map_comp]

Result:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ (L.commShiftIso n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
        (shiftFunctor D n).map ((L.commShiftIso a).hom.app Y) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) =
    (L.commShiftIso n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
        (shiftFunctor D n).map ((L.commShiftIso a).hom.app Y) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)

Proof state:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ (L.commShiftIso n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
        (shiftFunctor D n).map ((L.commShiftIso a).hom.app Y) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) =
    (L.commShiftIso n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
        (shiftFunctor D n).map ((L.commShiftIso a).hom.app Y) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ ((L.commShiftIso a').app Y).homToEquiv ((SmallHom.equiv W L) (f.shift n a' h)) =
    (L.commShiftIso n).hom.app X ≫
      (shiftFunctor D n).map (((L.commShiftIso a).app Y).homToEquiv ((SmallHom.equiv W L) f)) ≫
        (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)

Tactic:
erw [Iso.homToEquiv_apply, Iso.homToEquiv_apply, equiv_shift']

Result:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ ((L.commShiftIso n).hom.app X ≫
        (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
          (shiftFunctor D n).map ((L.commShiftIso a).hom.app Y) ≫
            (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (L.commShiftIso a').inv.app Y) ≫
      ((L.commShiftIso a').app Y).hom =
    (L.commShiftIso n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f ≫ ((L.commShiftIso a).app Y).hom) ≫
        (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)