-- 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
f₁ :
  (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 f
⊢ Functor.obj underlying (sSup.{w, v₁, u₁} s) ⟶ Functor.obj underlying f
have 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 sorry)) ≫
      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: refine (underlyingIso _).hom ≫ image.lift ⟨_, f.arrow, ?_, ?_⟩