awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
refine_1 :
  ∀ (hP : IsDetecting.{v₁, u₁} P.op) (X Y : C) (f : X ⟶ Y)
    (hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h), IsIso f
refine_2 :
  ∀ (hP : P.IsCodetecting) (X Y : Cᵒᵖ) (f : X ⟶ Y)
    (hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h), IsIso f
⊢ IsDetecting.{v₁, u₁} P.op ↔ P.IsCodetecting

Tactic:
refine ⟨fun hP X Y f hf => ?_, fun hP X Y f hf => ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsDetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
⊢ IsIso f

Tactic:
(isIso_op_iff _).1 (hP _ fun G hG h => ?_)

Premises used: Iff.mp, CategoryTheory.isIso_op_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsDetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
refine_1 : ∀ (G : Cᵒᵖ) (hG : P.op G) (h : G ⟶ op X), ∃! h' : G ⟶ op Y, h' ≫ f.op = h
⊢ IsIso f

Tactic:
refine (isIso_op_iff _).1 (hP _ fun G hG h => ?_)

Premises used: Iff.mp, CategoryTheory.isIso_op_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsDetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
G : Cᵒᵖ
hG : P.op G
h : G ⟶ op X
refine_1 :
  ∀ (t : Y ⟶ unop G) (ht : f ≫ t = h.unop)
    (ht' : ∀ (y : Y ⟶ unop G), (fun (h' : Y ⟶ unop G) ↦ f ≫ h' = h.unop) y → y = t), ∃! h' : G ⟶ op Y, h' ≫ f.op = h
⊢ ∃! h' : G ⟶ op Y, h' ≫ f.op = h

Tactic:
obtain ⟨t, ht, ht'⟩ := hf (unop G) hG h.unop

Premises used: Quiver.Hom.unop, Opposite.unop
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsDetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
G : Cᵒᵖ
hG : P.op G
h : G ⟶ op X
t : Y ⟶ unop G
ht : f ≫ t = h.unop
ht' : ∀ (y : Y ⟶ unop G), (fun (h' : Y ⟶ unop G) ↦ f ≫ h' = h.unop) y → y = t
⊢ ∃! h' : G ⟶ op Y, h' ≫ f.op = h

Tactic:
⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩

Premises used: Quiver.Hom.op, Quiver.Hom.op_inj, Quiver.Hom.unop, Quiver.Hom.unop_inj, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsDetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
G : Cᵒᵖ
hG : P.op G
h : G ⟶ op X
t : Y ⟶ unop G
ht : f ≫ t = h.unop
ht' : ∀ (y : Y ⟶ unop G), (fun (h' : Y ⟶ unop G) ↦ f ≫ h' = h.unop) y → y = t
⊢ ∃! h' : G ⟶ op Y, h' ≫ f.op = h

Tactic:
exact
      ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
⊢ IsIso f

Tactic:
(isIso_unop_iff _).1 (hP _ fun G hG h => ?_)

Premises used: CategoryTheory.isIso_unop_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
refine_2 : ∀ (G : C) (hG : P G) (h : unop Y ⟶ G), ∃! h' : unop X ⟶ G, f.unop ≫ h' = h
⊢ IsIso f

Tactic:
refine (isIso_unop_iff _).1 (hP _ fun G hG h => ?_)

Premises used: CategoryTheory.isIso_unop_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
G : C
hG : P G
h : unop Y ⟶ G
refine_2 :
  ∀ (t : op G ⟶ X) (ht : t ≫ f = h.op) (ht' : ∀ (y : op G ⟶ X), (fun (h' : op G ⟶ X) ↦ h' ≫ f = h.op) y → y = t),
    ∃! h' : unop X ⟶ G, f.unop ≫ h' = h
⊢ ∃! h' : unop X ⟶ G, f.unop ≫ h' = h

Tactic:
obtain ⟨t, ht, ht'⟩ := hf (op G) hG h.op

Premises used: Quiver.Hom.op, Opposite.op
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
G : C
hG : P G
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun (h' : op G ⟶ X) ↦ h' ≫ f = h.op) y → y = t
⊢ ∃! h' : unop X ⟶ G, f.unop ≫ h' = h

Tactic:
⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩

