-- 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
⊢ 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)
have 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 sorry)) ≫
          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)
Tactic: ext