awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
h :
  ∀ (X : C),
    ObjectProperty.pair.{v₁, u₁} G H X ↔
      ObjectProperty.ofObj.{v₁, u₁, 0}
        (fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) X
⊢ Eq (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.pair G H)
    (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
X : C
h : G = X ∨ H = X ↔ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
⊢ ObjectProperty.pair.{v₁, u₁} G H X ↔
    ObjectProperty.ofObj.{v₁, u₁, 0}
      (fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) X

Tactic:
simp only [ObjectProperty.pair_iff, ObjectProperty.ofObj_iff]

Premises used: CategoryTheory.ObjectProperty.ofObj_iff, CategoryTheory.ObjectProperty.pair_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
X : C
h : G = X ∨ H = X → ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
h₁ : (∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X) → G = X ∨ H = X
⊢ G = X ∨ H = X ↔ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
⊢ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = G

Tactic:
⟨.left, rfl⟩

Premises used: Exists.intro, CategoryTheory.Limits.WalkingPair.left, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
⊢ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = H

Tactic:
⟨.right, rfl⟩

Premises used: CategoryTheory.Limits.WalkingPair.right, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
⊢ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = G

Tactic:
exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩]
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
h h₁ :
  ¬G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left →
    H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left
⊢ G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left ∨
    H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
h h₁ h₂ h₃ h₄ :
  ¬G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right →
    H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right
⊢ G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right ∨
    H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
hG : IsCoseparator.{v₁, u₁} G
⊢ LE.le (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.singleton G) (ObjectProperty.pair G H)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
hH : IsCoseparator.{v₁, u₁} H
⊢ LE.le (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.singleton H) (ObjectProperty.pair G H)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
inst_2 : HasProduct.{w, v₁, u₁} f
b : β
hb : IsCoseparator.{v₁, u₁} (f b)
⊢ LE.le (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.singleton (f b)) (ObjectProperty.ofObj f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
⊢ IsDetector.{v₁, u₁} G ↔ Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))

Tactic:
⟨fun hG => ⟨fun f hf => hG.def _ fun h => ?_⟩, fun h =>
      (isDetector_def _).2 fun X Y f hf => ?_⟩

Premises used: Iff.mpr, CategoryTheory.Functor.ReflectsIsomorphisms.mk, Iff.intro, CategoryTheory.IsDetector.def, CategoryTheory.isDetector_def
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
refine_1 :
  ∀ (hG : IsDetector.{v₁, u₁} G) {A B : C} (f : A ⟶ B)
    (hf : IsIso (X := Functor.obj (Functor.obj coyoneda (op G)) A) (Functor.map (Functor.obj coyoneda (op G)) f))
    (h : G ⟶ B), ∃! h' : G ⟶ A, h' ≫ f = h
refine_2 :
  ∀ (h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))) (X Y : C) (f : X ⟶ Y)
    (hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h), IsIso f
⊢ IsDetector.{v₁, u₁} G ↔ Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))

Tactic:
refine
    ⟨fun hG => ⟨fun f hf => hG.def _ fun h => ?_⟩, fun h =>
      (isDetector_def _).2 fun X Y f hf => ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsDetector.{v₁, u₁} G
A B : C
f : A ⟶ B
hf : IsIso (X := Functor.obj (Functor.obj coyoneda (op G)) A) (Functor.map (Functor.obj coyoneda (op G)) f)
h : G ⟶ B
refine_1 :
  ∀
    (hf :
      ∀ (b : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) B)),
        ∃! a : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) A),
          (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f) :
                (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj A)) →
                  (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj B))
              a =
            b)
    (h : G ⟶ B), ∃! h' : G ⟶ A, h' ≫ f = h
⊢ ∃! h' : G ⟶ A, h' ≫ f = h

Tactic:
rw [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf

Premises used: CategoryTheory.isIso_iff_bijective, Function.bijective_iff_existsUnique
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsDetector.{v₁, u₁} G
A B : C
f : A ⟶ B
hf :
  ∀ (b : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) B)),
    ∃! a : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) A),
      (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f) :
            (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj A)) →
              (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj B))
          a =
        b
h : G ⟶ B
⊢ ∃! h' : G ⟶ A, h' ≫ f = h

