-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
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₂
⊢ (SmallHom.equiv W₂ L₂ :
        (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) → L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))
      ((Equiv.symm (SmallHom.equiv W₂ W₂.Q) :
          (a : W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Y)) →
            SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y))
        ((Iso.homCongr
                (Iso.app
                  (Iso.symm
                    (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
                      (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
                  X)
                (Iso.app
                  (Iso.symm
                    (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
                      (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
                  Y) :
              (a : (W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q).obj X ⟶ (W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q).obj Y) →
                (Φ.functor ⋙ W₂.Q).obj X ⟶ (Φ.functor ⋙ W₂.Q).obj Y)
            ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map g) :
          (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).obj X ⟶ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).obj Y)) =
    e.hom.app X ≫
      G.map
          ((SmallHom.equiv W₁ L₁ : (a : SmallHom W₁ X Y) → L₁.obj X ⟶ L₁.obj Y)
            ((Equiv.symm (SmallHom.equiv W₁ W₁.Q) : (a : W₁.Q.obj X ⟶ W₁.Q.obj Y) → SmallHom W₁ X Y) g)) ≫
        e.inv.app Y
have rw : α₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
    E₂.map
        ((Iso.homCongr
              (Iso.app
                (Iso.symm
                  (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
                    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
                X)
              (Iso.app
                (Iso.symm
                  (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
                    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
                Y) :
            (a : (W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q).obj X ⟶ (W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q).obj Y) →
              (Φ.functor ⋙ W₂.Q).obj X ⟶ (Φ.functor ⋙ W₂.Q).obj Y)
          ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map g)) ≫
      α₂.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: rw [SmallHom.equiv_equiv_symm W₁ W₁.Q L₁ E₁ α₁,
    SmallHom.equiv_equiv_symm W₂ W₂.Q L₂ E₂ α₂]