-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
D₁ : Type u₃
inst_2 : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
X Y : C₁
inst_6 : HasSmallLocalizedHom W₁ X Y
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X ⟶ W₁.Q.obj Y
G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
β : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q G'
E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor
α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor
α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
γ : G' ⋙ E₂ ≅ E₁ ⋙ G :=
  liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G)
    ((W₁.Q.associator G' E₂).symm ≪≫
      Functor.isoWhiskerRight β.symm E₂ ≪≫
        Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂ ≪≫
          Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft α₂ ≪≫
            e ≪≫ Functor.isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)
hγ :
  ∀ (X : C₁),
    γ.hom.app (W₁.Q.obj X) =
      E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X)
simp :
  γ.hom.app (W₁.Q.obj X) ≫
      G.map (α₁.hom.app X) ≫
        e.inv.app X ≫
          α₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
            E₂.map (β.hom.app X) ≫
              (G' ⋙ E₂).map g ≫ E₂.map (β.inv.app Y) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
    (G' ⋙ E₂).map g ≫ γ.hom.app (W₁.Q.obj Y) ≫ G.map (α₁.hom.app Y) ≫ e.inv.app Y
⊢ α₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
      E₂.map (β.hom.app X ≫ G'.map g ≫ β.inv.app Y) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
    e.hom.app X ≫ G.map (α₁.inv.app X ≫ E₁.map g ≫ α₁.hom.app Y) ≫ e.inv.app Y

Tactic:
simp only [Functor.map_comp, ← NatIso.naturality_1 γ, ← Functor.comp_map,
    ← cancel_epi (e.inv.app X), ← cancel_epi (G.map (α₁.hom.app X)),
    ← cancel_epi (γ.hom.app (W₁.Q.obj X)), assoc, Iso.inv_hom_id_app_assoc,
    ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.map_id, id_comp,
    Iso.hom_inv_id_app_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatIso.naturality_1, CategoryTheory.MorphismProperty.Q, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Iso.inv, CategoryTheory.Functor.comp_map, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.Category.id_comp