awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsCodetector.{v₁, u₁} (op G) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₁ : IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔
    IsCodetecting.{v₁, u₁} (ObjectProperty.op (ObjectProperty.singleton G))
rw₃ rw₄ :
  IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (op G))
⊢ IsCodetector.{v₁, u₁} (op G) ↔ IsDetector.{v₁, u₁} G

Tactic:
rw [IsDetector, IsCodetector, ← isCodetecting_op_iff, op_singleton]

Premises used: CategoryTheory.ObjectProperty.op_singleton, CategoryTheory.ObjectProperty.isCodetecting_op_iff, CategoryTheory.IsCodetector, CategoryTheory.IsDetector
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsCodetector.{v₁, u₁} (unop G) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₁ : IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
    IsCodetecting.{v₁, u₁} (ObjectProperty.unop (ObjectProperty.singleton G))
rw₃ rw₄ :
  IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
    IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (unop G))
⊢ IsCodetector.{v₁, u₁} (unop G) ↔ IsDetector.{v₁, u₁} G

Tactic:
rw [IsDetector, IsCodetector, ← isCodetecting_unop_iff, unop_singleton]

Premises used: CategoryTheory.ObjectProperty.isCodetecting_unop_iff, CategoryTheory.IsCodetector, CategoryTheory.IsDetector, CategoryTheory.ObjectProperty.unop_singleton
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCodetector.{v₁, u₁} G
rw₁ : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCodetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
    IsDetecting.{v₁, u₁} (ObjectProperty.unop (ObjectProperty.singleton G))
rw₃ rw₄ :
  IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G))
⊢ IsDetector.{v₁, u₁} (unop G) ↔ IsCodetector.{v₁, u₁} G

Tactic:
rw [IsDetector, IsCodetector, ← isDetecting_unop_iff, unop_singleton]

Premises used: CategoryTheory.ObjectProperty.isDetecting_unop_iff, CategoryTheory.IsCodetector, CategoryTheory.IsDetector, CategoryTheory.ObjectProperty.unop_singleton
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasEqualizers.{v₁, u₁} C
G : C
⊢ IsDetector.{v₁, u₁} G → IsSeparator.{v₁, u₁} G

Tactic:
ObjectProperty.IsDetecting.isSeparating

Premises used: CategoryTheory.IsSeparator, CategoryTheory.ObjectProperty.IsDetecting.isSeparating, CategoryTheory.IsDetector
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasCoequalizers.{v₁, u₁} C
G : C
⊢ IsCodetector.{v₁, u₁} G → IsCoseparator.{v₁, u₁} G

Tactic:
ObjectProperty.IsCodetecting.isCoseparating

Premises used: CategoryTheory.ObjectProperty.IsCodetecting.isCoseparating, CategoryTheory.IsCoseparator, CategoryTheory.IsCodetector
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
G : C
⊢ IsSeparator.{v₁, u₁} G → IsDetector.{v₁, u₁} G

Tactic:
ObjectProperty.IsSeparating.isDetecting

Premises used: CategoryTheory.IsSeparator, CategoryTheory.ObjectProperty.IsSeparating.isDetecting, CategoryTheory.IsDetector
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
G : C
⊢ IsCoseparator.{v₁, u₁} G → IsCodetector.{v₁, u₁} G

Tactic:
ObjectProperty.IsCoseparating.isCodetecting

Premises used: CategoryTheory.ObjectProperty.IsCoseparating.isCodetecting, CategoryTheory.IsCoseparator, CategoryTheory.IsCodetector
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsSeparator.{v₁, u₁} G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
H : C
hH : ObjectProperty.singleton.{v₁, u₁} G H
h : H ⟶ X
obtain : ∀ (hH : ObjectProperty.singleton.{v₁, u₁} G G) (h : G ⟶ X), h ≫ f = h ≫ g
⊢ h ≫ f = h ≫ g

Tactic:
obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH

Premises used: CategoryTheory.ObjectProperty.singleton_iff, Iff.mp, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsSeparator.{v₁, u₁} G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
hH : ObjectProperty.singleton.{v₁, u₁} G G
h : G ⟶ X
⊢ h ≫ f = h ≫ g

