-- Module: Mathlib.CategoryTheory.Localization.SmallHom
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
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)
⊢ 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)

Tactic:
dsimp [equiv, comp]

Premises used: CategoryTheory.Localization.SmallHom.equiv, CategoryTheory.Localization.SmallHom.comp