awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Comma (goal)
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)
| g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop
have a : g.unop.left.op.unop
Tactic: congr
    rw [← Quiver.Hom.unop_op g.unop.left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Comma (goal)
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 ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop
have a₁ : (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop
Tactic: congr
    rw [← Quiver.Hom.unop_op g.unop.left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Comma (goal)
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)
⊢ g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left
have conv_lhs : g.unop.left.op.unop ≫ (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Comma (goal)
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)
⊢ g.unop.left.op.unop ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left
have rw : (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h ≫ g.unop.left.op).unop = f.unop.left
Tactic: rw [← unop_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Comma (goal)
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 })
⊢ P ⟶ Q
have 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
Tactic: refine (homMk (Subobject.ofMkLEMk _ _ h).unop ((cancel_epi (S.map g.unop.left)).1 ?_)).op
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Comma (goal)
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 (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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Comma (goal)
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 = f
have h₁ : ((homMk (Subobject.ofMkLEMk (MonoOver.mk f).arrow.unop.left.op (MonoOver.mk g).arrow.unop.left.op h).unop sorry).op ≫
      g).unop =
  f.unop
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Comma (goal)
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 =
    f.unop
have h₁ : ((homMk (Subobject.ofMkLEMk (MonoOver.mk f).arrow.unop.left.op (MonoOver.mk g).arrow.unop.left.op h).unop sorry).op ≫
        g).unop.left =
  f.unop.left
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Comma (goal)
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 })
have h₁ : (Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op = (MonoOver.mk f).arrow.unop.left.op
Tactic: refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).unop.left.op ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Comma (goal)
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
⊢ (Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op = (MonoOver.mk f).arrow.unop.left.op
have h₁ : Quiver.Hom.unop ((Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op) =
  (MonoOver.mk f).arrow.unop.left.op.unop
Tactic: refine Quiver.Hom.unop_inj ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Comma (hypothesis)
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
⊢ Quiver.Hom.unop ((Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op) =
    (MonoOver.mk f).arrow.unop.left.op.unop
have this : (Subobject.ofMkLEMk f g h ≫ g).unop = f.unop
Tactic: have := congr_arg Quiver.Hom.unop (Subobject.ofMkLEMk_comp h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
⊢ Eq (α := Prop) ((fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) P) ((fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) Q)
have a : (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) P ↔ (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) Q
Tactic: apply propext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
⊢ (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) P ↔ (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) Q
have a : (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) P → (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) Q
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
a : (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) P → (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) Q
⊢ (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) P ↔ (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) Q
have a₁ : (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) Q → (fun (P : MonoOver.{v₁, u₁} Y) ↦ P.Factors f) P
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
i : X ⟶ P.obj (P := Over.isMono Y).left
w : i ≫ P.arrow = f
⊢ (i ≫ Over.Hom.left h.hom.hom) ≫ Q.arrow = f
have rw : i ≫ Over.Hom.left h.hom.hom ≫ Q.arrow = f
Tactic: rw [Category.assoc, Over.w h.hom.hom, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
i : X ⟶ P.obj (P := Over.isMono Y).left
w : i ≫ P.arrow = f
rw : i ≫ Over.Hom.left h.hom.hom ≫ Q.arrow = f
⊢ (i ≫ Over.Hom.left h.hom.hom) ≫ Q.arrow = f
have rw₁ : i ≫ P.obj (P := Over.isMono Y).hom = f
Tactic: rw [Category.assoc, Over.w h.hom.hom, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
i : X ⟶ P.obj (P := Over.isMono Y).left
w : i ≫ P.arrow = f
rw : i ≫ Over.Hom.left h.hom.hom ≫ Q.arrow = f
rw₁ : i ≫ P.obj (P := Over.isMono Y).hom = f
⊢ (i ≫ Over.Hom.left h.hom.hom) ≫ Q.arrow = f
have rw₂ : f = f
Tactic: rw [Category.assoc, Over.w h.hom.hom, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
i : X ⟶ Q.obj (P := Over.isMono Y).left
w : i ≫ Q.arrow = f
⊢ (i ≫ Over.Hom.left h.inv.hom) ≫ P.arrow = f
have rw : i ≫ Over.Hom.left h.inv.hom ≫ P.arrow = f
Tactic: rw [Category.assoc, Over.w h.inv.hom, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
i : X ⟶ Q.obj (P := Over.isMono Y).left
w : i ≫ Q.arrow = f
rw : i ≫ Over.Hom.left h.inv.hom ≫ P.arrow = f
⊢ (i ≫ Over.Hom.left h.inv.hom) ≫ P.arrow = f
have rw₁ : i ≫ Q.obj (P := Over.isMono Y).hom = f
Tactic: rw [Category.assoc, Over.w h.inv.hom, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
P_1 : Subobject.{v₁, u₁} Y
f : X ⟶ Y
P Q : MonoOver.{v₁, u₁} Y
h : P ≅ Q
i : X ⟶ Q.obj (P := Over.isMono Y).left
w : i ≫ Q.arrow = f
rw : i ≫ Over.Hom.left h.inv.hom ≫ P.arrow = f
rw₁ : i ≫ Q.obj (P := Over.isMono Y).hom = f
⊢ (i ≫ Over.Hom.left h.inv.hom) ≫ P.arrow = f
have rw₂ : f = f
Tactic: rw [Category.assoc, Over.w h.inv.hom, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
P : Subobject.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
⊢ P.Factors (f ≫ g)
have h₁ : ∀ (a : MonoOver.{v₁, u₁} Z) (h : Factors (Quotient.mk'' a) g), Factors (Quotient.mk'' a) (f ≫ g)
Tactic: induction P using Quotient.ind'
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.FactorThru (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
a : MonoOver.{v₁, u₁} Z
h : Factors (Quotient.mk'' a) g
⊢ Factors (Quotient.mk'' a) (f ≫ g)
have h₁ : ∀ (g : Y ⟶ a.obj (P := Over.isMono Z).left), Factors (Quotient.mk'' a) (f ≫ g ≫ a.arrow)
Tactic: obtain ⟨g, rfl⟩ := h
Cleared hypotheses: g, h