awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_3 : Category.{v₃, u₃} A
B : Type u₄
inst_4 : Category.{v₄, u₄} B
U : Functor.{v₃, v₄, u₃, u₄} A B
V : B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst_5 : F.IsEquivalence
inst_6 : G.Faithful
inst_7 : G.Full
inst_8 : IsIso α
inst_9 : IsIso β
X : Discrete PUnit.{1}
inst : IsIso β
⊢ IsIso.{v₄, u₄} (C := B) (X := (Functor.fromPUnit T ⋙ G).obj X) (Y :=
    Functor.obj.{0, v₄, 0, u₄} (𝟭 (Discrete PUnit.{1}) ⋙ Functor.fromPUnit V) X)
    (NatTrans.app (Discrete.natTrans fun (x : Discrete PUnit.{1}) ↦ β) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
B : Type u₄
inst_3 : Category.{v₄, u₄} B
U : Functor.{v₃, v₄, u₃, u₄} A B
V : B
F : Functor.{v₁, v₃, u₁, u₃} C A
G : Functor.{v₂, v₄, u₂, u₄} D B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
inst_4 : F.IsEquivalence
inst_5 : G.Faithful
inst_6 : G.Full
inst_7 : IsIso α
inst_8 : IsIso β
X : Discrete PUnit.{1}
⊢ IsIso β

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
f g : CostructuredArrow S T
h : f.IsUniversal
η : g ⟶ f
⊢ η = IsTerminal.from h g

Tactic:
h.hom_ext η (h.from g)

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
f : CostructuredArrow S T
h : f.IsUniversal
g : CostructuredArrow S T
⊢ S.map (h.lift g) ≫ f.hom = g.hom

Tactic:
Category.comp_id g.hom ▸ (h.from g).w

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.CostructuredArrow.hom, Eq.rec, CategoryTheory.CommaMorphism.w, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
f : CostructuredArrow S T
h : f.IsUniversal
c : C
η : c ⟶ f.left
⊢ η = h.lift (mk (S.map η ≫ f.hom))

Tactic:
let g := mk <| S.map η ≫ f.hom
  congrArg CommaMorphism.left (h.hom_ext (homMk η rfl : g ⟶ f) (h.from g))

Premises used: CategoryTheory.Limits.IsTerminal.from, congrArg, CategoryTheory.CostructuredArrow.hom, CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Functor.map, CategoryTheory.CommaMorphism.left, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.CostructuredArrow.mk, CategoryTheory.CostructuredArrow.IsUniversal.lift, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
f : CostructuredArrow S T
h : f.IsUniversal
c : C
η η' : c ⟶ f.left
w : S.map η ≫ f.hom = S.map η' ≫ f.hom
rw : h.lift (mk (S.map η ≫ f.hom)) = η'
rw₁ :
  Eq (α := c ⟶ f.left) (h.lift (mk (S.map η ≫ f.hom)) : (mk (S.map η ≫ f.hom)).left ⟶ f.left)
    (h.lift (mk (S.map η' ≫ f.hom)))
rw₂ rw₃ :
  Eq (α := c ⟶ f.left) (h.lift (mk (S.map η' ≫ f.hom)) : (mk (S.map η' ≫ f.hom)).left ⟶ f.left)
    (h.lift (mk (S.map η' ≫ f.hom)))
⊢ η = η'

Tactic:
rw [h.hom_desc η, h.hom_desc η', w]

Premises used: CategoryTheory.CostructuredArrow.IsUniversal.hom_desc
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : D
S : Functor.{v₁, v₂, u₁, u₂} C D
f_1 : CostructuredArrow S T
h : f_1.IsUniversal
g : CostructuredArrow S T
f : g.left ⟶ f_1.left
w : (fun (η : g.left ⟶ f_1.left) ↦ S.map η ≫ f_1.hom = g.hom) f
⊢ S.map f ≫ f_1.hom = S.map (h.lift g) ≫ f_1.hom

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₃, v₁, u₃, u₁} E C
X : D
F : Functor.{v₁, v₂, u₁, u₂} C D
f : (Y : E) → X ⟶ F.obj (G.obj Y)
h : ∀ {Y Z : E} (g : Y ⟶ Z), f Y ≫ F.map (G.map g) = f Z
⊢ G.toStructuredArrow X F f ⋯ ⋙ StructuredArrow.proj X F = G

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₃, v₁, u₃, u₁} E C
F : Functor.{v₁, v₂, u₁, u₂} C D
X : D
f : (Y : E) → F.obj (G.obj Y) ⟶ X
h : ∀ {Y Z : E} (g : Y ⟶ Z), F.map (G.map g) ≫ f Z = f Y
⊢ G.toCostructuredArrow F X f ⋯ ⋙ CostructuredArrow.proj F X = G

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X Y : (StructuredArrow d F)ᵒᵖ
f : X ⟶ Y
⊢ Eq (α :=
    F.op.obj
        (CostructuredArrow.left.{v₁, v₂, u₁, u₂} (D := Dᵒᵖ) (S := F.op) (T := op d)
          (CostructuredArrow.mk (Y := op (unop X).right) (unop X).hom.op)) ⟶
      op d)
    (F.op.map (Hom.right f.unop).op ≫
      CostructuredArrow.hom (CostructuredArrow.mk (Y := op (unop Y).right) (unop Y).hom.op))
    (CostructuredArrow.hom (CostructuredArrow.mk (Y := op (unop X).right) (unop X).hom.op))

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X Y : (StructuredArrow (op d) F.op)ᵒᵖ
f : X ⟶ Y
⊢ (F.map (Hom.right f.unop).unop ≫ (CostructuredArrow.mk (unop Y).hom.unop).hom).op =
    (CostructuredArrow.mk (unop X).hom.unop).hom.op

Tactic:
simp [dsimp% f.unop.w]

Premises used: Quiver.Hom.unop, CategoryTheory.StructuredArrow.Hom.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X Y : (CostructuredArrow F d)ᵒᵖ
f : X ⟶ Y
⊢ StructuredArrow.hom (StructuredArrow.mk (Y := op (unop X).left) (unop X).hom.op) ≫ F.op.map f.unop.left.op =
    StructuredArrow.hom (StructuredArrow.mk (Y := op (unop Y).left) (unop Y).hom.op)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X Y : (CostructuredArrow F.op (op d))ᵒᵖ
f : X ⟶ Y
⊢ ((StructuredArrow.mk (unop X).hom.unop).hom ≫ F.map f.unop.left.unop).op =
    (StructuredArrow.mk (unop Y).hom.unop).hom.op

Tactic:
simp [dsimp% f.unop.w]

Premises used: Quiver.Hom.unop, CategoryTheory.CommaMorphism.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X Y : StructuredArrow d F
f : op X ⟶ op Y
obtain :
  ∀ (X : C) (x : d ⟶ F.obj X) (f : op (StructuredArrow.mk x) ⟶ op Y),
    Eq (α :=
      Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x)) ⟶
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj (op Y))
      (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
        Iso.hom ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op) (op Y)))
      (Iso.hom
          ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
            (op (StructuredArrow.mk x))) ≫
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f)
⊢ Eq (α :=
    Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op X) ⟶
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj (op Y))
    (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
      Iso.hom ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op) (op Y)))
    (Iso.hom ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op) (op X)) ≫
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f)