Tactic:
hf h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsDetector.{v₁, u₁} G
A B : C
f : A ⟶ B
hf :
  ∀ (b : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) B)),
    ∃! a : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) A),
      (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f) :
            (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj A)) →
              (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj B))
          a =
        b
h : G ⟶ B
⊢ ∃! h' : G ⟶ A, h' ≫ f = h

Tactic:
exact hf h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
this : IsIso (X := Functor.obj (Functor.obj coyoneda (op G)) X) (Functor.map (Functor.obj coyoneda (op G)) f)
⊢ IsIso f

Tactic:
@isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h

Premises used: CategoryTheory.coyoneda, CategoryTheory.isIso_of_reflects_iso, Opposite.op, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
this : IsIso (X := Functor.obj (Functor.obj coyoneda (op G)) X) (Functor.map (Functor.obj coyoneda (op G)) f)
⊢ IsIso f

Tactic:
exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h

Premises used: CategoryTheory.coyoneda, CategoryTheory.isIso_of_reflects_iso, Opposite.op, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
refine_2 : IsIso (X := Functor.obj (Functor.obj coyoneda (op G)) X) (Functor.map (Functor.obj coyoneda (op G)) f)
⊢ IsIso f

Tactic:
suffices IsIso ((coyoneda.obj (op G)).map f) by
      exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj coyoneda (op G))
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
refine_2 :
  Function.Bijective (α := (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))
    (⇑(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))
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  ∀ (b : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) Y)),
    ∃! a : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) X),
      (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))
          a =
        b
⊢ IsIso (X := Functor.obj (Functor.obj coyoneda (op G)) X) (Functor.map (Functor.obj coyoneda (op G)) f)

Tactic:
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]

Premises used: CategoryTheory.isIso_iff_bijective, Function.bijective_iff_existsUnique
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
⊢ IsCodetector.{v₁, u₁} G ↔ Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)

Tactic:
⟨fun hG => ⟨fun f hf => ?_⟩, fun h => (isCodetector_def _).2 fun X Y f hf => ?_⟩

Premises used: Iff.mpr, CategoryTheory.Functor.ReflectsIsomorphisms.mk, CategoryTheory.isCodetector_def, Iff.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
refine_1 :
  ∀ (hG : IsCodetector.{v₁, u₁} G) {A B : Cᵒᵖ} (f : A ⟶ B)
    (hf : IsIso (X := Functor.obj (Functor.obj yoneda G) A) (Functor.map (Functor.obj yoneda G) f)), IsIso f
refine_2 :
  ∀ (h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)) (X Y : C) (f : X ⟶ Y)
    (hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h), IsIso f
⊢ IsCodetector.{v₁, u₁} G ↔ Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)

Tactic:
refine ⟨fun hG => ⟨fun f hf => ?_⟩, fun h => (isCodetector_def _).2 fun X Y f hf => ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCodetector.{v₁, u₁} G
A B : Cᵒᵖ
f : A ⟶ B
hf : IsIso (X := Functor.obj (Functor.obj yoneda G) A) (Functor.map (Functor.obj yoneda G) f)
⊢ IsIso f

Tactic:
(isIso_unop_iff _).1 (hG.def _ ?_)

Premises used: CategoryTheory.isIso_unop_iff, CategoryTheory.IsCodetector.def, Iff.mp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCodetector.{v₁, u₁} G
A B : Cᵒᵖ
f : A ⟶ B
hf : IsIso (X := Functor.obj (Functor.obj yoneda G) A) (Functor.map (Functor.obj yoneda G) f)
refine_1 : ∀ (h : unop B ⟶ G), ∃! h' : unop A ⟶ G, f.unop ≫ h' = h
⊢ IsIso f

Tactic:
refine (isIso_unop_iff _).1 (hG.def _ ?_)

Premises used: CategoryTheory.isIso_unop_iff, CategoryTheory.IsCodetector.def, Iff.mp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCodetector.{v₁, u₁} G
A B : Cᵒᵖ
f : A ⟶ B
hf : IsIso (X := Functor.obj (Functor.obj yoneda G) A) (Functor.map (Functor.obj yoneda G) f)
refine_1 :
  ∀
    (hf :
      Function.Bijective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) A)) (β :=
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) B))
        (⇑(hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj A)) → (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj B)))
    (h : unop B ⟶ G), ∃! h' : unop A ⟶ G, f.unop ≫ h' = h
