-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
D₁ : Type u₁'
inst_2 : Category.{v₁', u₁'} D₁
D₂ : Type u₂'
inst_3 : Category.{v₂', u₂'} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₁', u₁, u₁'} C₁ D₁
L₂ : Functor.{v₂, v₂', u₂, u₂'} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
M : Type w'
inst_6 : AddMonoid M
inst_7 : HasShift.{v₁, u₁, w'} C₁ M
inst_8 : HasShift.{v₂, u₂, w'} C₂ M
inst_9 : HasShift.{v₁', u₁', w'} D₁ M
inst_10 : HasShift.{v₂', u₂', w'} D₂ M
inst_11 : L₁.CommShift M
inst_12 : L₂.CommShift M
inst_13 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst_14 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_15 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_16 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_17 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
G : Functor.{v₁', v₂', u₁', u₂'} D₁ D₂
inst_18 : G.CommShift M
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
inst_19 : NatTrans.CommShift e.hom M
m : M
f : SmallShiftedHom W₁ X₁ Y₁ m
this : HasSmallLocalizedHom W₂ X₂ X₂
a :
  Eq (α := L₂.obj X₂ ⟶ (shiftFunctor C₂ m ⋙ L₂).obj Y₂)
    ((Equiv.symm (Iso.homToEquiv (Iso.app (Functor.commShiftIso L₂ m) Y₂)) :
          (a : L₂.obj X₂ ⟶ (L₂ ⋙ shiftFunctor D₂ m).obj Y₂) → L₂.obj X₂ ⟶ (shiftFunctor C₂ m ⋙ L₂).obj Y₂)
        ((SmallShiftedHom.equiv W₂ L₂ : (a : SmallShiftedHom W₂ X₂ Y₂ m) → ShiftedHom (L₂.obj X₂) (L₂.obj Y₂) m)
            (Φ.smallShiftedHomMap (W₁ := W₁) (W₂ := W₂) eX eY f) :
          ShiftedHom (L₂.obj X₂) (L₂.obj Y₂) m) :
      L₂.obj X₂ ⟶ (shiftFunctor C₂ m ⋙ L₂).obj Y₂)
    ((Equiv.symm (Iso.homToEquiv (Iso.app (Functor.commShiftIso L₂ m) Y₂)) :
          (a : L₂.obj X₂ ⟶ (L₂ ⋙ shiftFunctor D₂ m).obj Y₂) → L₂.obj X₂ ⟶ (shiftFunctor C₂ m ⋙ L₂).obj Y₂)
        (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (L₂.map eX.inv ≫ e.hom.app X₁))
            (ShiftedHom.comp
              (ShiftedHom.map
                ((SmallShiftedHom.equiv W₁ L₁ : (a : SmallShiftedHom W₁ X₁ Y₁ m) → ShiftedHom (L₁.obj X₁) (L₁.obj Y₁) m)
                  f)
                G)
              (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Y₁ ≫ L₂.map eY.hom)) ⋯)
            ⋯ :
          ShiftedHom (L₂.obj X₂) (L₂.obj Y₂) m) :
      L₂.obj X₂ ⟶ (shiftFunctor C₂ m ⋙ L₂).obj Y₂)
⊢ Eq.{v₂' + 1} (α := ShiftedHom (L₂.obj X₂) (L₂.obj Y₂) m)
    ((SmallShiftedHom.equiv W₂ L₂ : (a : SmallShiftedHom W₂ X₂ Y₂ m) → ShiftedHom (L₂.obj X₂) (L₂.obj Y₂) m)
        (Φ.smallShiftedHomMap (W₁ := W₁) (W₂ := W₂) eX eY f) :
      ShiftedHom (L₂.obj X₂) (L₂.obj Y₂) m)
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (L₂.map eX.inv ≫ e.hom.app X₁))
        (ShiftedHom.comp
          (ShiftedHom.map
            ((SmallShiftedHom.equiv W₁ L₁ : (a : SmallShiftedHom W₁ X₁ Y₁ m) → ShiftedHom (L₁.obj X₁) (L₁.obj Y₁) m) f)
            G)
          (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Y₁ ≫ L₂.map eY.hom)) ⋯)
        ⋯ :
      ShiftedHom (L₂.obj X₂) (L₂.obj Y₂) m)

Tactic:
apply ((L₂.commShiftIso m).app Y₂).homToEquiv.symm.injective

Premises used: CategoryTheory.Iso.homToEquiv, Equiv.injective, CategoryTheory.Iso.app, Equiv.symm, CategoryTheory.Functor.CommShift.commShiftIso