Tactic:
hfg h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsSeparator.{v₁, u₁} G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
hH : ObjectProperty.singleton.{v₁, u₁} G G
h : G ⟶ X
⊢ h ≫ f = h ≫ g

Tactic:
exact hfg h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g
x x_1 : C
x_2 x_3 : x ⟶ x_1
hfg : ∀ (G_1 : C), ObjectProperty.singleton.{v₁, u₁} G G_1 → ∀ (h : G_1 ⟶ x), h ≫ x_2 = h ≫ x_3
x_4 : G ⟶ x
⊢ ObjectProperty.singleton.{v₁, u₁} G G

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
⊢ IsSeparator.{v₁, u₁} G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g

Tactic:
(isSeparator_def _).1

Premises used: CategoryTheory.isSeparator_def, Iff.mp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCoseparator.{v₁, u₁} G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
H : C
hH : ObjectProperty.singleton.{v₁, u₁} G H
h : Y ⟶ H
obtain : ∀ (hH : ObjectProperty.singleton.{v₁, u₁} G G) (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f ≫ h = g ≫ h

Tactic:
obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH

Premises used: CategoryTheory.ObjectProperty.singleton_iff, Iff.mp, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCoseparator.{v₁, u₁} G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
hH : ObjectProperty.singleton.{v₁, u₁} G G
h : Y ⟶ G
⊢ f ≫ h = g ≫ h

Tactic:
hfg h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCoseparator.{v₁, u₁} G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
hH : ObjectProperty.singleton.{v₁, u₁} G G
h : Y ⟶ G
⊢ f ≫ h = g ≫ h

Tactic:
exact hfg h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g
x x_1 : C
x_2 x_3 : x ⟶ x_1
hfg : ∀ (G_1 : C), ObjectProperty.singleton.{v₁, u₁} G G_1 → ∀ (h : x_1 ⟶ G_1), x_2 ≫ h = x_3 ≫ h
x_4 : x_1 ⟶ G
⊢ ObjectProperty.singleton.{v₁, u₁} G G

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
⊢ IsCoseparator.{v₁, u₁} G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g

Tactic:
(isCoseparator_def _).1

Premises used: CategoryTheory.isCoseparator_def, Iff.mp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsDetector.{v₁, u₁} G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
H : C
hH : ObjectProperty.singleton.{v₁, u₁} G H
h : H ⟶ Y
obtain : ∀ (hH : ObjectProperty.singleton.{v₁, u₁} G G) (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
⊢ ∃! h' : H ⟶ X, h' ≫ f = h

Tactic:
obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH

Premises used: CategoryTheory.ObjectProperty.singleton_iff, Iff.mp, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsDetector.{v₁, u₁} G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
hH : ObjectProperty.singleton.{v₁, u₁} G G
h : G ⟶ Y
⊢ ∃! h' : G ⟶ X, 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
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
hH : ObjectProperty.singleton.{v₁, u₁} G G
h : G ⟶ Y
⊢ ∃! h' : G ⟶ X, h' ≫ f = h

Tactic:
exact hf h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h) → IsIso f
x x_1 : C
x_2 : x ⟶ x_1
hf : ∀ (G_1 : C), ObjectProperty.singleton.{v₁, u₁} G G_1 → ∀ (h : G_1 ⟶ x_1), ∃! h' : G_1 ⟶ x, h' ≫ x_2 = h
x_3 : G ⟶ x_1
⊢ ObjectProperty.singleton.{v₁, u₁} G G

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
⊢ IsDetector.{v₁, u₁} G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h) → IsIso f

Tactic:
(isDetector_def _).1

