-- 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)
    ((equiv W L : (a : SmallHom W X Z) → L.obj X ⟶ L.obj Z)
        (comp (W := W) (Y := 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))
            α)
          ((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)
        ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.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))
            α))
        ((equiv W L : (a : SmallHom W Y Z) → L.obj Y ⟶ L.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 dsimp : 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)
Tactic: dsimp [equiv, comp]