-- Module: Mathlib.CategoryTheory.Subobject.Comma
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : HasFiniteColimits.{v₁, u₁} C
inst_3 : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h :
  (h :
      LE.le (α :=
        { P : Subobject.{v₁, u₁} (op A.left) //
          ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
        (({
                toFun := fun (P : Subobject (op A)) ↦
                  Subtype.mk (p := fun (P : Subobject.{v₁, u₁} (op A.left)) ↦
                    ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom)
                    (projectQuotient P) ⋯,
                invFun :=
                  fun
                    (P :
                      { P : Subobject.{v₁, u₁} (op A.left) //
                        ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T),
                          S.map P.arrow.unop ≫ q = A.hom }) ↦
                  liftQuotient (↑P : Subobject (op A.left)) ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : Subobject (op A)) →
                { P : Subobject (op A.left) //
                  ∃ (q : S.obj (unop (Subobject.underlying.obj P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
            (Subobject.mk f) :
          { P : Subobject.{v₁, u₁} (op A.left) //
            ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
        (({
                toFun := fun (P : Subobject (op A)) ↦
                  Subtype.mk (p := fun (P : Subobject.{v₁, u₁} (op A.left)) ↦
                    ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom)
                    (projectQuotient P) ⋯,
                invFun :=
                  fun
                    (P :
                      { P : Subobject.{v₁, u₁} (op A.left) //
                        ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T),
                          S.map P.arrow.unop ≫ q = A.hom }) ↦
                  liftQuotient (↑P : Subobject (op A.left)) ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : Subobject (op A)) →
                { P : Subobject (op A.left) //
                  ∃ (q : S.obj (unop (Subobject.underlying.obj P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
            (Subobject.mk g) :
          { P : Subobject.{v₁, u₁} (op A.left) //
            ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })) →
    P ⟶ Q
h₁ :
  ∀
    (h :
      LE.le (α :=
        { P : Subobject.{v₁, u₁} (op A.left) //
          ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
        (({
                toFun := fun (P : Subobject (op A)) ↦
                  Subtype.mk (p := fun (P : Subobject.{v₁, u₁} (op A.left)) ↦
                    ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom)
                    (projectQuotient P) ⋯,
                invFun :=
                  fun
                    (P :
                      { P : Subobject.{v₁, u₁} (op A.left) //
                        ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T),
                          S.map P.arrow.unop ≫ q = A.hom }) ↦
                  liftQuotient (↑P : Subobject (op A.left)) ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : Subobject (op A)) →
                { P : Subobject (op A.left) //
                  ∃ (q : S.obj (unop (Subobject.underlying.obj P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
            (Subobject.mk f) :
          { P : Subobject.{v₁, u₁} (op A.left) //
            ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
        (({
                toFun := fun (P : Subobject (op A)) ↦
                  Subtype.mk (p := fun (P : Subobject.{v₁, u₁} (op A.left)) ↦
                    ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom)
                    (projectQuotient P) ⋯,
                invFun :=
                  fun
                    (P :
                      { P : Subobject.{v₁, u₁} (op A.left) //
                        ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T),
                          S.map P.arrow.unop ≫ q = A.hom }) ↦
                  liftQuotient (↑P : Subobject (op A.left)) ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : Subobject (op A)) →
                { P : Subobject (op A.left) //
                  ∃ (q : S.obj (unop (Subobject.underlying.obj P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
            (Subobject.mk g) :
          { P : Subobject.{v₁, u₁} (op A.left) //
            ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })),
    (homMk (Subobject.ofMkLEMk (MonoOver.mk f).arrow.unop.left.op (MonoOver.mk g).arrow.unop.left.op h).unop ⋯).op ≫ g =
      f
h₂ :
  ∀ (h : Subobject.mk f ≤ Subobject.mk g),
    LE.le (α :=
      { P : Subobject.{v₁, u₁} (op A.left) //
        ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
      (({
              toFun := fun (P : Subobject (op A)) ↦
                Subtype.mk (p := fun (P : Subobject.{v₁, u₁} (op A.left)) ↦
                  ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom)
                  (projectQuotient P) ⋯,
              invFun :=
                fun
                  (P :
                    { P : Subobject.{v₁, u₁} (op A.left) //
                      ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom }) ↦
                liftQuotient (↑P : Subobject (op A.left)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subobject (op A)) →
              { P : Subobject (op A.left) //
                ∃ (q : S.obj (unop (Subobject.underlying.obj P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
          (Subobject.mk f) :
        { P : Subobject.{v₁, u₁} (op A.left) //
          ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
      (({
              toFun := fun (P : Subobject (op A)) ↦
                Subtype.mk (p := fun (P : Subobject.{v₁, u₁} (op A.left)) ↦
                  ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom)
                  (projectQuotient P) ⋯,
              invFun :=
                fun
                  (P :
                    { P : Subobject.{v₁, u₁} (op A.left) //
                      ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom }) ↦
                liftQuotient (↑P : Subobject (op A.left)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subobject (op A)) →
              { P : Subobject (op A.left) //
                ∃ (q : S.obj (unop (Subobject.underlying.obj P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
          (Subobject.mk g) :
        { P : Subobject.{v₁, u₁} (op A.left) //
          ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
⊢ LE.le (α :=
      { P : Subobject.{v₁, u₁} (op A.left) //
        ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
      (({
              toFun := fun (P : Subobject (op A)) ↦
                Subtype.mk (p := fun (P : Subobject.{v₁, u₁} (op A.left)) ↦
                  ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom)
                  (projectQuotient P) ⋯,
              invFun :=
                fun
                  (P :
                    { P : Subobject.{v₁, u₁} (op A.left) //
                      ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom }) ↦
                liftQuotient (↑P : Subobject (op A.left)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subobject (op A)) →
              { P : Subobject (op A.left) //
                ∃ (q : S.obj (unop (Subobject.underlying.obj P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
          (Subobject.mk f) :
        { P : Subobject.{v₁, u₁} (op A.left) //
          ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
      (({
              toFun := fun (P : Subobject (op A)) ↦
                Subtype.mk (p := fun (P : Subobject.{v₁, u₁} (op A.left)) ↦
                  ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom)
                  (projectQuotient P) ⋯,
              invFun :=
                fun
                  (P :
                    { P : Subobject.{v₁, u₁} (op A.left) //
                      ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom }) ↦
                liftQuotient (↑P : Subobject (op A.left)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subobject (op A)) →
              { P : Subobject (op A.left) //
                ∃ (q : S.obj (unop (Subobject.underlying.obj P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom })
          (Subobject.mk g) :
        { P : Subobject.{v₁, u₁} (op A.left) //
          ∃ (q : S.obj (unop (Functor.obj Subobject.underlying P)) ⟶ T), S.map P.arrow.unop ≫ q = A.hom }) ↔
    Subobject.mk f ≤ Subobject.mk g

Tactic:
refine ⟨fun h => Subobject.mk_le_mk_of_comm ?_ ?_, fun h => ?_⟩