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 : 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
i : P ≅ Q
hi : i.hom ≫ g = f
refine : ((proj S T).mapIso i).hom ≫ Hom.right g = Hom.right f
⊢ Eq (α := Subobject.{v₁, u₁} A.right)
    ((fun (P : StructuredArrow S T) (f : P ⟶ A) (hf : Mono f) ↦ Subobject.mk (Hom.right f)) P f hf)
    ((fun (P : StructuredArrow S T) (f : P ⟶ A) (hf : Mono f) ↦ Subobject.mk (Hom.right f)) Q g hg)

Tactic:
refine Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i) ?_

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.StructuredArrow.proj, CategoryTheory.Functor.mapIso
-- 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 P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ ((proj S T).mapIso i).hom ≫ Hom.right g = Hom.right f

Tactic:
congr_arg CommaMorphism.right hi

Premises used: congr_arg, CategoryTheory.CommaMorphism.right
-- 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 P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ ((proj S T).mapIso i).hom ≫ Hom.right g = Hom.right f

Tactic:
exact congr_arg CommaMorphism.right hi

Premises used: congr_arg, CategoryTheory.CommaMorphism.right
-- 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 P : StructuredArrow S T
f : P ⟶ A
inst_4 : Mono f
⊢ projectSubobject (Subobject.mk f) = Subobject.mk (Hom.right f)

Tactic:
rfl

Premises used: Quotient.liftOn', CategoryTheory.Subobject.mk, CategoryTheory.StructuredArrow.projectSubobject, rfl
-- 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 P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
⊢ (P.hom ≫ T.map (Iso.inv (Subobject.underlyingIso (Hom.right (MonoOver.mk f).arrow)))) ≫
      T.map (projectSubobject (Subobject.mk f)).arrow =
    A.hom

Tactic:
simp [← T.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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
P :
  { P : Subobject.{v₁, u₁} A.right //
    ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom }
⊢ (↑((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)
                ⋯ :
              { P : Subobject.{v₁, u₁} A.right //
                ∃ (q : S ⟶ T.obj (Functor.obj Subobject.underlying P)), q ≫ T.map P.arrow = A.hom }))
          ((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) ⋯)
            P)) :
      Subobject A.right) =
    (↑P : Subobject A.right)

Tactic:
simp only [liftSubobject, homMk_right, projectSubobject_mk,
      Subobject.mk_arrow]

Premises used: CategoryTheory.StructuredArrow.projectSubobject_mk, CategoryTheory.StructuredArrow.liftSubobject, CategoryTheory.Subobject.mk_arrow, CategoryTheory.StructuredArrow.homMk_right
-- 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 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

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

Premises used: CategoryTheory.Subobject.mk_le_mk_of_comm, Iff.intro
-- 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 P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
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)
                ⋯,
            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 })
⊢ (P.hom ≫ T.map (Subobject.ofMkLEMk (Hom.right (MonoOver.mk f).arrow) (Hom.right (MonoOver.mk g).arrow) h)) ≫
      T.map (Hom.right g) =
    Q.hom ≫ T.map (Hom.right g)

Tactic:
simp [← T.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
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)
                ⋯,
            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 })
⊢ P ⟶ Q

Tactic:
exact homMk (Subobject.ofMkLEMk _ _ h)
        ((cancel_mono (T.map g.right)).1 (by simp [← T.map_comp]))

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, Iff.mp, CategoryTheory.Subobject.ofMkLEMk, CategoryTheory.StructuredArrow.Hom.right
-- 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 P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
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)
                ⋯,
            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 })
⊢ homMk (Subobject.ofMkLEMk (Hom.right (MonoOver.mk f).arrow) (Hom.right (MonoOver.mk g).arrow) h) ⋯ ≫ g = f

Tactic:
simp
-- 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 P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk 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 })

Tactic:
Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).right ?_

Premises used: Quotient.liftOn', CategoryTheory.Subobject.lift, CategoryTheory.Subobject.mk_le_mk_of_comm, CategoryTheory.Subobject.mk, CategoryTheory.StructuredArrow.projectSubobject, Quotient.mk', CategoryTheory.Subobject.ofMkLEMk, CategoryTheory.StructuredArrow.Hom.right
-- 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 P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
h₁ : Hom.right (Subobject.ofMkLEMk f g h) ≫ Hom.right (MonoOver.mk g).arrow = Hom.right (MonoOver.mk f).arrow
⊢ 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 })

