-- 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
hf : f ∈ s
⊢ 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)
                  ⋯) :
              Shrink.{w, max u₁ v₁} (Subobject A))))
        (eqToHom ⋯)
        (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) ⋯ :
                { 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)
                          ⋯) :
                      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:
simp [sSup, smallCoproductDesc]

Premises used: CategoryTheory.Subobject.sSup, CategoryTheory.Subobject.smallCoproductDesc