-- Module: Mathlib.CategoryTheory.Subobject.Comma
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 : StructuredArrow S T
h :
  ∀ ⦃A_1 B : StructuredArrow S T⦄ (f : A_1 ⟶ A) (g : B ⟶ A) [inst_4 : Mono f] [inst_5 : 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
⊢ ∀ {a b : Subobject A},
    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 })
            a :
          { 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 })
            b :
          { P : Subobject.{v₁, u₁} A.right //
            ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom }) ↔
      a ≤ b

Tactic:
apply Subobject.ind₂

Premises used: CategoryTheory.Subobject.ind₂