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

Tactic:
fapply le_of_comm

Premises used: CategoryTheory.Subobject.le_of_comm