awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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 })
h₁ :
  S.map g.unop.left ≫
      S.map (Subobject.ofMkLEMk (MonoOver.mk f).arrow.unop.left.op (MonoOver.mk g).arrow.unop.left.op h).unop ≫
        (unop (MonoOver.mk f).obj (P := Over.isMono (op A)).left).hom =
    S.map g.unop.left ≫ (unop (MonoOver.mk g).obj (P := Over.isMono (op A)).left).hom
⊢ P ⟶ Q

Tactic:
refine (homMk (Subobject.ofMkLEMk _ _ h).unop ((cancel_epi (S.map g.unop.left)).1 ?_)).op

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Functor.map, CategoryTheory.CommaMorphism.left, Iff.mp, CategoryTheory.Subobject.ofMkLEMk, CategoryTheory.cancel_epi
-- 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 :
  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 })
h₁ :
  S.map g.unop.left ≫ S.map (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop ≫ (unop P).hom =
    S.map g.unop.left ≫ (unop Q).hom
⊢ S.map g.unop.left ≫
      S.map (Subobject.ofMkLEMk (MonoOver.mk f).arrow.unop.left.op (MonoOver.mk g).arrow.unop.left.op h).unop ≫
        (unop (MonoOver.mk f).obj (P := Over.isMono (op A)).left).hom =
    S.map g.unop.left ≫ (unop (MonoOver.mk g).obj (P := Over.isMono (op A)).left).hom

Tactic:
dsimp
-- 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 :
  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 })
⊢ S.map g.unop.left ≫ S.map (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop ≫ (unop P).hom =
    S.map g.unop.left ≫ (unop Q).hom

Tactic:
simp only [← S.map_comp_assoc, unop_left_comp_ofMkLEMk_unop, unop_op, CommaMorphism.w,
        Functor.const_obj_obj, right_eq_id, Functor.const_obj_map, Category.comp_id]

Premises used: CategoryTheory.CostructuredArrow.unop_left_comp_ofMkLEMk_unop, CategoryTheory.CommaMorphism.w, CategoryTheory.Category.comp_id, CategoryTheory.CostructuredArrow.right_eq_id, CategoryTheory.Functor.map_comp_assoc, Opposite.unop_op, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map
-- 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 :
  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 })
h₁ :
  ((homMk (Subobject.ofMkLEMk (MonoOver.mk f).arrow.unop.left.op (MonoOver.mk g).arrow.unop.left.op h).unop ⋯).op ≫
        g).unop =
    f.unop
⊢ (homMk (Subobject.ofMkLEMk (MonoOver.mk f).arrow.unop.left.op (MonoOver.mk g).arrow.unop.left.op h).unop ⋯).op ≫ g = f

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- 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 :
  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 })
h₁ :
  ((homMk (Subobject.ofMkLEMk (MonoOver.mk f).arrow.unop.left.op (MonoOver.mk g).arrow.unop.left.op h).unop ⋯).op ≫
          g).unop.left =
    f.unop.left
⊢ ((homMk (Subobject.ofMkLEMk (MonoOver.mk f).arrow.unop.left.op (MonoOver.mk g).arrow.unop.left.op h).unop ⋯).op ≫
        g).unop =
    f.unop

Tactic:
ext
-- 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 :
  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).unop.left =
    f.unop.left

Tactic:
unop_left_comp_ofMkLEMk_unop _

Premises used: CategoryTheory.CostructuredArrow.unop_left_comp_ofMkLEMk_unop, Quiver.Hom.unop
-- 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 :
  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).unop.left =
    f.unop.left

Tactic:
exact unop_left_comp_ofMkLEMk_unop _

Premises used: CategoryTheory.CostructuredArrow.unop_left_comp_ofMkLEMk_unop
-- 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 : 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 })

Tactic:
Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).unop.left.op ?_

Premises used: Quotient.liftOn', Quiver.Hom.op, CategoryTheory.Subobject.lift, CategoryTheory.Subobject.mk_le_mk_of_comm, Quiver.Hom.unop, CategoryTheory.CostructuredArrow.projectQuotient, CategoryTheory.Subobject.mk, CategoryTheory.CommaMorphism.left, Quotient.mk', CategoryTheory.Subobject.ofMkLEMk