-- 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
hf : f ∈ s
f₁ : Functor.obj underlying f ⟶ Functor.obj underlying (sSup.{w, v₁, u₁} s)
⊢ f ≤ sSup.{w, v₁, u₁} s
have w : CategoryStruct.comp (Y :=
      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)
          (↑(Subtype.mk (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)
                ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f) sorry) :
            Shrink.{w, max u₁ v₁} (Subobject A))))
      (eqToHom sorry)
      (CategoryStruct.comp (Y :=
        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))))
        (Sigma.ι.{w, v₁, u₁} (β :=
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w))
            (C := C)
            (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 : Subobject.{v₁, u₁} A ⥤ C)
                ((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)) :
                  Subobject.{v₁, u₁} A))
            (Subtype.mk (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)
                ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f) sorry :
              { 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 }) :
          Quiver.Hom.{v₁, u₁} (V := C)
            (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)
                  (↑(Subtype.mk (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)
                        ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A))
                          f)
                        sorry) :
                    Shrink.{w, max u₁ v₁} (Subobject A))) :
              C)
            (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))) :
              C))
        (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))
            (factorThruImage (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)))) ⟶
                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.inv (underlyingIso (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) ⟶
                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))) :
          (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)))) ⟶
            Functor.obj underlying (sSup.{w, v₁, u₁} s))) ≫
    (sSup.{w, v₁, u₁} s).arrow =
  f.arrow
Tactic: fapply le_of_comm