Tactic:
obtain ⟨X, x, rfl⟩ := X.mk_surjective

Premises used: CategoryTheory.StructuredArrow.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
Y : StructuredArrow d F
X : C
x : d ⟶ F.obj X
f : op (StructuredArrow.mk x) ⟶ op Y
obtain :
  ∀ (Y : C) (y : d ⟶ F.obj Y) (f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)),
    Eq (α :=
      Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x)) ⟶
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj
          (op (StructuredArrow.mk y)))
      (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
            (op (StructuredArrow.mk y))))
      (Iso.hom
          ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
            (op (StructuredArrow.mk x))) ≫
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f)
⊢ Eq (α :=
    Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x)) ⟶
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj (op Y))
    (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
      Iso.hom ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op) (op Y)))
    (Iso.hom
        ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
          (op (StructuredArrow.mk x))) ≫
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f)

Tactic:
obtain ⟨Y, y, rfl⟩ := Y.mk_surjective

Premises used: CategoryTheory.StructuredArrow.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X : C
x : d ⟶ F.obj X
Y : C
y : d ⟶ F.obj Y
f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)
h :
  Eq (α :=
    (unop
          ((StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj
            (op (StructuredArrow.mk y)))).right ⟶
      (unop (Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x)))).right)
    (StructuredArrow.Hom.right
      (Quiver.Hom.unop
        (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
          Iso.hom
            ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
              (op (StructuredArrow.mk y))))))
    (StructuredArrow.Hom.right
      (Quiver.Hom.unop
        (Iso.hom
            ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
              (op (StructuredArrow.mk x))) ≫
          (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f)))
