-- 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₁ :
  ∀
    (b :
      (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
        Type w)),
    Eq (α :=
      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)
            (↑b : Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
        A)
      (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₁} (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
                ((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))))
            b)
          ((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 ⋯)) ≫
            f.arrow) :
        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)
              (↑b : Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
          A)
      (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₁} (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
                  ((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))))
              b :
            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)
                  (↑b : Shrink.{w, max u₁ v₁} (Subobject 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))))
          (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 (C := Subobject.{v₁, u₁} A) underlying
            ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
              (↑b : Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
          A)
⊢ Eq (α :=
    (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)
    ((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 ⋯)) ≫
        f.arrow :
      (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)
    (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)

Tactic:
ext