Premises used: Iff.mp, CategoryTheory.isDetector_def
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCodetector.{v₁, u₁} G
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
H : C
hH : ObjectProperty.singleton.{v₁, u₁} G H
h : X ⟶ H
obtain : ∀ (hH : ObjectProperty.singleton.{v₁, u₁} G G) (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
⊢ ∃! h' : Y ⟶ H, f ≫ h' = h

Tactic:
obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH

Premises used: CategoryTheory.ObjectProperty.singleton_iff, Iff.mp, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCodetector.{v₁, u₁} G
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
hH : ObjectProperty.singleton.{v₁, u₁} G G
h : X ⟶ G
⊢ ∃! h' : Y ⟶ G, f ≫ h' = h

Tactic:
hf h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCodetector.{v₁, u₁} G
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
hH : ObjectProperty.singleton.{v₁, u₁} G G
h : X ⟶ G
⊢ ∃! h' : Y ⟶ G, f ≫ h' = h

Tactic:
exact hf h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h) → IsIso f
x x_1 : C
x_2 : x ⟶ x_1
hf : ∀ (G_1 : C), ObjectProperty.singleton.{v₁, u₁} G G_1 → ∀ (h : x ⟶ G_1), ∃! h' : x_1 ⟶ G_1, x_2 ≫ h' = h
x_3 : x ⟶ G
⊢ ObjectProperty.singleton.{v₁, u₁} G G

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
⊢ IsCodetector.{v₁, u₁} G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h) → IsIso f

Tactic:
(isCodetector_def _).1

Premises used: CategoryTheory.isCodetector_def, Iff.mp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h_1 : Functor.Faithful.{v₁, v₁, u₁, v₁ + 1} (Functor.obj coyoneda (op G))
x x_1 : C
x_2 x_3 : x ⟶ x_1
hfg : ∀ (h : G ⟶ x), h ≫ x_2 = h ≫ x_3
h :
  ∀ (x_4 : Functor.obj (Functor.obj coyoneda (op G)) x),
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) x_2)) x_4 =
      TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) x_3)) x_4
⊢ Eq (α := Functor.obj (Functor.obj coyoneda (op G)) x ⟶ Functor.obj (Functor.obj coyoneda (op G)) x_1)
    (Functor.map (Functor.obj coyoneda (op G)) x_2) (Functor.map (Functor.obj coyoneda (op G)) x_3)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.Faithful.{v₁, v₁, u₁, v₁ + 1} (Functor.obj coyoneda (op G))
x x_1 : C
x_2 x_3 : x ⟶ x_1
hfg : ∀ (h : G ⟶ x), h ≫ x_2 = h ≫ x_3
x_4 : Functor.obj (Functor.obj coyoneda (op G)) x
⊢ TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) x_2)) x_4 =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) x_3)) x_4

Tactic:
apply hfg
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h_1 : Functor.Faithful.{v₁, v₁, u₁, v₁ + 1} (Functor.obj yoneda G)
x x_1 : C
x_2 x_3 : x ⟶ x_1
hfg : ∀ (h : x_1 ⟶ G), x_2 ≫ h = x_3 ≫ h
h :
  ∀ (x_4 : Functor.obj (Functor.obj yoneda G) (op x_1)),
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) x_2.op)) x_4 =
      TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) x_3.op)) x_4
⊢ Eq (α := Functor.obj (Functor.obj yoneda G) (op x_1) ⟶ Functor.obj (Functor.obj yoneda G) (op x))
    (Functor.map (Functor.obj yoneda G) x_2.op) (Functor.map (Functor.obj yoneda G) x_3.op)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.Faithful.{v₁, v₁, u₁, v₁ + 1} (Functor.obj yoneda G)
x x_1 : C
x_2 x_3 : x ⟶ x_1
hfg : ∀ (h : x_1 ⟶ G), x_2 ≫ h = x_3 ≫ h
x_4 : Functor.obj (Functor.obj yoneda G) (op x_1)
⊢ TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) x_2.op)) x_4 =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) x_3.op)) x_4

Tactic:
apply hfg
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
rw :
  (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) ↔
    ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
⊢ IsSeparator.{v₁, u₁} G ↔
    ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)

Tactic:
rw [isSeparator_def]

Premises used: CategoryTheory.isSeparator_def
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) ↔
    ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)

Tactic:
⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩

Premises used: CategoryTheory.Epi.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
refine_1 :
  ∀ (h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) (A : C) {Z : C} (u v : A ⟶ Z)
    (huv :
      Eq (α := (∐ fun (f : G ⟶ A) ↦ G) ⟶ Z) ((Sigma.desc fun (f : G ⟶ A) ↦ f) ≫ u)
        ((Sigma.desc fun (f : G ⟶ A) ↦ f) ≫ v))
    (i : G ⟶ A), i ≫ u = i ≫ v
