-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
⊢ 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)) ↦
                  Subtype.casesOn (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
                    Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                      ((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s)
                      x)
                    (motive :=
                    fun
                      (x :
                        (↑((⇑(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)
                          (↑x : Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
                      Functor.obj underlying f)
                    b
                    fun (g : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A))
                      (m :
                        Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                          ((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                            s)
                          g) ↦
                    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)) ↦
                      Subtype.casesOn (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
                        Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                          ((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                              (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                            s)
                          x)
                        (motive :=
                        fun
                          (x :
                            (↑((⇑(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)
                              (↑x : Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
                          Functor.obj underlying f)
                        b
                        fun (g : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A))
                          (m :
                            Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                              ((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                                  (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                                s)
                              g) ↦
                        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 =
    (sSup.{w, v₁, u₁} s).arrow
have 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 := sorry,
            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 sorry),
            fac := sorry } :
        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 := sorry,
                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 sorry),
                fac := sorry } :
              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: dsimp [sSup]