Premises used: Quiver.Hom.op, Quiver.Hom.op_inj, Quiver.Hom.unop, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
G : C
hG : P G
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun (h' : op G ⟶ X) ↦ h' ≫ f = h.op) y → y = t
refine_2 :
  ∀ (y : unop X ⟶ G) (hy : (fun (h' : unop X ⟶ G) ↦ f.unop ≫ h' = h) y), (fun (h' : op G ⟶ X) ↦ h' ≫ f = h.op) y.op
⊢ ∃! h' : unop X ⟶ G, f.unop ≫ h' = h

Tactic:
refine ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
G : C
hG : P G
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun (h' : op G ⟶ X) ↦ h' ≫ f = h.op) y → y = t
y : unop X ⟶ G
hy : (fun (h' : unop X ⟶ G) ↦ f.unop ≫ h' = h) y
⊢ Quiver.Hom.unop (y.op ≫ f) = h.op.unop

Tactic:
simpa only using hy
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
G : C
hG : P G
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun (h' : op G ⟶ X) ↦ h' ≫ f = h.op) y → y = t
y : unop X ⟶ G
hy : (fun (h' : unop X ⟶ G) ↦ f.unop ≫ h' = h) y
⊢ (fun (h' : op G ⟶ X) ↦ h' ≫ f = h.op) y.op

Tactic:
exact Quiver.Hom.unop_inj (by simpa only using hy)

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
⊢ IsCodetecting.{v₁, u₁} P.op ↔ P.IsDetecting

Tactic:
⟨fun hP X Y f hf => ?_, fun hP X Y f hf => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
refine_1 :
  ∀ (hP : IsCodetecting.{v₁, u₁} P.op) (X Y : C) (f : X ⟶ Y)
    (hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h), IsIso f
refine_2 :
  ∀ (hP : P.IsDetecting) (X Y : Cᵒᵖ) (f : X ⟶ Y) (hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h),
    IsIso f
⊢ IsCodetecting.{v₁, u₁} P.op ↔ P.IsDetecting

Tactic:
refine ⟨fun hP X Y f hf => ?_, fun hP X Y f hf => ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsCodetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
⊢ IsIso f

Tactic:
(isIso_op_iff _).1 (hP _ fun G hG h => ?_)

Premises used: Iff.mp, CategoryTheory.isIso_op_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsCodetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
refine_1 : ∀ (G : Cᵒᵖ) (hG : P.op G) (h : op Y ⟶ G), ∃! h' : op X ⟶ G, f.op ≫ h' = h
⊢ IsIso f

Tactic:
refine (isIso_op_iff _).1 (hP _ fun G hG h => ?_)

Premises used: Iff.mp, CategoryTheory.isIso_op_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsCodetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
G : Cᵒᵖ
hG : P.op G
h : op Y ⟶ G
refine_1 :
  ∀ (t : unop G ⟶ X) (ht : t ≫ f = h.unop)
    (ht' : ∀ (y : unop G ⟶ X), (fun (h' : unop G ⟶ X) ↦ h' ≫ f = h.unop) y → y = t), ∃! h' : op X ⟶ G, f.op ≫ h' = h
⊢ ∃! h' : op X ⟶ G, f.op ≫ h' = h

Tactic:
obtain ⟨t, ht, ht'⟩ := hf (unop G) hG h.unop

Premises used: Quiver.Hom.unop, Opposite.unop
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsCodetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
G : Cᵒᵖ
hG : P.op G
h : op Y ⟶ G
t : unop G ⟶ X
ht : t ≫ f = h.unop
ht' : ∀ (y : unop G ⟶ X), (fun (h' : unop G ⟶ X) ↦ h' ≫ f = h.unop) y → y = t
⊢ ∃! h' : op X ⟶ G, f.op ≫ h' = h

Tactic:
⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩

Premises used: Quiver.Hom.op, Quiver.Hom.op_inj, Quiver.Hom.unop, Quiver.Hom.unop_inj, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsCodetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
G : Cᵒᵖ
hG : P.op G
h : op Y ⟶ G
t : unop G ⟶ X
ht : t ≫ f = h.unop
ht' : ∀ (y : unop G ⟶ X), (fun (h' : unop G ⟶ X) ↦ h' ≫ f = h.unop) y → y = t
⊢ ∃! h' : op X ⟶ G, f.op ≫ h' = h

Tactic:
exact
      ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
⊢ IsIso f

Tactic:
(isIso_unop_iff _).1 (hP _ fun G hG h => ?_)

Premises used: CategoryTheory.isIso_unop_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
refine_2 : ∀ (G : C) (hG : P G) (h : G ⟶ unop X), ∃! h' : G ⟶ unop Y, h' ≫ f.unop = h
⊢ IsIso f

Tactic:
refine (isIso_unop_iff _).1 (hP _ fun G hG h => ?_)

Premises used: CategoryTheory.isIso_unop_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
G : C
hG : P G
h : G ⟶ unop X
refine_2 :
  ∀ (t : Y ⟶ op G) (ht : f ≫ t = h.op) (ht' : ∀ (y : Y ⟶ op G), (fun (h' : Y ⟶ op G) ↦ f ≫ h' = h.op) y → y = t),
    ∃! h' : G ⟶ unop Y, h' ≫ f.unop = h
⊢ ∃! h' : G ⟶ unop Y, h' ≫ f.unop = h

Tactic:
obtain ⟨t, ht, ht'⟩ := hf (op G) hG h.op

Premises used: Quiver.Hom.op, Opposite.op
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
G : C
hG : P G
h : G ⟶ unop X
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun (h' : Y ⟶ op G) ↦ f ≫ h' = h.op) y → y = t
⊢ ∃! h' : G ⟶ unop Y, h' ≫ f.unop = h

Tactic:
⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩

Premises used: Quiver.Hom.op, Quiver.Hom.op_inj, Quiver.Hom.unop, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
G : C
hG : P G
h : G ⟶ unop X
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun (h' : Y ⟶ op G) ↦ f ≫ h' = h.op) y → y = t
refine_2 :
  ∀ (y : G ⟶ unop Y) (hy : (fun (h' : G ⟶ unop Y) ↦ h' ≫ f.unop = h) y), (fun (h' : Y ⟶ op G) ↦ f ≫ h' = h.op) y.op
⊢ ∃! h' : G ⟶ unop Y, h' ≫ f.unop = h

Tactic:
refine ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
G : C
hG : P G
h : G ⟶ unop X
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun (h' : Y ⟶ op G) ↦ f ≫ h' = h.op) y → y = t
y : G ⟶ unop Y
hy : (fun (h' : G ⟶ unop Y) ↦ h' ≫ f.unop = h) y
⊢ (f ≫ y.op).unop = h.op.unop

Tactic:
simpa only using hy
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
G : C
hG : P G
h : G ⟶ unop X
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun (h' : Y ⟶ op G) ↦ f ≫ h' = h.op) y → y = t
y : G ⟶ unop Y
hy : (fun (h' : G ⟶ unop Y) ↦ h' ≫ f.unop = h) y
⊢ (fun (h' : Y ⟶ op G) ↦ f ≫ h' = h.op) y.op

Tactic:
exact Quiver.Hom.unop_inj (by simpa only using hy)

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} Cᵒᵖ
⊢ P.unop.IsDetecting ↔ IsCodetecting.{v₁, u₁} P

Tactic:
P.unop.isCodetecting_op_iff.symm

Premises used: CategoryTheory.ObjectProperty.unop, CategoryTheory.ObjectProperty.isCodetecting_op_iff, CategoryTheory.ObjectProperty.op, Iff.symm
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} Cᵒᵖ
⊢ P.unop.IsCodetecting ↔ IsDetecting.{v₁, u₁} P

Tactic:
P.unop.isDetecting_op_iff.symm

Premises used: CategoryTheory.ObjectProperty.isDetecting_op_iff, CategoryTheory.ObjectProperty.unop, CategoryTheory.ObjectProperty.op, Iff.symm
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : HasEqualizers.{v₁, u₁} C
hP : P.IsDetecting
⊢ P.IsSeparating

Tactic:
fun _ _ f g hfg =>
  have : IsIso (equalizer.ι f g) := hP _ fun _ hG _ => equalizer.existsUnique _ (hfg _ hG _)
  eq_of_epi_equalizer

Premises used: CategoryTheory.Limits.equalizer.ι, CategoryTheory.Limits.equalizer.existsUnique, CategoryTheory.Limits.eq_of_epi_equalizer, CategoryTheory.ObjectProperty.IsSeparating
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : HasCoequalizers.{v₁, u₁} C
⊢ P.IsCodetecting → P.IsCoseparating

Tactic:
simpa only [← isSeparating_op_iff, ← isDetecting_op_iff] using IsDetecting.isSeparating

Premises used: CategoryTheory.ObjectProperty.isDetecting_op_iff, CategoryTheory.ObjectProperty.IsDetecting.isSeparating, CategoryTheory.ObjectProperty.isSeparating_op_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
h_1 : Mono f
x : C
h_2 : P x
x_1 x_2 : x ⟶ X
h : x_1 ≫ f = x_2 ≫ f
⊢ x_1 = x_2

Tactic:
simpa [cancel_mono] using h

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (g₁ g₂ : G ⟶ X), g₁ ≫ f = g₂ ≫ f → g₁ = g₂
Z : C
g₁ g₂ : Z ⟶ X
h : g₁ ≫ f = g₂ ≫ f
G : C
hG : P G
h' : G ⟶ Z
⊢ (h' ≫ g₁) ≫ f = (h' ≫ g₂) ≫ f

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCoseparating
X Y : C
f : X ⟶ Y
h_1 : Epi f
x : C
h_2 : P x
x_1 x_2 : Y ⟶ x
h : f ≫ x_1 = f ≫ x_2
⊢ x_1 = x_2

Tactic:
simpa [cancel_epi] using h

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCoseparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (g₁ g₂ : Y ⟶ G), f ≫ g₁ = f ≫ g₂ → g₁ = g₂
Z : C
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
G : C
hG : P G
h' : Z ⟶ G
⊢ f ≫ g₁ ≫ h' = f ≫ g₂ ≫ h'

Tactic:
simp [reassoc_of% h]
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
⊢ IsIso f

Tactic:
(isIso_iff_mono_and_epi _).2 ⟨⟨fun g h hgh => hP _ _ fun G hG i => ?_⟩, ⟨fun g h hgh => ?_⟩⟩

Premises used: Iff.mpr, CategoryTheory.Epi.mk, CategoryTheory.isIso_iff_mono_and_epi, And.intro, CategoryTheory.Mono.mk
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
refine_1 : ∀ {Z : C} (g h : Z ⟶ X) (hgh : g ≫ f = h ≫ f) (G : C) (hG : P G) (i : G ⟶ Z), i ≫ g = i ≫ h
refine_2 : ∀ {Z : C} (g h : Y ⟶ Z) (hgh : f ≫ g = f ≫ h), g = h
⊢ IsIso f

Tactic:
refine
    (isIso_iff_mono_and_epi _).2 ⟨⟨fun g h hgh => hP _ _ fun G hG i => ?_⟩, ⟨fun g h hgh => ?_⟩⟩

Premises used: Iff.mpr, CategoryTheory.Epi.mk, CategoryTheory.isIso_iff_mono_and_epi, And.intro, CategoryTheory.Mono.mk
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z
refine_1 : ∀ (t : G ⟶ X) (ht : ∀ (y : G ⟶ X), (fun (h' : G ⟶ X) ↦ h' ≫ f = i ≫ g ≫ f) y → y = t), i ≫ g = i ≫ h
⊢ i ≫ g = i ≫ h

Tactic:
obtain ⟨t, -, ht⟩ := hf G hG (i ≫ g ≫ f)

Premises used: CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z
t : G ⟶ X
ht : ∀ (y : G ⟶ X), (fun (h' : G ⟶ X) ↦ h' ≫ f = i ≫ g ≫ f) y → y = t
refine_1 : t = i ≫ h
refine_1₁ refine_1₂ : t = t
⊢ i ≫ g = i ≫ h

Tactic:
rw [ht (i ≫ g) (Category.assoc _ _ _), ht (i ≫ h) (hgh.symm ▸ Category.assoc _ _ _)]

Premises used: CategoryTheory.Category.assoc, Eq.rec, CategoryTheory.CategoryStruct.comp, Eq.symm
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
⊢ g = h

Tactic:
hP _ _ fun G hG i => ?_
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
refine_2 : ∀ (G : C) (hG : P G) (i : G ⟶ Y), i ≫ g = i ≫ h
⊢ g = h

Tactic:
refine hP _ _ fun G hG i => ?_
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
G : C
hG : P G
i : G ⟶ Y
refine_2 : ∀ (t : G ⟶ X), (t ≫ f) ≫ g = (t ≫ f) ≫ h
⊢ i ≫ g = i ≫ h

Tactic:
obtain ⟨t, rfl, -⟩ := hf G hG i

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
G : C
hG : P G
t : G ⟶ X
refine_2 : t ≫ f ≫ g = (t ≫ f) ≫ h
refine_2₁ : t ≫ f ≫ h = (t ≫ f) ≫ h
refine_2₂ refine_2₃ : t ≫ f ≫ h = t ≫ f ≫ h
⊢ (t ≫ f) ≫ g = (t ≫ f) ≫ h

Tactic:
rw [Category.assoc, hgh, Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst_1 : Mono f
mp :
  IsIso f →
    ∀ (G : C),
      P G →
        Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) X)) (β :=
          (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f)) :
            (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj X)) →
              (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj Y))
mpr :
  (∀ (G : C),
      P G →
        Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) X)) (β :=
          (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f)) :
            (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj X)) →
              (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj Y))) →
    IsIso f
⊢ IsIso f ↔
    ∀ (G : C),
      P G →
        Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) X)) (β :=
          (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f)) :
            (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj X)) →
              (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj Y))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst_1 : Mono f
h : IsIso f
⊢ ∀ (T : C), Function.Bijective (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f

Tactic:
rw [isIso_iff_yoneda_map_bijective] at h

Premises used: CategoryTheory.isIso_iff_yoneda_map_bijective
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst_1 : Mono f
h : ∀ (T : C), Function.Bijective (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f
A : C
mp :
  P A →
    Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op A)) X)) (β :=
      (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op A)) Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op A)) f)) :
        (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op A)).obj X)) →
          (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op A)).obj Y))
⊢ P A →
    Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op A)) X)) (β :=
      (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op A)) Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op A)) f)) :
        (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op A)).obj X)) →
          (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op A)).obj Y))

Tactic:
_