-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
rw :
  ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
          (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
        (isoOfHom L₁ W f hf).inv ≫
      (isoOfHom L₂ W f hf).hom =
    (isoOfHom L₂ W f hf).inv ≫ (isoOfHom L₂ W f hf).hom
rw₁ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv ≫
        (isoOfHom L₂ W f hf).hom :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₂ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv ≫
        L₂.map f :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₃ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (CategoryStruct.comp (Y := L₂.obj Y)
        (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv)
        (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj Y ⟶ L₁.obj X) (L₂.obj Y ⟶ L₂.obj X)) :
            (a : L₁.obj Y ⟶ L₁.obj X) → L₂.obj Y ⟶ L₂.obj X)
          (L₁.map f)) :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₄ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj X) (L₂.obj X ⟶ L₂.obj X)) :
          (a : L₁.obj X ⟶ L₁.obj X) → L₂.obj X ⟶ L₂.obj X)
        ((isoOfHom L₁ W f hf).inv ≫ L₁.map f) :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₅ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj X) (L₂.obj X ⟶ L₂.obj X)) :
          (a : L₁.obj X ⟶ L₁.obj X) → L₂.obj X ⟶ L₂.obj X)
        (𝟙 (L₁.obj X)) :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₆ rw₇ : Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X) (𝟙 (L₂.obj X)) (𝟙 (L₂.obj X))
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      (isoOfHom L₁ W f hf).inv =
    (isoOfHom L₂ W f hf).inv

Tactic:
rw [← cancel_mono (isoOfHom L₂ W f hf).hom, Iso.inv_hom_id, isoOfHom_hom,
    ← homEquiv_map W L₁ L₂ f, ← homEquiv_comp, isoOfHom_inv_hom_id, homEquiv_id]

Premises used: CategoryTheory.Localization.isoOfHom_inv_hom_id, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Localization.isoOfHom_hom, CategoryTheory.Localization.homEquiv_comp, CategoryTheory.cancel_mono, CategoryTheory.Localization.isoOfHom, CategoryTheory.Localization.homEquiv_map, CategoryTheory.Iso.hom, CategoryTheory.Localization.homEquiv_id