Tactic:
refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).right ?_

Premises used: CategoryTheory.Subobject.mk_le_mk_of_comm, CategoryTheory.Subobject.ofMkLEMk, CategoryTheory.StructuredArrow.Hom.right
-- 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 P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Hom.right (Subobject.ofMkLEMk f g h) ≫ Hom.right (MonoOver.mk g).arrow = Hom.right (MonoOver.mk f).arrow

Tactic:
congr_arg CommaMorphism.right (Subobject.ofMkLEMk_comp h)

Premises used: CategoryTheory.Subobject.ofMkLEMk_comp, congr_arg, CategoryTheory.CommaMorphism.right
-- 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 P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Hom.right (Subobject.ofMkLEMk f g h) ≫ Hom.right (MonoOver.mk g).arrow = Hom.right (MonoOver.mk f).arrow

Tactic:
exact congr_arg CommaMorphism.right (Subobject.ofMkLEMk_comp h)

Premises used: CategoryTheory.Subobject.ofMkLEMk_comp, congr_arg, CategoryTheory.CommaMorphism.right
-- 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
refine :
  ∀ ⦃A_1 B : (CostructuredArrow S T)ᵒᵖ⦄ (f : A_1 ⟶ op A) (g : B ⟶ op A) [inst_4 : Mono f] [inst_5 : Mono g]
    (i : A_1 ≅ B),
    i.hom ≫ g = f →
      Eq (α := Subobject.{v₁, u₁} (op A.left))
        ((fun (P : (CostructuredArrow S T)ᵒᵖ) (f : P ⟶ op A) (hf : Mono f) ↦
            (Subobject.mk f.unop.left.op : Subobject.{v₁, u₁} (op A.left)))
          A_1 f inst_4)
        ((fun (P : (CostructuredArrow S T)ᵒᵖ) (f : P ⟶ op A) (hf : Mono f) ↦
            (Subobject.mk f.unop.left.op : Subobject.{v₁, u₁} (op A.left)))
          B g inst_5)
⊢ Subobject (op A) → Subobject.{v₁, u₁} (op A.left)

Tactic:
refine Subobject.lift (fun P f hf => Subobject.mk f.unop.left.op) ?_
-- 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
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ Eq (α := Subobject.{v₁, u₁} (op A.left))
    ((fun (P : (CostructuredArrow S T)ᵒᵖ) (f : P ⟶ op A) (hf : Mono f) ↦
        (Subobject.mk f.unop.left.op : Subobject.{v₁, u₁} (op A.left)))
      P f hf)
    ((fun (P : (CostructuredArrow S T)ᵒᵖ) (f : P ⟶ op A) (hf : Mono f) ↦
        (Subobject.mk f.unop.left.op : Subobject.{v₁, u₁} (op A.left)))
      Q g hg)

Tactic:
Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i.unop).op (Quiver.Hom.unop_inj ?_)

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.Iso.op, Quiver.Hom.unop_inj, CategoryTheory.Functor.mapIso, CategoryTheory.Iso.unop, CategoryTheory.CostructuredArrow.proj
-- 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
i : P ≅ Q
hi : i.hom ≫ g = f
refine : (((proj S T).mapIso i.unop).op.hom ≫ g.unop.left.op).unop = f.unop.left.op.unop
⊢ Eq (α := Subobject.{v₁, u₁} (op A.left))
    ((fun (P : (CostructuredArrow S T)ᵒᵖ) (f : P ⟶ op A) (hf : Mono f) ↦
        (Subobject.mk f.unop.left.op : Subobject.{v₁, u₁} (op A.left)))
      P f hf)
    ((fun (P : (CostructuredArrow S T)ᵒᵖ) (f : P ⟶ op A) (hf : Mono f) ↦
        (Subobject.mk f.unop.left.op : Subobject.{v₁, u₁} (op A.left)))
      Q g hg)

Tactic:
refine Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i.unop).op (Quiver.Hom.unop_inj ?_)

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.Iso.op, Quiver.Hom.unop_inj, CategoryTheory.Functor.mapIso, CategoryTheory.Iso.unop, CategoryTheory.CostructuredArrow.proj
-- 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
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ (i.hom ≫ g).unop = f.unop

Tactic:
have := congr_arg Quiver.Hom.unop hi