refine_2 :
  ∀ (h : ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f))
    (X Y : C) (f g : X ⟶ Y) (hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g), f = g
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) ↔
    ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)

Tactic:
refine ⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g
A Z : C
u v : A ⟶ Z
huv :
  Eq (α := (∐ fun (f : G ⟶ A) ↦ G) ⟶ Z) ((Sigma.desc fun (f : G ⟶ A) ↦ f) ≫ u) ((Sigma.desc fun (f : G ⟶ A) ↦ f) ≫ v)
i : G ⟶ A
⊢ i ≫ u = i ≫ v

Tactic:
simpa using Sigma.ι _ i ≫= huv

Premises used: CategoryTheory.Limits.Sigma.ι
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
h : ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ X) ↦ G) (Y := X) (Sigma.desc fun (f : G ⟶ X) ↦ f)

Tactic:
haveI := h X
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
h : ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ X) ↦ G) (Y := X) (Sigma.desc fun (f : G ⟶ X) ↦ f)
⊢ f = g

Tactic:
(cancel_epi (Sigma.desc fun f : G ⟶ X => f)).1 (colimit.hom_ext fun j => ?_)

Premises used: Iff.mp, CategoryTheory.Limits.Sigma.desc, CategoryTheory.cancel_epi, CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
h : ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ X) ↦ G) (Y := X) (Sigma.desc fun (f : G ⟶ X) ↦ f)
refine_2 :
  ∀ (j : Discrete (G ⟶ X)),
    Eq (α := Functor.obj (Discrete.functor fun (f : G ⟶ X) ↦ G) j ⟶ Y)
      (CategoryStruct.comp (Y :=
        colimit.{v₁, v₁, v₁, u₁} (J := Discrete (G ⟶ X)) (Discrete.functor fun (f : G ⟶ X) ↦ G))
        (colimit.ι (Discrete.functor fun (f : G ⟶ X) ↦ G) j) ((Sigma.desc fun (f : G ⟶ X) ↦ f) ≫ f))
      (CategoryStruct.comp (Y :=
        colimit.{v₁, v₁, v₁, u₁} (J := Discrete (G ⟶ X)) (Discrete.functor fun (f : G ⟶ X) ↦ G))
        (colimit.ι (Discrete.functor fun (f : G ⟶ X) ↦ G) j) ((Sigma.desc fun (f : G ⟶ X) ↦ f) ≫ g))
⊢ f = g

Tactic:
refine (cancel_epi (Sigma.desc fun f : G ⟶ X => f)).1 (colimit.hom_ext fun j => ?_)

Premises used: Iff.mp, CategoryTheory.Limits.Sigma.desc, CategoryTheory.cancel_epi, CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
h : ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ X) ↦ G) (Y := X) (Sigma.desc fun (f : G ⟶ X) ↦ f)
j : Discrete (G ⟶ X)
⊢ Eq (α := Functor.obj (Discrete.functor fun (f : G ⟶ X) ↦ G) j ⟶ Y)
    (CategoryStruct.comp (Y := colimit.{v₁, v₁, v₁, u₁} (J := Discrete (G ⟶ X)) (Discrete.functor fun (f : G ⟶ X) ↦ G))
      (colimit.ι (Discrete.functor fun (f : G ⟶ X) ↦ G) j) ((Sigma.desc fun (f : G ⟶ X) ↦ f) ≫ f))
    (CategoryStruct.comp (Y := colimit.{v₁, v₁, v₁, u₁} (J := Discrete (G ⟶ X)) (Discrete.functor fun (f : G ⟶ X) ↦ G))
      (colimit.ι (Discrete.functor fun (f : G ⟶ X) ↦ G) j) ((Sigma.desc fun (f : G ⟶ X) ↦ f) ≫ g))

Tactic:
simpa using hh j.as

Premises used: CategoryTheory.Discrete.as
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasProduct.{v₁, v₁, u₁} (C := C) fun (x : A ⟶ G) ↦ G
rw :
  (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) ↔
    ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f)
⊢ IsCoseparator.{v₁, u₁} G ↔
    ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f)

