-- 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₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X ≅ X'
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y ≅ Y'
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this_4 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
this_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
this_6 : HasSmallLocalizedHom W₂ Y' (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
e_β :
  Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
    (SmallHom.comp (W := W₂) (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom) (SmallHom.mk W₂ eY.inv))
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom)))
e_β₁ :
  Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ (eY.hom ≫ eY.inv))
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom)))
e_β₂ :
  Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)))
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom)))
⊢ Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom)
      (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.inv)
        (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))
have e_β₃ : Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
  (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
  (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
Tactic: rw [← SmallHom.comp_assoc, SmallHom.mk_comp_mk, eY.hom_inv_id, SmallHom.mk_id_comp]