-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y Z : C
inst_3 : HasSmallLocalizedHom W X Y
inst_4 : HasSmallLocalizedHom W Y Z
inst_5 : HasSmallLocalizedHom W X Z
this_1 : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := ⋯
this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := ⋯
α : W.Q.obj X ⟶ W.Q.obj Y
β : W.Q.obj Y ⟶ W.Q.obj Z
⊢ Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Z)
    ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Z) → L.obj X ⟶ L.obj Z)
        ((Equiv.symm (equivShrink (W.Q.obj X ⟶ W.Q.obj Z)) : (a : SmallHom W X Z) → W.Q.obj X ⟶ W.Q.obj Z)
          ((equivShrink (W.Q.obj X ⟶ W.Q.obj Z) : (a : W.Q.obj X ⟶ W.Q.obj Z) → SmallHom W X Z)
            ((homEquiv W W.Q W.Q : (a : W.Q.obj X ⟶ W.Q.obj Z) → W.Q.obj X ⟶ W.Q.obj Z)
                (CategoryStruct.comp (Y := W.Q.obj Y)
                  ((homEquiv W W.Q W.Q : (a : W.Q.obj X ⟶ W.Q.obj Y) → W.Q.obj X ⟶ W.Q.obj Y)
                    ((Equiv.symm (equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y)
                      ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
                          (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
                        α)))
                  ((homEquiv W W.Q W.Q : (a : W.Q.obj Y ⟶ W.Q.obj Z) → W.Q.obj Y ⟶ W.Q.obj Z)
                    ((Equiv.symm (equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) : (a : SmallHom W Y Z) → W.Q.obj Y ⟶ W.Q.obj Z)
                      ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z) :
                          (a : W.Q.obj Y ⟶ W.Q.obj Z) → Shrink.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z))
                        β)))) :
              W.Q.obj X ⟶ W.Q.obj Z))) :
      L.obj X ⟶ L.obj Z)
    (CategoryStruct.comp (Y := L.obj Y)
        ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Y) → L.obj X ⟶ L.obj Y)
          ((Equiv.symm (equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y)
            ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
                (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
              α)))
        ((homEquiv W W.Q L : (a : W.Q.obj Y ⟶ W.Q.obj Z) → L.obj Y ⟶ L.obj Z)
          ((Equiv.symm (equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) : (a : SmallHom W Y Z) → W.Q.obj Y ⟶ W.Q.obj Z)
            ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z) :
                (a : W.Q.obj Y ⟶ W.Q.obj Z) → Shrink.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z))
              β))) :
      L.obj X ⟶ L.obj Z)
have rw : Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Z)
  ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Z) → L.obj X ⟶ L.obj Z)
      ((homEquiv W W.Q W.Q : (a : W.Q.obj X ⟶ W.Q.obj Z) → W.Q.obj X ⟶ W.Q.obj Z)
        (CategoryStruct.comp (Y := W.Q.obj Y)
          ((homEquiv W W.Q W.Q : (a : W.Q.obj X ⟶ W.Q.obj Y) → W.Q.obj X ⟶ W.Q.obj Y)
            ((Equiv.symm (equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y)
              ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
                  (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
                α)))
          ((homEquiv W W.Q W.Q : (a : W.Q.obj Y ⟶ W.Q.obj Z) → W.Q.obj Y ⟶ W.Q.obj Z)
            ((Equiv.symm (equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) : (a : SmallHom W Y Z) → W.Q.obj Y ⟶ W.Q.obj Z)
              ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z) :
                  (a : W.Q.obj Y ⟶ W.Q.obj Z) → Shrink.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z))
                β))))) :
    L.obj X ⟶ L.obj Z)
  (CategoryStruct.comp (Y := L.obj Y)
      ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Y) → L.obj X ⟶ L.obj Y)
        ((Equiv.symm (equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y)
          ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
              (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
            α)))
      ((homEquiv W W.Q L : (a : W.Q.obj Y ⟶ W.Q.obj Z) → L.obj Y ⟶ L.obj Z)
        ((Equiv.symm (equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) : (a : SmallHom W Y Z) → W.Q.obj Y ⟶ W.Q.obj Z)
          ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z) :
              (a : W.Q.obj Y ⟶ W.Q.obj Z) → Shrink.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z))
            β))) :
    L.obj X ⟶ L.obj Z)
Tactic: rw [Equiv.symm_apply_apply]