Tactic:
rw [isCoseparator_def]

Premises used: CategoryTheory.isCoseparator_def
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasProduct.{v₁, v₁, u₁} (C := C) fun (x : A ⟶ G) ↦ G
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) ↔
    ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f)

Tactic:
⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩

Premises used: CategoryTheory.Mono.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasProduct.{v₁, v₁, u₁} (C := C) fun (x : A ⟶ G) ↦ G
refine_1 :
  ∀ (h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) (A : C) {Z : C} (u v : Z ⟶ A)
    (huv : Eq (α := Z ⟶ ∏ᶜ fun (f : A ⟶ G) ↦ G) (u ≫ Pi.lift fun (f : A ⟶ G) ↦ f) (v ≫ Pi.lift fun (f : A ⟶ G) ↦ f))
    (i : A ⟶ G), u ≫ i = v ≫ i
refine_2 :
  ∀ (h : ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f))
    (X Y : C) (f g : X ⟶ Y) (hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h), f = g
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) ↔
    ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f)

Tactic:
refine ⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasProduct.{v₁, v₁, u₁} (C := C) fun (x : A ⟶ G) ↦ G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g
A Z : C
u v : Z ⟶ A
huv : Eq (α := Z ⟶ ∏ᶜ fun (f : A ⟶ G) ↦ G) (u ≫ Pi.lift fun (f : A ⟶ G) ↦ f) (v ≫ Pi.lift fun (f : A ⟶ G) ↦ f)
i : A ⟶ G
⊢ u ≫ i = v ≫ i

Tactic:
simpa using huv =≫ Pi.π _ i

Premises used: CategoryTheory.Limits.Pi.π
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasProduct.{v₁, v₁, u₁} (C := C) fun (x : A ⟶ G) ↦ G
h : ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ Mono.{v₁, u₁} (C := C) (X := Y) (Y := ∏ᶜ fun (f : Y ⟶ G) ↦ G) (Pi.lift fun (f : Y ⟶ G) ↦ f)

Tactic:
haveI := h Y
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasProduct.{v₁, v₁, u₁} (C := C) fun (x : A ⟶ G) ↦ G
h : ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono.{v₁, u₁} (C := C) (X := Y) (Y := ∏ᶜ fun (f : Y ⟶ G) ↦ G) (Pi.lift fun (f : Y ⟶ G) ↦ f)
⊢ f = g

Tactic:
(cancel_mono (Pi.lift fun f : Y ⟶ G => f)).1 (limit.hom_ext fun j => ?_)

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.limit.hom_ext, Iff.mp, CategoryTheory.Limits.Pi.lift
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasProduct.{v₁, v₁, u₁} (C := C) fun (x : A ⟶ G) ↦ G
h : ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono.{v₁, u₁} (C := C) (X := Y) (Y := ∏ᶜ fun (f : Y ⟶ G) ↦ G) (Pi.lift fun (f : Y ⟶ G) ↦ f)
refine_2 :
  ∀ (j : Discrete (Y ⟶ G)),
    Eq (α := X ⟶ Functor.obj (Discrete.functor fun (f : Y ⟶ G) ↦ G) j)
      (CategoryStruct.comp (Y := limit.{v₁, v₁, v₁, u₁} (J := Discrete (Y ⟶ G)) (Discrete.functor fun (f : Y ⟶ G) ↦ G))
        (f ≫ Pi.lift fun (f : Y ⟶ G) ↦ f) (limit.π (Discrete.functor fun (f : Y ⟶ G) ↦ G) j))
      (CategoryStruct.comp (Y := limit.{v₁, v₁, v₁, u₁} (J := Discrete (Y ⟶ G)) (Discrete.functor fun (f : Y ⟶ G) ↦ G))
        (g ≫ Pi.lift fun (f : Y ⟶ G) ↦ f) (limit.π (Discrete.functor fun (f : Y ⟶ G) ↦ G) j))
⊢ f = g

Tactic:
refine (cancel_mono (Pi.lift fun f : Y ⟶ G => f)).1 (limit.hom_ext fun j => ?_)

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.limit.hom_ext, Iff.mp, CategoryTheory.Limits.Pi.lift