-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Comma (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasFiniteLimits.{v₁, u₁} C
inst_3 : PreservesFiniteLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
⊢ LE.le (α :=
      { P : Subobject.{v₁, u₁} A.right //
        ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom })
      (({
              toFun := fun (P : Subobject A) ↦
                Subtype.mk (p := fun (P : Subobject.{v₁, u₁} A.right) ↦
                  ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom)
                  (projectSubobject P) ⋯,
              invFun :=
                fun
                  (P :
                    { P : Subobject.{v₁, u₁} A.right //
                      ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom }) ↦
                liftSubobject (↑P : Subobject A.right) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subobject A) →
              { P : Subobject A.right // ∃ (q : S ⟶ T.obj (Subobject.underlying.obj P)), q ≫ T.map P.arrow = A.hom })
          (Subobject.mk f) :
        { P : Subobject.{v₁, u₁} A.right //
          ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom })
      (({
              toFun := fun (P : Subobject A) ↦
                Subtype.mk (p := fun (P : Subobject.{v₁, u₁} A.right) ↦
                  ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom)
                  (projectSubobject P) ⋯,
              invFun :=
                fun
                  (P :
                    { P : Subobject.{v₁, u₁} A.right //
                      ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom }) ↦
                liftSubobject (↑P : Subobject A.right) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subobject A) →
              { P : Subobject A.right // ∃ (q : S ⟶ T.obj (Subobject.underlying.obj P)), q ≫ T.map P.arrow = A.hom })
          (Subobject.mk g) :
        { P : Subobject.{v₁, u₁} A.right //
          ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom }) ↔
    Subobject.mk f ≤ Subobject.mk g
have h : (h :
    LE.le (α :=
      { P : Subobject.{v₁, u₁} A.right //
        ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom })
      (({
              toFun := fun (P : Subobject A) ↦
                Subtype.mk (p := fun (P : Subobject.{v₁, u₁} A.right) ↦
                  ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom)
                  (projectSubobject P) sorry,
              invFun :=
                fun
                  (P :
                    { P : Subobject.{v₁, u₁} A.right //
                      ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom }) ↦
                liftSubobject (↑P : Subobject A.right) sorry,
              left_inv := sorry, right_inv := sorry } :
            (a : Subobject A) →
              { P : Subobject A.right // ∃ (q : S ⟶ T.obj (Subobject.underlying.obj P)), q ≫ T.map P.arrow = A.hom })
          (Subobject.mk f) :
        { P : Subobject.{v₁, u₁} A.right //
          ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom })
      (({
              toFun := fun (P : Subobject A) ↦
                Subtype.mk (p := fun (P : Subobject.{v₁, u₁} A.right) ↦
                  ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom)
                  (projectSubobject P) sorry,
              invFun :=
                fun
                  (P :
                    { P : Subobject.{v₁, u₁} A.right //
                      ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom }) ↦
                liftSubobject (↑P : Subobject A.right) sorry,
              left_inv := sorry, right_inv := sorry } :
            (a : Subobject A) →
              { P : Subobject A.right // ∃ (q : S ⟶ T.obj (Subobject.underlying.obj P)), q ≫ T.map P.arrow = A.hom })
          (Subobject.mk g) :
        { P : Subobject.{v₁, u₁} A.right //
          ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom })) →
  P ⟶ Q
Tactic: refine ⟨fun h => Subobject.mk_le_mk_of_comm ?_ ?_, fun h => ?_⟩