-- Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean
lemma equiv_comp [HasSmallLocalizedShiftedHom.{w} W M X Y]
    [HasSmallLocalizedShiftedHom.{w} W M Y Z] [HasSmallLocalizedShiftedHom.{w} W M X Z]
    [HasSmallLocalizedShiftedHom.{w} W M Z Z] {a b c : M}
    (f : SmallShiftedHom.{w} W X Y a) (g : SmallShiftedHom.{w} W Y Z b) (h : b + a = c) :
    equiv W L (f.comp g h) = (equiv W L f).comp (equiv W L g) h

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 Z : C
inst✝⁴ : W.IsCompatibleWithShift M
inst✝³ : HasSmallLocalizedShiftedHom W M X Y
inst✝² : HasSmallLocalizedShiftedHom W M Y Z
inst✝¹ : HasSmallLocalizedShiftedHom W M X Z
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
⊢ (equiv W L) (f.comp g h) = ((equiv W L) f).comp ((equiv W L) g) h

Tactic:
dsimp [comp, equiv, ShiftedHom.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 Z : C
inst✝⁴ : W.IsCompatibleWithShift M
inst✝³ : HasSmallLocalizedShiftedHom W M X Y
inst✝² : HasSmallLocalizedShiftedHom W M Y Z
inst✝¹ : HasSmallLocalizedShiftedHom W M X Z
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
⊢ ((L.commShiftIso c).app Z).homToEquiv ((SmallHom.equiv W L) (SmallHom.comp f (g.shift a c h))) =
    ((L.commShiftIso a).app Y).homToEquiv ((SmallHom.equiv W L) f) ≫
      (shiftFunctor D a).map (((L.commShiftIso b).app Z).homToEquiv ((SmallHom.equiv W L) g)) ≫
        (shiftFunctorAdd' D b a c h).inv.app (L.obj Z)

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 Z : C
inst✝⁴ : W.IsCompatibleWithShift M
inst✝³ : HasSmallLocalizedShiftedHom W M X Y
inst✝² : HasSmallLocalizedShiftedHom W M Y Z
inst✝¹ : HasSmallLocalizedShiftedHom W M X Z
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
⊢ (SmallHom.equiv W L) f ≫
      (L.commShiftIso a).hom.app Y ≫
        (shiftFunctor D a).map ((SmallHom.equiv W L) g) ≫
          (shiftFunctor D a).map ((L.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (L.obj Z) =
    (SmallHom.equiv W L) f ≫
      (L.commShiftIso a).hom.app Y ≫
        (shiftFunctor D a).map ((SmallHom.equiv W L) g) ≫
          (shiftFunctor D a).map ((L.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (L.obj Z)

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 Z : C
inst✝⁴ : W.IsCompatibleWithShift M
inst✝³ : HasSmallLocalizedShiftedHom W M X Y
inst✝² : HasSmallLocalizedShiftedHom W M Y Z
inst✝¹ : HasSmallLocalizedShiftedHom W M X Z
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
⊢ ((SmallHom.equiv W L) f ≫ (SmallHom.equiv W L) (g.shift a c h)) ≫ ((L.commShiftIso c).app Z).hom =
    ((SmallHom.equiv W L) f ≫ ((L.commShiftIso a).app Y).hom) ≫
      (shiftFunctor D a).map ((SmallHom.equiv W L) g ≫ ((L.commShiftIso b).app Z).hom) ≫
        (shiftFunctorAdd' D b a c h).inv.app (L.obj Z)

Tactic:
simp only [equiv_shift', 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 Z : C
inst✝⁴ : W.IsCompatibleWithShift M
inst✝³ : HasSmallLocalizedShiftedHom W M X Y
inst✝² : HasSmallLocalizedShiftedHom W M Y Z
inst✝¹ : HasSmallLocalizedShiftedHom W M X Z
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
⊢ (SmallHom.equiv W L) f ≫
      (L.commShiftIso a).hom.app Y ≫
        (shiftFunctor D a).map ((SmallHom.equiv W L) g) ≫
          (shiftFunctor D a).map ((L.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (L.obj Z) =
    (SmallHom.equiv W L) f ≫
      (L.commShiftIso a).hom.app Y ≫
        (shiftFunctor D a).map ((SmallHom.equiv W L) g) ≫
          (shiftFunctor D a).map ((L.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (L.obj Z)

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 Z : C
inst✝⁴ : W.IsCompatibleWithShift M
inst✝³ : HasSmallLocalizedShiftedHom W M X Y
inst✝² : HasSmallLocalizedShiftedHom W M Y Z
inst✝¹ : HasSmallLocalizedShiftedHom W M X Z
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
⊢ ((L.commShiftIso c).app Z).homToEquiv ((SmallHom.equiv W L) (SmallHom.comp f (g.shift a c h))) =
    ((L.commShiftIso a).app Y).homToEquiv ((SmallHom.equiv W L) f) ≫
      (shiftFunctor D a).map (((L.commShiftIso b).app Z).homToEquiv ((SmallHom.equiv W L) g)) ≫
        (shiftFunctorAdd' D b a c h).inv.app (L.obj Z)

Tactic:
erw [Iso.homToEquiv_apply, Iso.homToEquiv_apply, Iso.homToEquiv_apply, SmallHom.equiv_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 Z : C
inst✝⁴ : W.IsCompatibleWithShift M
inst✝³ : HasSmallLocalizedShiftedHom W M X Y
inst✝² : HasSmallLocalizedShiftedHom W M Y Z
inst✝¹ : HasSmallLocalizedShiftedHom W M X Z
inst✝ : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
⊢ ((SmallHom.equiv W L) f ≫ (SmallHom.equiv W L) (g.shift a c h)) ≫ ((L.commShiftIso c).app Z).hom =
    ((SmallHom.equiv W L) f ≫ ((L.commShiftIso a).app Y).hom) ≫
      (shiftFunctor D a).map ((SmallHom.equiv W L) g ≫ ((L.commShiftIso b).app Z).hom) ≫
        (shiftFunctorAdd' D b a c h).inv.app (L.obj Z)