refine_1₁ refine_1₂ refine_1₃ refine_1₄ :
  ∀
    (hf :
      ∀ (b : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) B)),
        ∃! a : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) A),
          (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f) :
                (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj A)) → (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj B))
              a =
            b)
    (h : unop B ⟶ G), ∃! h' : unop A ⟶ G, f.unop ≫ h' = h
⊢ ∀ (h : unop B ⟶ G), ∃! h' : unop A ⟶ G, f.unop ≫ h' = h

Tactic:
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf

Premises used: CategoryTheory.isIso_iff_bijective, Function.bijective_iff_existsUnique
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
refine_2 : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op X) f.op
⊢ IsIso f

Tactic:
rw [← isIso_op_iff]

Premises used: CategoryTheory.isIso_op_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
this : IsIso (X := Functor.obj (Functor.obj yoneda G) (op Y)) (Functor.map (Functor.obj yoneda G) f.op)
⊢ IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op X) f.op

Tactic:
@isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.yoneda, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
this : IsIso (X := Functor.obj (Functor.obj yoneda G) (op Y)) (Functor.map (Functor.obj yoneda G) f.op)
⊢ IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op X) f.op

Tactic:
exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.yoneda, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
refine_2 : IsIso (X := Functor.obj (Functor.obj yoneda G) (op Y)) (Functor.map (Functor.obj yoneda G) f.op)
⊢ IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op X) f.op

Tactic:
suffices IsIso ((yoneda.obj G).map f.op) by
      exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.ReflectsIsomorphisms.{v₁, u₁, v₁, v₁ + 1} (Functor.obj yoneda G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
refine_2 :
  Function.Bijective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y))) (β :=
    (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X)))
    (⇑(hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op)) :
      (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) → (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  ∀ (b : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X))),
    ∃! a : (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y)),
      (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op) :
            (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) →
              (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))
          a =
        b
⊢ IsIso (X := Functor.obj (Functor.obj yoneda G) (op Y)) (Functor.map (Functor.obj yoneda G) f.op)

Tactic:
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]

Premises used: CategoryTheory.isIso_iff_bijective, Function.bijective_iff_existsUnique
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
G : C
hG : IsDetector.{v₁, u₁} G
⊢ WellPowered.{v₁, v₁, u₁} C

Tactic:
wellPowered_of_isDetecting hG

Premises used: CategoryTheory.wellPowered_of_isDetecting
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
inst_2 : Balanced.{v₁, u₁} C
G : C
hG : IsSeparator.{v₁, u₁} G
⊢ WellPowered.{v₁, v₁, u₁} C

Tactic:
wellPowered_of_isDetecting hG.isDetector

Premises used: CategoryTheory.IsSeparator.isDetector, CategoryTheory.wellPowered_of_isDetecting
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasSeparator.{v₁, u₁} C
⊢ IsSeparator.{v₁, u₁} (separator.{v₁, u₁} C)

Tactic:
HasSeparator.hasSeparator.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.HasSeparator.hasSeparator, CategoryTheory.separator
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
inst_2 : HasSeparator.{v₁, u₁} C
⊢ IsDetector.{v₁, u₁} (separator.{v₁, u₁} C)

Tactic:
isSeparator_separator C |>.isDetector

Premises used: CategoryTheory.IsSeparator.isDetector, CategoryTheory.isSeparator_separator
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasCoseparator.{v₁, u₁} C
⊢ IsCoseparator.{v₁, u₁} (coseparator.{v₁, u₁} C)

Tactic:
HasCoseparator.hasCoseparator.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.coseparator, CategoryTheory.HasCoseparator.hasCoseparator
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
inst_2 : HasCoseparator.{v₁, u₁} C
⊢ IsCodetector.{v₁, u₁} (coseparator.{v₁, u₁} C)

Tactic:
isCoseparator_coseparator C |>.isCodetector

