-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, g ≤ f
w :
  CategoryStruct.comp (Y :=
      image (X :=
        sigmaObj.{w, v₁, u₁}
          fun
            (j :
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w)) ↦
          Functor.obj (C := Subobject.{v₁, u₁} A) underlying
            ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
              (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
        (smallCoproductDesc s :
          (sigmaObj.{w, v₁, u₁}
              fun
                (j :
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w)) ↦
              Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                    (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                  (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
            A))
      (Iso.hom (underlyingIso (image.ι (smallCoproductDesc s))) :
        Functor.obj underlying
            (mk (A :=
              image (X :=
                sigmaObj.{w, v₁, u₁}
                  fun
                    (j :
                      (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                            s) :
                        Type w)) ↦
                  Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                        (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                      (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
                (smallCoproductDesc s :
                  (sigmaObj.{w, v₁, u₁}
                      fun
                        (j :
                          (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                  (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                                s) :
                            Type w)) ↦
                      Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                        ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                          (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                    A))
              (image.ι (smallCoproductDesc s) :
                image (X :=
                    sigmaObj.{w, v₁, u₁}
                      fun
                        (j :
                          (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                  (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                                s) :
                            Type w)) ↦
                      Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                        ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                          (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
                    (smallCoproductDesc s :
                      (sigmaObj.{w, v₁, u₁}
                          fun
                            (j :
                              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                      (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                                    s) :
                                Type w)) ↦
                          Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                            ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                                (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                              (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                        A) ⟶
                  A)) ⟶
          image (X :=
            sigmaObj.{w, v₁, u₁}
              fun
                (j :
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w)) ↦
              Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                    (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                  (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
            (smallCoproductDesc s :
              (sigmaObj.{w, v₁, u₁}
                  fun
                    (j :
                      (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                            s) :
                        Type w)) ↦
                  Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                        (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                      (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                A))
      (image.lift
            { I := Functor.obj underlying f, m := f.arrow, m_mono := ⋯,
              e :=
                Sigma.desc
                  fun
                    (b :
                      (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                            s) :
                        Type w)) ↦
                  Functor.map underlying (homOfLE ⋯),
              fac := ⋯ } ≫
          f.arrow :
        image (X :=
            sigmaObj.{w, v₁, u₁}
              fun
                (j :
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w)) ↦
              Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                    (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                  (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
            (smallCoproductDesc s :
              (sigmaObj.{w, v₁, u₁}
                  fun
                    (j :
                      (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                            s) :
                        Type w)) ↦
                  Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                        (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                      (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                A) ⟶
          A) =
    (mk (A :=
        image (X :=
          sigmaObj.{w, v₁, u₁}
            fun
              (j :
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w)) ↦
            Functor.obj (C := Subobject.{v₁, u₁} A) underlying
              ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                  (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
          (smallCoproductDesc s :
            (sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
              A))
        (image.ι (smallCoproductDesc s) :
          image (X :=
              sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
              (smallCoproductDesc s :
                (sigmaObj.{w, v₁, u₁}
                    fun
                      (j :
                        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                              s) :
                          Type w)) ↦
                    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                        (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                  A) ⟶
            A)).arrow
w₁ :
  CategoryStruct.comp (Y :=
      image (X :=
        sigmaObj.{w, v₁, u₁}
          fun
            (j :
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w)) ↦
          Functor.obj (C := Subobject.{v₁, u₁} A) underlying
            ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
              (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
        (smallCoproductDesc s :
          (sigmaObj.{w, v₁, u₁}
              fun
                (j :
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w)) ↦
              Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                    (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                  (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
            A))
      (Iso.hom (underlyingIso (image.ι (smallCoproductDesc s))) :
        Functor.obj underlying
            (mk (A :=
              image (X :=
                sigmaObj.{w, v₁, u₁}
                  fun
                    (j :
                      (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                            s) :
                        Type w)) ↦
                  Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                        (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                      (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
                (smallCoproductDesc s :
                  (sigmaObj.{w, v₁, u₁}
                      fun
                        (j :
                          (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                  (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                                s) :
                            Type w)) ↦
                      Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                        ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                          (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                    A))
              (image.ι (smallCoproductDesc s) :
                image (X :=
                    sigmaObj.{w, v₁, u₁}
                      fun
                        (j :
                          (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                  (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                                s) :
                            Type w)) ↦
                      Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                        ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                          (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
                    (smallCoproductDesc s :
                      (sigmaObj.{w, v₁, u₁}
                          fun
                            (j :
                              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                      (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                                    s) :
                                Type w)) ↦
                          Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                            ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                                (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                              (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                        A) ⟶
                  A)) ⟶
          image (X :=
            sigmaObj.{w, v₁, u₁}
              fun
                (j :
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w)) ↦
              Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                    (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                  (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
            (smallCoproductDesc s :
              (sigmaObj.{w, v₁, u₁}
                  fun
                    (j :
                      (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                            s) :
                        Type w)) ↦
                  Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                        (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                      (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                A))
      (image.ι (smallCoproductDesc s) :
        image (X :=
            sigmaObj.{w, v₁, u₁}
              fun
                (j :
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w)) ↦
              Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                    (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                  (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
            (smallCoproductDesc s :
              (sigmaObj.{w, v₁, u₁}
                  fun
                    (j :
                      (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                            s) :
                        Type w)) ↦
                  Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                        (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                      (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                A) ⟶
          A) =
    (mk (A :=
        image (X :=
          sigmaObj.{w, v₁, u₁}
            fun
              (j :
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w)) ↦
            Functor.obj (C := Subobject.{v₁, u₁} A) underlying
              ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                  (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
          (smallCoproductDesc s :
            (sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
              A))
        (image.ι (smallCoproductDesc s) :
          image (X :=
              sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
              (smallCoproductDesc s :
                (sigmaObj.{w, v₁, u₁}
                    fun
                      (j :
                        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                              s) :
                          Type w)) ↦
                    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                        (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                  A) ⟶
            A)).arrow
w₂ w₃ :
  (mk (A :=
        image (X :=
          sigmaObj.{w, v₁, u₁}
            fun
              (j :
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w)) ↦
            Functor.obj (C := Subobject.{v₁, u₁} A) underlying
              ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                  (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
          (smallCoproductDesc s :
            (sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
              A))
        (image.ι (smallCoproductDesc s) :
          image (X :=
              sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
              (smallCoproductDesc s :
                (sigmaObj.{w, v₁, u₁}
                    fun
                      (j :
                        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                              s) :
                          Type w)) ↦
                    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                        (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                  A) ⟶
            A)).arrow =
    (mk (A :=
        image (X :=
          sigmaObj.{w, v₁, u₁}
            fun
              (j :
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w)) ↦
            Functor.obj (C := Subobject.{v₁, u₁} A) underlying
              ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                  (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
          (smallCoproductDesc s :
            (sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
              A))
        (image.ι (smallCoproductDesc s) :
          image (X :=
              sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
              (smallCoproductDesc s :
                (sigmaObj.{w, v₁, u₁}
                    fun
                      (j :
                        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                              s) :
                          Type w)) ↦
                    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                        (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                  A) ⟶
            A)).arrow
⊢ CategoryStruct.comp (Y :=
        image (X :=
          sigmaObj.{w, v₁, u₁}
            fun
              (j :
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w)) ↦
            Functor.obj (C := Subobject.{v₁, u₁} A) underlying
              ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                  (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
          (smallCoproductDesc s :
            (sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
              A))
        (Iso.hom (underlyingIso (image.ι (smallCoproductDesc s))) :
          Functor.obj underlying
              (mk (A :=
                image (X :=
                  sigmaObj.{w, v₁, u₁}
                    fun
                      (j :
                        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                              s) :
                          Type w)) ↦
                    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                        (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
                  (smallCoproductDesc s :
                    (sigmaObj.{w, v₁, u₁}
                        fun
                          (j :
                            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                    (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                                  s) :
                              Type w)) ↦
                        Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                          ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                            (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                      A))
                (image.ι (smallCoproductDesc s) :
                  image (X :=
                      sigmaObj.{w, v₁, u₁}
                        fun
                          (j :
                            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                    (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                                  s) :
                              Type w)) ↦
                        Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                          ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                            (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
                      (smallCoproductDesc s :
                        (sigmaObj.{w, v₁, u₁}
                            fun
                              (j :
                                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                        (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                                      s) :
                                  Type w)) ↦
                            Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                              ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                                  (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                                (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                          A) ⟶
                    A)) ⟶
            image (X :=
              sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
              (smallCoproductDesc s :
                (sigmaObj.{w, v₁, u₁}
                    fun
                      (j :
                        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                              s) :
                          Type w)) ↦
                    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                        (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                  A))
        (image.lift
            { I := Functor.obj underlying f, m := f.arrow, m_mono := ⋯,
              e :=
                Sigma.desc
                  fun
                    (b :
                      (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                            s) :
                        Type w)) ↦
                  Functor.map underlying (homOfLE ⋯),
              fac := ⋯ } :
          image (X :=
              sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
              (smallCoproductDesc s :
                (sigmaObj.{w, v₁, u₁}
                    fun
                      (j :
                        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                              s) :
                          Type w)) ↦
                    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                        (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                  A) ⟶
            MonoFactorisation.I (X :=
              sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
              (f :=
              (smallCoproductDesc s :
                (sigmaObj.{w, v₁, u₁}
                    fun
                      (j :
                        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                              s) :
                          Type w)) ↦
                    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                        (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                  A))
              ({ I := Functor.obj underlying f, m := f.arrow, m_mono := ⋯,
                  e :=
                    Sigma.desc
                      fun
                        (b :
                          (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                  (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                                s) :
                            Type w)) ↦
                      Functor.map underlying (homOfLE ⋯),
                  fac := ⋯ } :
                MonoFactorisation (X :=
                  sigmaObj.{w, v₁, u₁}
                    fun
                      (j :
                        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                              s) :
                          Type w)) ↦
                    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                        (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
                  (smallCoproductDesc s :
                    (sigmaObj.{w, v₁, u₁}
                        fun
                          (j :
                            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                    (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                                  s) :
                              Type w)) ↦
                        Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                          ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                            (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                      A))) ≫
      f.arrow =
    (mk (A :=
        image (X :=
          sigmaObj.{w, v₁, u₁}
            fun
              (j :
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w)) ↦
            Functor.obj (C := Subobject.{v₁, u₁} A) underlying
              ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                  (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
          (smallCoproductDesc s :
            (sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
              A))
        (image.ι (smallCoproductDesc s) :
          image (X :=
              sigmaObj.{w, v₁, u₁}
                fun
                  (j :
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ↦
                Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                  ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                      (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                    (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
              (smallCoproductDesc s :
                (sigmaObj.{w, v₁, u₁}
                    fun
                      (j :
                        (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                              s) :
                          Type w)) ↦
                    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                        (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
                  A) ⟶
            A)).arrow

Tactic:
rw [assoc, image.lift_fac, underlyingIso_hom_comp_eq_mk]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.image.lift_fac, CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk