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
i : P ≅ Q
hi : i.hom ≫ g = f
this : (i.hom ≫ g).unop = f.unop
⊢ (((proj S T).mapIso i.unop).op.hom ≫ g.unop.left.op).unop = f.unop.left.op.unop

Tactic:
simpa using congr_arg CommaMorphism.left this

Premises used: congr_arg, CategoryTheory.CommaMorphism.left
-- 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 : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst_4 : Mono f
⊢ projectQuotient (Subobject.mk f) = Subobject.mk f.unop.left.op

Tactic:
rfl

Premises used: Quotient.liftOn', CategoryTheory.CostructuredArrow.projectQuotient, CategoryTheory.Subobject.mk, 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 : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : HasFiniteColimits.{v₁, u₁} C
inst_3 : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
dsimp :
  CategoryStruct.comp (Y :=
      S.obj
        (unop (Functor.obj (C := Subobject.{v₁, u₁} (op A.left)) Subobject.underlying (Subobject.mk f.unop.left.op))))
      (S.map (Quiver.Hom.unop (Subobject.arrow (Subobject.mk f.unop.left.op))))
      (S.map (Quiver.Hom.unop (Iso.inv (Subobject.underlyingIso f.unop.left.op))) ≫ (unop P).hom) =
    A.hom
⊢ S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫
      S.map (Iso.inv (Iso.unop (Subobject.underlyingIso (MonoOver.mk f).arrow.unop.left.op))) ≫ (unop P).hom =
    A.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 : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
rw :
  S.map
        (Quiver.Hom.unop
          (CategoryStruct.comp (Y :=
            Functor.obj (C := Subobject.{v₁, u₁} (op A.left)) Subobject.underlying (Subobject.mk f.unop.left.op))
            (Iso.inv (Subobject.underlyingIso f.unop.left.op)) (Subobject.arrow (Subobject.mk f.unop.left.op)))) ≫
      (unop P).hom =
    A.hom
⊢ CategoryStruct.comp (Y :=
      S.obj
        (unop (Functor.obj (C := Subobject.{v₁, u₁} (op A.left)) Subobject.underlying (Subobject.mk f.unop.left.op))))
      (S.map (Quiver.Hom.unop (Subobject.arrow (Subobject.mk f.unop.left.op))))
      (S.map (Quiver.Hom.unop (Iso.inv (Subobject.underlyingIso f.unop.left.op))) ≫ (unop P).hom) =
    A.hom

Tactic:
rw [← Category.assoc, ← S.map_comp, ← unop_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.unop_comp, 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 : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : HasFiniteColimits.{v₁, u₁} C
inst_3 : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map
        (Quiver.Hom.unop
          (CategoryStruct.comp (Y :=
            Functor.obj (C := Subobject.{v₁, u₁} (op A.left)) Subobject.underlying (Subobject.mk f.unop.left.op))
            (Iso.inv (Subobject.underlyingIso f.unop.left.op)) (Subobject.arrow (Subobject.mk f.unop.left.op)))) ≫
      (unop P).hom =
    A.hom

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 : Functor.{v₁, v₂, u₁, u₂} C D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst_2 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop P).left) (Y := op (unop (op A)).left) f.unop.left.op
a : f.unop.left
a₁ : Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op))
| f.unop.left ≫ Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op))

Tactic:
congr
-- 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
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst_2 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop P).left) (Y := op (unop (op A)).left) f.unop.left.op
a : f.unop.left.op.unop
| f.unop.left

Tactic:
rw [← Quiver.Hom.unop_op f.unop.left]

Premises used: Quiver.Hom.unop_op, Quiver.Hom.unop, CategoryTheory.CommaMorphism.left
-- 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
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst_2 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop P).left) (Y := op (unop (op A)).left) f.unop.left.op
a : f.unop.left.op.unop
a₁ : Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op))
| f.unop.left ≫ Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op))

Tactic:
congr
    rw [← Quiver.Hom.unop_op f.unop.left]

Premises used: Quiver.Hom.unop_op, Quiver.Hom.unop, CategoryTheory.CommaMorphism.left
-- 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
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst_2 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop P).left) (Y := op (unop (op A)).left) f.unop.left.op
conv_lhs :
  Eq (α :=
    (unop (op A)).left ⟶
      unop
        (Functor.obj (C := Subobject.{v₁, u₁} (op (unop (op A)).left)) Subobject.underlying
          (Subobject.mk f.unop.left.op)))
    (f.unop.left.op.unop ≫ Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op)))
    (Quiver.Hom.unop (Subobject.arrow (Subobject.mk f.unop.left.op)))
⊢ Eq (α :=
    (unop (op A)).left ⟶
      unop
        (Functor.obj (C := Subobject.{v₁, u₁} (op (unop (op A)).left)) Subobject.underlying
          (Subobject.mk f.unop.left.op)))
    (f.unop.left ≫ Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op)))
    (Quiver.Hom.unop (Subobject.arrow (Subobject.mk f.unop.left.op)))

Tactic:
conv_lhs =>
    congr
    rw [← Quiver.Hom.unop_op f.unop.left]

Premises used: Quiver.Hom.unop_op, Quiver.Hom.unop, CategoryTheory.CommaMorphism.left
-- 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
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst_2 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop P).left) (Y := op (unop (op A)).left) f.unop.left.op
rw :
  Eq.{v₁ + 1} (α :=
    (unop (op A)).left ⟶
      unop
        (Functor.obj (C := Subobject.{v₁, u₁} (op (unop (op A)).left)) Subobject.underlying
          (Subobject.mk f.unop.left.op)))
    (Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op) ≫ f.unop.left.op) :
      unop (op (unop (op A)).left) ⟶
        unop
          (Functor.obj (C := Subobject.{v₁, u₁} (op (unop (op A)).left)) Subobject.underlying
            (Subobject.mk f.unop.left.op)))
    (Quiver.Hom.unop (Subobject.arrow (Subobject.mk f.unop.left.op)))
rw₁ rw₂ :
  Eq.{v₁ + 1} (α :=
    (unop (op A)).left ⟶
      unop
        (Functor.obj (C := Subobject.{v₁, u₁} (op (unop (op A)).left)) Subobject.underlying
          (Subobject.mk f.unop.left.op)))
    (Quiver.Hom.unop (Subobject.arrow (Subobject.mk f.unop.left.op)) :
      unop (op (unop (op A)).left) ⟶
        unop
          (Functor.obj (C := Subobject.{v₁, u₁} (op (unop (op A)).left)) Subobject.underlying
            (Subobject.mk f.unop.left.op)))
    (Quiver.Hom.unop (Subobject.arrow (Subobject.mk f.unop.left.op)))
⊢ Eq (α :=
    (unop (op A)).left ⟶
      unop
        (Functor.obj (C := Subobject.{v₁, u₁} (op (unop (op A)).left)) Subobject.underlying
          (Subobject.mk f.unop.left.op)))
    (f.unop.left.op.unop ≫ Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op)))
    (Quiver.Hom.unop (Subobject.arrow (Subobject.mk f.unop.left.op)))

Tactic:
rw [← unop_comp, Subobject.underlyingIso_hom_comp_eq_mk]

Premises used: CategoryTheory.unop_comp, CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk
-- 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 : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Functor.obj Subobject.underlying (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
i : op (mk q) ≅ P
w :
  Eq (α := op (mk q) ⟶ op A) (Iso.hom (Iso.op (isoMk (Iso.unop (Subobject.underlyingIso f.unop.left.op)) ⋯)) ≫ f)
    (Quiver.Hom.op (homMk (projectQuotient (Subobject.mk f)).arrow.unop hq))
⊢ liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f

Tactic:
fapply Subobject.mk_eq_mk_of_comm

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm
-- 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 : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Functor.obj Subobject.underlying (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
i : (unop P).left ≅ (mk q).left
i₁ : S.map (Iso.hom (Iso.unop (Subobject.underlyingIso f.unop.left.op))) ≫ (mk q).hom = (unop P).hom
⊢ op (mk q) ≅ P

Tactic:
refine (Iso.op (isoMk ?_ ?_) : _ ≅ op (unop P))

Premises used: CategoryTheory.Iso.op, CategoryTheory.CostructuredArrow.isoMk
-- 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 : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Functor.obj Subobject.underlying (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ (unop P).left ≅ (mk q).left

Tactic:
exact (Subobject.underlyingIso f.unop.left.op).unop

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Subobject.underlyingIso, CategoryTheory.CommaMorphism.left, CategoryTheory.Iso.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 : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Functor.obj Subobject.underlying (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ S.map (Iso.hom (Iso.unop (Subobject.underlyingIso f.unop.left.op))) ≫ (mk q).hom = (unop P).hom

Tactic:
(cancel_epi (S.map f.unop.left)).1 ?_

Premises used: Quiver.Hom.unop, CategoryTheory.Functor.map, CategoryTheory.CommaMorphism.left, Iff.mp, 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 : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Functor.obj Subobject.underlying (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
i :
  S.map f.unop.left ≫ S.map (Iso.hom (Iso.unop (Subobject.underlyingIso f.unop.left.op))) ≫ (mk q).hom =
    S.map f.unop.left ≫ (unop P).hom
⊢ S.map (Iso.hom (Iso.unop (Subobject.underlyingIso f.unop.left.op))) ≫ (mk q).hom = (unop P).hom

Tactic:
refine (cancel_epi (S.map f.unop.left)).1 ?_

Premises used: Quiver.Hom.unop, CategoryTheory.Functor.map, CategoryTheory.CommaMorphism.left, Iff.mp, 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 : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Functor.obj Subobject.underlying (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ S.map f.unop.left ≫ S.map (Iso.hom (Iso.unop (Subobject.underlyingIso f.unop.left.op))) ≫ (mk q).hom =
    S.map f.unop.left ≫ (unop P).hom

Tactic:
simpa [← Category.assoc, ← S.map_comp] using hq

Premises used: CategoryTheory.Category.assoc, 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 : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : HasFiniteColimits.{v₁, u₁} C
inst_3 : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Functor.obj Subobject.underlying (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ Eq (α := unop (op A) ⟶ unop (op (mk q)))
    (Quiver.Hom.unop (Iso.hom (Iso.op (isoMk (Iso.unop (Subobject.underlyingIso f.unop.left.op)) ⋯)) ≫ f))
    (Quiver.Hom.unop (Quiver.Hom.op (homMk (projectQuotient (Subobject.mk f)).arrow.unop hq)))

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 : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : HasFiniteColimits.{v₁, u₁} C
inst_3 : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Functor.obj Subobject.underlying (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ Eq (α := op (mk q) ⟶ op A) (Iso.hom (Iso.op (isoMk (Iso.unop (Subobject.underlyingIso f.unop.left.op)) ⋯)) ≫ f)
    (Quiver.Hom.op (homMk (projectQuotient (Subobject.mk f)).arrow.unop hq))

Tactic:
exact Quiver.Hom.unop_inj (by simp)

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
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst_2 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop P).left) (Y := op (unop (op A)).left) f.unop.left.op
inst_3 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop Q).left) (Y := op (unop (op A)).left) g.unop.left.op
h : LE.le (α := Subobject.{v₁, u₁} (op (unop (op A)).left)) (Subobject.mk f.unop.left.op) (Subobject.mk g.unop.left.op)
a : g.unop.left
a₁ : (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop
| g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop

Tactic:
congr
-- 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
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst_2 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop P).left) (Y := op (unop (op A)).left) f.unop.left.op
inst_3 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop Q).left) (Y := op (unop (op A)).left) g.unop.left.op
h : LE.le (α := Subobject.{v₁, u₁} (op (unop (op A)).left)) (Subobject.mk f.unop.left.op) (Subobject.mk g.unop.left.op)
a : g.unop.left.op.unop
| g.unop.left

Tactic:
rw [← Quiver.Hom.unop_op g.unop.left]

Premises used: Quiver.Hom.unop_op, Quiver.Hom.unop, CategoryTheory.CommaMorphism.left
-- 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
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst_2 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop P).left) (Y := op (unop (op A)).left) f.unop.left.op
inst_3 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop Q).left) (Y := op (unop (op A)).left) g.unop.left.op
h : LE.le (α := Subobject.{v₁, u₁} (op (unop (op A)).left)) (Subobject.mk f.unop.left.op) (Subobject.mk g.unop.left.op)
a : g.unop.left.op.unop
a₁ : (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop
| g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop

Tactic:
congr
    rw [← Quiver.Hom.unop_op g.unop.left]

Premises used: Quiver.Hom.unop_op, Quiver.Hom.unop, CategoryTheory.CommaMorphism.left
-- 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
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst_2 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop P).left) (Y := op (unop (op A)).left) f.unop.left.op
inst_3 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop Q).left) (Y := op (unop (op A)).left) g.unop.left.op
h : LE.le (α := Subobject.{v₁, u₁} (op (unop (op A)).left)) (Subobject.mk f.unop.left.op) (Subobject.mk g.unop.left.op)
conv_lhs : g.unop.left.op.unop ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left
⊢ g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left