⊢ Eq (α :=
    unop
        ((StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj
          (op (StructuredArrow.mk y))) ⟶
      unop (Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x))))
    (Quiver.Hom.unop
      (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
            (op (StructuredArrow.mk y)))))
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
            (op (StructuredArrow.mk x))) ≫
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X : C
x : d ⟶ F.obj X
Y : C
y : d ⟶ F.obj Y
f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)
⊢ Eq (α :=
    op (unop (Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x)))).right ⟶
      op
        (unop
            ((StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj
              (op (StructuredArrow.mk y)))).right)
    (Quiver.Hom.op
      (StructuredArrow.Hom.right
        (Quiver.Hom.unop
          (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
            Iso.hom
              ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
                (op (StructuredArrow.mk y)))))))
    (Quiver.Hom.op
      (StructuredArrow.Hom.right
        (Quiver.Hom.unop
          (Iso.hom
              ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
                (op (StructuredArrow.mk x))) ≫
            (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X : C
x : d ⟶ F.obj X
Y : C
y : d ⟶ F.obj Y
f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)
⊢ Eq (α :=
    (unop
          ((StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj
            (op (StructuredArrow.mk y)))).right ⟶
      (unop (Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x)))).right)
    (StructuredArrow.Hom.right
      (Quiver.Hom.unop
        (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
          Iso.hom
            ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
              (op (StructuredArrow.mk y))))))
    (StructuredArrow.Hom.right
      (Quiver.Hom.unop
        (Iso.hom
            ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
              (op (StructuredArrow.mk x))) ≫
          (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f)))

Tactic:
apply Quiver.Hom.op_inj (by simp)

Premises used: Quiver.Hom.op_inj
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X : C
x : d ⟶ F.obj X
Y : C
y : d ⟶ F.obj Y
f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)
⊢ Eq (α :=
    Functor.obj (𝟭 (StructuredArrow d F)ᵒᵖ) (op (StructuredArrow.mk x)) ⟶
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).obj
        (op (StructuredArrow.mk y)))
    (Functor.map (𝟭 (StructuredArrow d F)ᵒᵖ) f ≫
      Iso.hom
        ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
          (op (StructuredArrow.mk y))))
    (Iso.hom
        ((fun (X : (StructuredArrow d F)ᵒᵖ) ↦ (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op)
          (op (StructuredArrow.mk x))) ≫
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f)

Tactic:
exact Quiver.Hom.unop_inj (by ext; apply Quiver.Hom.op_inj (by simp))

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X Y : CostructuredArrow F d
f : op X ⟶ op Y
obtain :
  ∀ (X : C) (x : F.obj X ⟶ d) (f : op (CostructuredArrow.mk x) ⟶ op Y),
    Eq (α :=
      Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x)) ⟶
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj (op Y))
      (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op) (op Y)))
      (Iso.hom
          ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
            (op (CostructuredArrow.mk x))) ≫
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f)
⊢ Eq (α :=
    Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op X) ⟶
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj (op Y))
    (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
      Iso.hom ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op) (op Y)))
    (Iso.hom ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op) (op X)) ≫
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f)

Tactic:
obtain ⟨X, x, rfl⟩ := X.mk_surjective

Premises used: CategoryTheory.CostructuredArrow.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
Y : CostructuredArrow F d
X : C
x : F.obj X ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op Y
obtain :
  ∀ (Y : C) (y : F.obj Y ⟶ d) (f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)),
    Eq (α :=
      Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x)) ⟶
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj
          (op (CostructuredArrow.mk y)))
      (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
            (op (CostructuredArrow.mk y))))
      (Iso.hom
          ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
            (op (CostructuredArrow.mk x))) ≫
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f)
⊢ Eq (α :=
    Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x)) ⟶
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj (op Y))
    (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
      Iso.hom ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op) (op Y)))
    (Iso.hom
        ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
          (op (CostructuredArrow.mk x))) ≫
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f)

Tactic:
obtain ⟨Y, y, rfl⟩ := Y.mk_surjective

Premises used: CategoryTheory.CostructuredArrow.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X : C
x : F.obj X ⟶ d
Y : C
y : F.obj Y ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)
h :
  Eq (α :=
    (unop
          ((CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj
            (op (CostructuredArrow.mk y)))).left ⟶
      (unop (Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x)))).left)
    (CommaMorphism.left
      (Quiver.Hom.unop
        (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
          Iso.hom
            ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
              (op (CostructuredArrow.mk y))))))
    (CommaMorphism.left
      (Quiver.Hom.unop
        (Iso.hom
            ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
              (op (CostructuredArrow.mk x))) ≫
          (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f)))
⊢ Eq (α :=
    unop
        ((CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj
          (op (CostructuredArrow.mk y))) ⟶
      unop (Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x))))
    (Quiver.Hom.unop
      (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
            (op (CostructuredArrow.mk y)))))
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
            (op (CostructuredArrow.mk x))) ≫
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X : C
x : F.obj X ⟶ d
Y : C
y : F.obj Y ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)
⊢ Eq (α :=
    op (unop (Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x)))).left ⟶
      op
        (unop
            ((CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj
              (op (CostructuredArrow.mk y)))).left)
    (Quiver.Hom.op
      (CommaMorphism.left
        (Quiver.Hom.unop
          (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
            Iso.hom
              ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
                (op (CostructuredArrow.mk y)))))))
    (Quiver.Hom.op
      (CommaMorphism.left
        (Quiver.Hom.unop
          (Iso.hom
              ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
                (op (CostructuredArrow.mk x))) ≫
            (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
X : C
x : F.obj X ⟶ d
Y : C
y : F.obj Y ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)
⊢ Eq (α :=
    (unop
          ((CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj
            (op (CostructuredArrow.mk y)))).left ⟶
      (unop (Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x)))).left)
    (CommaMorphism.left
      (Quiver.Hom.unop
        (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
          Iso.hom
            ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
              (op (CostructuredArrow.mk y))))))
    (CommaMorphism.left
      (Quiver.Hom.unop
        (Iso.hom
            ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
              (op (CostructuredArrow.mk x))) ≫
          (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f)))

Tactic:
apply Quiver.Hom.op_inj (by simp)

Premises used: Quiver.Hom.op_inj