awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
commfst : e.functor.map (e.inverse.map m) ≫ (e.counitIso.app G).hom = (e.counitIso.app F).hom ≫ m
commsnd :
  e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)) ≫ Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω₀)) =
    (e.counitIso.app F).hom ≫ e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F))
commf :
  e.functor.map (𝒞₁.χ (e.inverse.map m)) ≫ Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω)) =
    (e.counitIso.app G).hom ≫ e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))
⊢ IsPullback m (e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)))
    (e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))) (e.functor.map 𝒞₁.truth)
have commg : e.functor.map 𝒞₁.truth ≫ Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω)) =
  Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω₀)) ≫ e.functor.map 𝒞₁.truth
Tactic: apply ((𝒞₁.isPullback (e.inverse.map m)).map e.functor).of_iso (e.counitIso.app _)
      (e.counitIso.app _) (.refl _) (.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀
χ' : G ⟶ e.functor.obj 𝒞₁.Ω
hχ' : IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth)
⊢ e.inverse.map χ' ≫ e.unitInv.app 𝒞₁.Ω = 𝒞₁.χ (e.inverse.map m)
have apply : IsPullback (e.inverse.map m) (e.inverse.map χ₀' ≫ e.unitInv.app 𝒞₁.Ω₀) (e.inverse.map χ' ≫ e.unitInv.app 𝒞₁.Ω) 𝒞₁.truth
Tactic: apply 𝒞₁.uniq (e.inverse.map m) (χ₀' := e.inverse.map χ₀' ≫ e.unitInv.app _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀
χ' : G ⟶ e.functor.obj 𝒞₁.Ω
hχ' : IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth)
⊢ χ' = e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))
have this : e.inverse.map χ' ≫ e.unitInv.app 𝒞₁.Ω = 𝒞₁.χ (e.inverse.map m)
Tactic: have : e.inverse.map χ' ≫ e.unitInv.app _ = 𝒞₁.χ (e.inverse.map m) := by
      apply 𝒞₁.uniq (e.inverse.map m) (χ₀' := e.inverse.map χ₀' ≫ e.unitInv.app _)
      exact (hχ'.map e.inverse).paste_vert <| IsPullback.of_vert_isIso_mono .mk
-- 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 : D
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasFiniteLimits.{v₁, u₁} C
inst_3 : PreservesFiniteLimits T
A : StructuredArrow S T
⊢ Subobject A → Subobject.{v₁, u₁} A.right
have refine : ∀ ⦃A_1 B : StructuredArrow S T⦄ (f : A_1 ⟶ A) (g : B ⟶ A) [inst_4 : Mono f] [inst_5 : Mono g] (i : A_1 ≅ B),
  i.hom ≫ g = f →
    Eq (α := Subobject.{v₁, u₁} A.right)
      ((fun (P : StructuredArrow S T) (f : P ⟶ A) (hf : Mono f) ↦ Subobject.mk (Hom.right f)) A_1 f inst_4)
      ((fun (P : StructuredArrow S T) (f : P ⟶ A) (hf : Mono f) ↦ Subobject.mk (Hom.right f)) B g inst_5)
Tactic: refine Subobject.lift (fun P f hf => Subobject.mk f.right) ?_
-- 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 : 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
⊢ 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)
have refine : ((proj S T).mapIso i).hom ≫ Hom.right g = Hom.right f
Tactic: refine Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i) ?_
-- 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 : 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 })
have h₁ : Hom.right (Subobject.ofMkLEMk f g h) ≫ Hom.right (MonoOver.mk g).arrow = Hom.right (MonoOver.mk f).arrow
Tactic: refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).right ?_
-- 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
⊢ Subobject (op A) → Subobject.{v₁, u₁} (op A.left)
have 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)
Tactic: refine Subobject.lift (fun P f hf => Subobject.mk f.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
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)
have refine : (((proj S T).mapIso i.unop).op.hom ≫ g.unop.left.op).unop = f.unop.left.op.unop
Tactic: refine Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i.unop).op (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
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ (((proj S T).mapIso i.unop).op.hom ≫ g.unop.left.op).unop = f.unop.left.op.unop
have this : (i.hom ≫ g).unop = f.unop
Tactic: have := congr_arg Quiver.Hom.unop hi
-- 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 : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ 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
have 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
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 : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ 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
have 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
Tactic: rw [← Category.assoc, ← S.map_comp, ← 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
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
| f.unop.left ≫ Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op))
have a : f.unop.left
Tactic: congr
-- 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 : (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
| f.unop.left ≫ Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op))
have a₁ : Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op))
Tactic: congr
-- 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 : (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
| f.unop.left
have a : f.unop.left.op.unop
Tactic: rw [← Quiver.Hom.unop_op f.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 : (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
| f.unop.left ≫ Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op))
have a : f.unop.left.op.unop
Tactic: congr
    rw [← Quiver.Hom.unop_op f.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 : (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 ≫ Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op))
have a₁ : Quiver.Hom.unop (Iso.hom (Subobject.underlyingIso f.unop.left.op))
Tactic: congr
    rw [← Quiver.Hom.unop_op f.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 : (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
⊢ 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)))
have 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)))
Tactic: conv_lhs =>
    congr
    rw [← Quiver.Hom.unop_op f.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 : (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
⊢ 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)))
have 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)))
Tactic: rw [← unop_comp, Subobject.underlyingIso_hom_comp_eq_mk]
-- 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 : (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)))
⊢ 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)))
have 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)))
Tactic: rw [← unop_comp, Subobject.underlyingIso_hom_comp_eq_mk]
-- 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 : (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
⊢ liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f
have i : op (mk q) ≅ P
Tactic: fapply Subobject.mk_eq_mk_of_comm
-- 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 : (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
⊢ liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f
have w : Eq (α := op (mk q) ⟶ op A) (Iso.hom (Iso.op (isoMk (Iso.unop (Subobject.underlyingIso f.unop.left.op)) sorry)) ≫ f)
  (Quiver.Hom.op (homMk (projectQuotient (Subobject.mk f)).arrow.unop hq))
Tactic: fapply Subobject.mk_eq_mk_of_comm
-- 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 : (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
⊢ op (mk q) ≅ P
have i : (unop P).left ≅ (mk q).left
Tactic: refine (Iso.op (isoMk ?_ ?_) : _ ≅ op (unop P))
-- 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 : (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
⊢ op (mk q) ≅ P
have i₁ : S.map (Iso.hom (Iso.unop (Subobject.underlyingIso f.unop.left.op))) ≫ (mk q).hom = (unop P).hom
Tactic: refine (Iso.op (isoMk ?_ ?_) : _ ≅ op (unop P))
-- 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 : (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
have 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
Tactic: refine (cancel_epi (S.map f.unop.left)).1 ?_
-- 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
Tactic: congr
-- 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
| 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
-- 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
have a : g.unop.left.op.unop
Tactic: rw [← Quiver.Hom.unop_op g.unop.left]