-- 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
f₁ : Functor.obj underlying (sSup.{w, v₁, u₁} s) ⟶ Functor.obj underlying f
⊢ sSup.{w, v₁, u₁} s ≤ f
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)) ↦
                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 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)) ↦
                    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 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 =
  (sSup.{w, v₁, u₁} s).arrow
Tactic: fapply le_of_comm