Tactic:
conv_lhs =>
    congr
    rw [← Quiver.Hom.unop_op g.unop.left]

Premises used: Quiver.Hom.unop_op, Quiver.Hom.unop, CategoryTheory.CommaMorphism.left
-- 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
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst_2 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop P).left) (Y := op (unop (op A)).left) f.unop.left.op
inst_3 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop Q).left) (Y := op (unop (op A)).left) g.unop.left.op
h : LE.le (α := Subobject.{v₁, u₁} (op (unop (op A)).left)) (Subobject.mk f.unop.left.op) (Subobject.mk g.unop.left.op)
rw : (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h ≫ g.unop.left.op).unop = f.unop.left
⊢ g.unop.left.op.unop ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left

Tactic:
rw [← unop_comp]

Premises used: CategoryTheory.unop_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 : Functor.{v₁, v₂, u₁, u₂} C D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst_2 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop P).left) (Y := op (unop (op A)).left) f.unop.left.op
inst_3 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop Q).left) (Y := op (unop (op A)).left) g.unop.left.op
h : LE.le (α := Subobject.{v₁, u₁} (op (unop (op A)).left)) (Subobject.mk f.unop.left.op) (Subobject.mk g.unop.left.op)
⊢ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h ≫ g.unop.left.op).unop = f.unop.left

Tactic:
simp only [Subobject.ofMkLEMk_comp, Quiver.Hom.unop_op]

Premises used: Quiver.Hom.unop_op, CategoryTheory.Subobject.ofMkLEMk_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 : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : HasFiniteColimits.{v₁, u₁} C
inst_3 : PreservesFiniteColimits S
A : CostructuredArrow S T
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 }
⊢ (↑((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) ⋯ :
              { 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 }))
          ((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)) ⋯)
            P)) :
      Subobject (op A.left)) =
    (↑P : Subobject (op A.left))

Tactic:
simp only [liftQuotient, Quiver.Hom.unop_op, homMk_left,
      Quiver.Hom.op_unop, projectQuotient_mk, Subobject.mk_arrow]

Premises used: Quiver.Hom.unop_op, Quiver.Hom.op_unop, CategoryTheory.Subobject.mk_arrow, CategoryTheory.CostructuredArrow.homMk_left, CategoryTheory.CostructuredArrow.liftQuotient, CategoryTheory.CostructuredArrow.projectQuotient_mk
-- 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
⊢ 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:
⟨fun h => Subobject.mk_le_mk_of_comm ?_ ?_, fun h => ?_⟩

Premises used: CategoryTheory.Subobject.mk_le_mk_of_comm, Iff.intro