Premises used: CategoryTheory.isCoseparator_coseparator, CategoryTheory.IsCoseparator.isCodetector
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasDetector.{v₁, u₁} C
⊢ IsDetector.{v₁, u₁} (detector.{v₁, u₁} C)

Tactic:
HasDetector.hasDetector.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.detector, CategoryTheory.HasDetector.hasDetector
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasEqualizers.{v₁, u₁} C
inst_2 : HasDetector.{v₁, u₁} C
⊢ IsSeparator.{v₁, u₁} (detector.{v₁, u₁} C)

Tactic:
isDetector_detector C |>.isSeparator

Premises used: CategoryTheory.isDetector_detector, CategoryTheory.IsDetector.isSeparator
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasCodetector.{v₁, u₁} C
⊢ IsCodetector.{v₁, u₁} (codetector.{v₁, u₁} C)

Tactic:
HasCodetector.hasCodetector.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.codetector, CategoryTheory.HasCodetector.hasCodetector
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasCoequalizers.{v₁, u₁} C
inst_2 : HasCodetector.{v₁, u₁} C
⊢ IsCoseparator.{v₁, u₁} (codetector.{v₁, u₁} C)

Tactic:
isCodetector_codetector C |>.isCoseparator

Premises used: CategoryTheory.IsCodetector.isCoseparator, CategoryTheory.isCodetector_codetector
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
inst_2 : HasSeparator.{v₁, u₁} C
⊢ HasDetector.{v₁, u₁} C

Tactic:
⟨_, isDetector_separator C⟩

Premises used: CategoryTheory.HasDetector.mk, CategoryTheory.isDetector_separator, Exists.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasEqualizers.{v₁, u₁} C
inst_2 : HasDetector.{v₁, u₁} C
⊢ HasSeparator.{v₁, u₁} C

Tactic:
⟨_, isSeparator_detector C⟩

Premises used: CategoryTheory.HasSeparator.mk, CategoryTheory.isSeparator_detector, Exists.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
inst_2 : HasCoseparator.{v₁, u₁} C
⊢ HasCodetector.{v₁, u₁} C

Tactic:
⟨_, isCodetector_coseparator C⟩

Premises used: CategoryTheory.HasCodetector.mk, CategoryTheory.isCodetector_coseparator, Exists.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasCoequalizers.{v₁, u₁} C
inst_2 : HasCodetector.{v₁, u₁} C
⊢ HasCoseparator.{v₁, u₁} C

Tactic:
⟨_, isCoseparator_codetector C⟩

Premises used: CategoryTheory.isCoseparator_codetector, CategoryTheory.HasCoseparator.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : HasDetector.{v₁, u₁} C
⊢ WellPowered.{v₁, v₁, u₁} C

Tactic:
isDetector_detector C |> wellPowered_of_isDetector _

Premises used: CategoryTheory.isDetector_detector, CategoryTheory.wellPowered_of_isDetector
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : Balanced.{v₁, u₁} C
inst_4 : HasSeparator.{v₁, u₁} C
⊢ WellPowered.{v₁, v₁, u₁} C

Tactic:
HasSeparator.hasDetector.wellPowered

Premises used: CategoryTheory.HasDetector.wellPowered
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasSeparator.{v₁, u₁} C
α : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ HasSeparator.{v₂, u₂} D

Tactic:
⟨α.functor.obj (separator C), isSeparator_separator C |>.of_equivalence α⟩

Premises used: CategoryTheory.HasSeparator.mk, CategoryTheory.IsSeparator.of_equivalence, CategoryTheory.Equivalence.functor, CategoryTheory.separator, Exists.intro, CategoryTheory.isSeparator_separator, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasCoseparator.{v₁, u₁} C
α : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ HasCoseparator.{v₂, u₂} D

Tactic:
⟨α.functor.obj (coseparator C), isCoseparator_coseparator C |>.of_equivalence α⟩

Premises used: CategoryTheory.isCoseparator_coseparator, CategoryTheory.Equivalence.functor, CategoryTheory.HasCoseparator.mk, CategoryTheory.coseparator, Exists.intro, CategoryTheory.IsCoseparator.of_equivalence, CategoryTheory.Functor.obj