awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasSeparator.{v₁, u₁} Cᵒᵖ ↔ HasCoseparator.{v₁, u₁} C

Tactic:
⟨fun ⟨G, hG⟩ => ⟨unop G, (isCoseparator_unop_iff G).mpr hG⟩,
   fun ⟨G, hG⟩ => ⟨op G, (isSeparator_op_iff G).mpr hG⟩⟩

Premises used: Iff.mpr, CategoryTheory.HasSeparator, CategoryTheory.HasSeparator.mk, Opposite, CategoryTheory.HasCoseparator, _private.0.CategoryTheory.hasSeparator_op_iff.match_2, Opposite.op, CategoryTheory.HasCoseparator.mk, CategoryTheory.isSeparator_op_iff, Iff.intro, Exists.intro, _private.0.CategoryTheory.hasSeparator_op_iff.match_1, Opposite.unop, CategoryTheory.isCoseparator_unop_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasCoseparator.{v₁, u₁} Cᵒᵖ ↔ HasSeparator.{v₁, u₁} C

Tactic:
⟨fun ⟨G, hG⟩ => ⟨unop G, (isSeparator_unop_iff G).mpr hG⟩,
   fun ⟨G, hG⟩ => ⟨op G, (isCoseparator_op_iff G).mpr hG⟩⟩

Premises used: Iff.mpr, CategoryTheory.HasSeparator, CategoryTheory.HasSeparator.mk, Opposite, CategoryTheory.HasCoseparator, _private.0.CategoryTheory.hasCoseparator_op_iff.match_1, _private.0.CategoryTheory.hasCoseparator_op_iff.match_2, Opposite.op, CategoryTheory.HasCoseparator.mk, Iff.intro, Exists.intro, CategoryTheory.isCoseparator_op_iff, Opposite.unop, CategoryTheory.isSeparator_unop_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasDetector.{v₁, u₁} Cᵒᵖ ↔ HasCodetector.{v₁, u₁} C

Tactic:
⟨fun ⟨G, hG⟩ => ⟨unop G, (isCodetector_unop_iff G).mpr hG⟩,
   fun ⟨G, hG⟩ => ⟨op G, (isDetector_op_iff G).mpr hG⟩⟩

Premises used: Iff.mpr, CategoryTheory.HasCodetector.mk, CategoryTheory.HasDetector.mk, Opposite, CategoryTheory.isCodetector_unop_iff, CategoryTheory.HasCodetector, _private.0.CategoryTheory.hasDetector_op_iff.match_2, Opposite.op, Iff.intro, Exists.intro, _private.0.CategoryTheory.hasDetector_op_iff.match_1, CategoryTheory.HasDetector, CategoryTheory.isDetector_op_iff, Opposite.unop
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasCodetector.{v₁, u₁} Cᵒᵖ ↔ HasDetector.{v₁, u₁} C

Tactic:
⟨fun ⟨G, hG⟩ => ⟨unop G, (isDetector_unop_iff G).mpr hG⟩,
   fun ⟨G, hG⟩ => ⟨op G, (isCodetector_op_iff G).mpr hG⟩⟩

Premises used: Iff.mpr, CategoryTheory.HasCodetector.mk, CategoryTheory.HasDetector.mk, _private.0.CategoryTheory.hasCodetector_op_iff.match_2, Opposite, CategoryTheory.isDetector_unop_iff, CategoryTheory.HasCodetector, CategoryTheory.isCodetector_op_iff, Opposite.op, Iff.intro, Exists.intro, _private.0.CategoryTheory.hasCodetector_op_iff.match_1, CategoryTheory.HasDetector, Opposite.unop
-- 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
⊢ HasCoseparator.{v₁, u₁} Cᵒᵖ

Tactic:
simp [*]
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasSeparator.{v₁, u₁} Cᵒᵖ
⊢ HasCoseparator.{v₁, u₁} C

Tactic:
simp_all
-- 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
⊢ HasSeparator.{v₁, u₁} Cᵒᵖ

Tactic:
simp [*]
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasCoseparator.{v₁, u₁} Cᵒᵖ
⊢ HasSeparator.{v₁, u₁} C

Tactic:
simp_all
-- 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 : HasDetector.{v₁, u₁} C
⊢ HasCodetector.{v₁, u₁} Cᵒᵖ

Tactic:
simp [*]
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasDetector.{v₁, u₁} Cᵒᵖ
⊢ HasCodetector.{v₁, u₁} C

Tactic:
simp_all
-- 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 : HasCodetector.{v₁, u₁} C
⊢ HasDetector.{v₁, u₁} Cᵒᵖ

Tactic:
simp [*]
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasCodetector.{v₁, u₁} Cᵒᵖ
⊢ HasDetector.{v₁, u₁} C

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Generator.HomologicalComplex
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
α : Type t
X : α → C
hX : ObjectProperty.IsSeparating.{v, u} (ObjectProperty.ofObj X)
K L : HomologicalComplex.{v, u, w} C c
f g : K ⟶ L
h :
  ∀ (G : HomologicalComplex.{v, u, w} C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g
h₁ : ∀ (j : ι), f.f j = g.f j
⊢ f = g

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Generator.HomologicalComplex
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
α : Type t
X : α → C
hX : ObjectProperty.IsSeparating.{v, u} (ObjectProperty.ofObj X)
K L : HomologicalComplex.{v, u, w} C c
f g : K ⟶ L
h :
  ∀ (G : HomologicalComplex.{v, u, w} C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
h₁ : ∀ (G : C), ObjectProperty.ofObj.{v, u, t} X G → ∀ (h : G ⟶ K.X j), h ≫ f.f j = h ≫ g.f j
⊢ f.f j = g.f j

Tactic:
apply hX
-- Module: Mathlib.CategoryTheory.Generator.HomologicalComplex
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
α : Type t
X : α → C
hX : ObjectProperty.IsSeparating.{v, u} (ObjectProperty.ofObj X)
K L : HomologicalComplex.{v, u, w} C c
f g : K ⟶ L
h :
  ∀ (G : HomologicalComplex.{v, u, w} C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
h₁ :
  ∀
    (H :
      Functor.CorepresentableBy (C := HomologicalComplex.{v, u, w} C c)
        (eval C c j ⋙ Functor.obj coyoneda (Opposite.op (X a))) (evalCompCoyonedaCorepresentative c (X a) j)),
    p ≫ f.f j = p ≫ g.f j
⊢ p ≫ f.f j = p ≫ g.f j

Tactic:
have H := evalCompCoyonedaCorepresentable c (X a) j
-- Module: Mathlib.CategoryTheory.Generator.HomologicalComplex
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
α : Type t
X : α → C
hX : ObjectProperty.IsSeparating.{v, u} (ObjectProperty.ofObj X)
K L : HomologicalComplex.{v, u, w} C c
f g : K ⟶ L
h :
  ∀ (G : HomologicalComplex.{v, u, w} C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
H :
  Functor.CorepresentableBy (C := HomologicalComplex.{v, u, w} C c)
    (eval C c j ⋙ Functor.obj coyoneda (Opposite.op (X a))) (evalCompCoyonedaCorepresentative c (X a) j)
h₁ :
  Eq (α := evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
    ((Equiv.symm H.homEquiv :
          (a_1 : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).obj L) →
            evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
        (p ≫ f.f j) :
      evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
    ((Equiv.symm H.homEquiv :
          (a_1 : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).obj L) →
            evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
        (p ≫ g.f j) :
      evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
⊢ p ≫ f.f j = p ≫ g.f j

Tactic:
apply H.homEquiv.symm.injective

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.Generator.HomologicalComplex
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
α : Type t
X : α → C
hX : ObjectProperty.IsSeparating.{v, u} (ObjectProperty.ofObj X)
K L : HomologicalComplex.{v, u, w} C c
f g : K ⟶ L
h :
  ∀ (G : HomologicalComplex.{v, u, w} C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
H :
  Functor.CorepresentableBy (C := HomologicalComplex.{v, u, w} C c)
    (eval C c j ⋙ Functor.obj coyoneda (Opposite.op (X a))) (evalCompCoyonedaCorepresentative c (X a) j)
⊢ Eq (α := evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
    ((Equiv.symm H.homEquiv :
          (a_1 : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).obj L) →
            evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
        (p ≫ f.f j) :
      evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
    ((Equiv.symm H.homEquiv :
          (a_1 : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).obj L) →
            evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
        (p ≫ g.f j) :
      evalCompCoyonedaCorepresentative c (X a) j ⟶ L)

Tactic:
simpa only [H.homEquiv_symm_comp] using h _
    (ObjectProperty.ofObj_apply _ ⟨a, j⟩) (H.homEquiv.symm p)

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv, CategoryTheory.ObjectProperty.ofObj_apply, CategoryTheory.Functor.CorepresentableBy.homEquiv_symm_comp, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Generator.HomologicalComplex
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasCoproductsOfShape.{w, u, v} ι C
inst_3 : Preadditive.{v, u} C
inst_4 : HasZeroObject.{v, u} C
X : C
hX : IsSeparator.{v, u} X
φ : (i : ι) → HomologicalComplex.{v, u, w} C c := fun (i : ι) ↦ separatingFamily c (fun (x : Unit) ↦ X) (PUnit.unit, i)
⊢ ObjectProperty.IsSeparating.{v, u} (C := C) (ObjectProperty.ofObj fun (x : Unit) ↦ X)

Tactic:
simpa using hX
-- Module: Mathlib.CategoryTheory.Generator.HomologicalComplex
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasCoproductsOfShape.{w, u, v} ι C
inst_3 : Preadditive.{v, u} C
inst_4 : HasZeroObject.{v, u} C
X : C
hX : IsSeparator.{v, u} X
φ : (i : ι) → HomologicalComplex.{v, u, w} C c := fun (i : ι) ↦ separatingFamily c (fun (x : Unit) ↦ X) (PUnit.unit, i)
refine :
  IsColimit (J := Discrete (Unit × ι)) (F := Discrete.functor (separatingFamily c fun (x : Unit) ↦ X))
    (Cofan.mk (∐ φ) fun (x : Unit × ι) ↦
      match (motive := (x : Unit × ι) → separatingFamily c (fun (x : Unit) ↦ X) x ⟶ ∐ φ) x with
      | (fst, i) => Sigma.ι φ i)
⊢ IsSeparator (C := HomologicalComplex.{v, u, w} C c)
    (∐ fun (i : ι) ↦ separatingFamily c (fun (x : Unit) ↦ X) (PUnit.unit, i))

Tactic:
refine isSeparator_of_isColimit_cofan
    (isSeparating_separatingFamily c (X := fun (_ : Unit) ↦ X) (by simpa using hX))
      (c := Cofan.mk (∐ φ) (fun ⟨_, i⟩ ↦ Sigma.ι φ i)) ?_

Premises used: HomologicalComplex.isSeparating_separatingFamily, CategoryTheory.isSeparator_of_isColimit_cofan
-- Module: Mathlib.CategoryTheory.Generator.HomologicalComplex
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasCoproductsOfShape.{w, u, v} ι C
inst_3 : Preadditive.{v, u} C
inst_4 : HasZeroObject.{v, u} C
X : C
hX : IsSeparator.{v, u} X
φ : (i : ι) → HomologicalComplex.{v, u, w} C c := fun (i : ι) ↦ separatingFamily c (fun (x : Unit) ↦ X) (PUnit.unit, i)
⊢ IsColimit (J := Discrete (Unit × ι)) (F := Discrete.functor (separatingFamily c fun (x : Unit) ↦ X))
    (Cofan.mk (∐ φ) fun (x : Unit × ι) ↦
      match (motive := (x : Unit × ι) → separatingFamily c (fun (x : Unit) ↦ X) x ⟶ ∐ φ) x with
      | (fst, i) => Sigma.ι φ i)

Tactic:
exact IsColimit.ofWhiskerEquivalence
    (Discrete.equivalence (Equiv.punitProd.{0} ι).symm) (coproductIsCoproduct φ)
-- Module: Mathlib.CategoryTheory.Generator.HomologicalComplex
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasCoproductsOfShape.{w, u, v} ι C
inst_3 : Preadditive.{v, u} C
inst_4 : HasZeroObject.{v, u} C
inst_5 : HasSeparator.{v, u} C
⊢ HasSeparator (HomologicalComplex.{v, u, w} C c)

Tactic:
⟨_, isSeparator_coproduct_separatingFamily c (isSeparator_separator C)⟩

Premises used: CategoryTheory.HasSeparator.mk, HomologicalComplex.isSeparator_coproduct_separatingFamily, Exists.intro, CategoryTheory.isSeparator_separator
-- Module: Mathlib.CategoryTheory.Generator.Indization
Goal:
C : Type u
inst : Category.{v, u} C
⊢ ObjectProperty.IsSeparating (C := Ind.{v, u} C) (ObjectProperty.ofObj (Functor.obj Ind.yoneda))

Tactic:
fun X Y f g h => (cancel_epi (Ind.colimitPresentationCompYoneda X).hom).1 ?_

Premises used: CategoryTheory.Ind.colimitPresentationCompYoneda, Iff.mp, CategoryTheory.ObjectProperty.IsSeparating, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Generator.Indization
Goal:
C : Type u
inst : Category.{v, u} C
refine :
  ∀ (X Y : Ind.{v, u} C) (f g : X ⟶ Y)
    (h : ∀ (G : Ind.{v, u} C), ObjectProperty.ofObj (Functor.obj Ind.yoneda) G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g),
    X.colimitPresentationCompYoneda.hom ≫ f = X.colimitPresentationCompYoneda.hom ≫ g
⊢ ObjectProperty.IsSeparating (C := Ind.{v, u} C) (ObjectProperty.ofObj (Functor.obj Ind.yoneda))

Tactic:
refine fun X Y f g h => (cancel_epi (Ind.colimitPresentationCompYoneda X).hom).1 ?_

Premises used: CategoryTheory.Ind.colimitPresentationCompYoneda, Iff.mp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Generator.Indization
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Ind.{v, u} C
f g : X ⟶ Y
h : ∀ (G : Ind.{v, u} C), ObjectProperty.ofObj (Functor.obj Ind.yoneda) G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
i : X.presentation.I
⊢ colimit.ι (X.presentation.F ⋙ Ind.yoneda) i ≫ X.colimitPresentationCompYoneda.hom ≫ f =
    colimit.ι (X.presentation.F ⋙ Ind.yoneda) i ≫ X.colimitPresentationCompYoneda.hom ≫ g

Tactic:
simp [← Category.assoc, h]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Generator.Indization
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Ind.{v, u} C
f g : X ⟶ Y
h : ∀ (G : Ind.{v, u} C), ObjectProperty.ofObj (Functor.obj Ind.yoneda) G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ X.colimitPresentationCompYoneda.hom ≫ f = X.colimitPresentationCompYoneda.hom ≫ g

Tactic:
exact colimit.hom_ext (fun i => by simp [← Category.assoc, h])

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Generator.Indization
Goal:
C : Type u
inst : SmallCategory C
inst_1 : Preadditive C
inst_2 : HasFiniteColimits C
⊢ IsSeparator.{u, u + 1} (C := Ind C) (∐ Functor.obj Ind.yoneda)

Tactic:
Ind.isSeparating_range_yoneda.isSeparator_coproduct

Premises used: CategoryTheory.Ind.isSeparating_range_yoneda, CategoryTheory.ObjectProperty.IsSeparating.isSeparator_coproduct
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : ObjectProperty.{v, u} C
h𝒢 : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = 0
⊢ ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ 0

Tactic:
simpa only [Limits.comp_zero] using hf

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : ObjectProperty.{v, u} C
h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ (f - g) = 0

Tactic:
simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg

Premises used: sub_eq_zero, CategoryTheory.Preadditive.comp_sub
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : ObjectProperty.{v, u} C
h𝒢 : P.IsCoseparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = 0
⊢ ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = 0 ≫ h

Tactic:
simpa only [Limits.zero_comp] using hf

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : ObjectProperty.{v, u} C
h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ ∀ (G : C), P G → ∀ (h : Y ⟶ G), (f - g) ≫ h = 0

Tactic:
simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg

Premises used: sub_eq_zero, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
hG : IsSeparator.{v, u} G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ X), h ≫ f = 0
⊢ ∀ (h : G ⟶ X), h ≫ f = h ≫ 0

Tactic:
simpa only [Limits.comp_zero] using hf

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ ∀ (h : G ⟶ X), h ≫ (f - g) = 0

Tactic:
simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg

Premises used: sub_eq_zero, CategoryTheory.Preadditive.comp_sub
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
hG : IsCoseparator.{v, u} G
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ G), f ≫ h = 0
⊢ ∀ (h : Y ⟶ G), f ≫ h = 0 ≫ h

Tactic:
simpa only [Limits.zero_comp] using hf

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ ∀ (h : Y ⟶ G), (f - g) ≫ h = 0

Tactic:
simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg

Premises used: sub_eq_zero, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
rw :
  Functor.Faithful
      (Functor.obj preadditiveCoyoneda (op G) ⋙
        forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier)) ↔
    Functor.Faithful.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op G))
⊢ IsSeparator.{v, u} G ↔ Functor.Faithful.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op G))

Tactic:
rw [isSeparator_iff_faithful_coyoneda_obj, ← whiskering_preadditiveCoyoneda, Functor.comp_obj,
    Functor.whiskeringRight_obj_obj]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.isSeparator_iff_faithful_coyoneda_obj, CategoryTheory.Functor.whiskeringRight_obj_obj, CategoryTheory.whiskering_preadditiveCoyoneda
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
⊢ Functor.Faithful
      (Functor.obj preadditiveCoyoneda (op G) ⋙
        forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier)) ↔
    Functor.Faithful.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op G))

Tactic:
⟨fun h => Functor.Faithful.of_comp _ (forget AddCommGrpCat),
    fun h => Functor.Faithful.comp _ _⟩

Premises used: CategoryTheory.Functor.Faithful.of_comp, AddCommGrpCat, CategoryTheory.Functor.Faithful.comp, Opposite.op, Iff.intro, CategoryTheory.forget, CategoryTheory.preadditiveCoyoneda, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
⊢ Functor.Faithful
      (Functor.obj preadditiveCoyoneda (op G) ⋙
        forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier)) ↔
    Functor.Faithful.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op G))

Tactic:
exact ⟨fun h => Functor.Faithful.of_comp _ (forget AddCommGrpCat),
    fun h => Functor.Faithful.comp _ _⟩
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
rw :
  Functor.Faithful
      (preadditiveCoyonedaObj (unop (op G)) ⋙
        forget₂ (ModuleCat (End (unop (op G)))ᵐᵒᵖ) (FC := fun (x1 x2 : ModuleCat (End (unop (op G)))ᵐᵒᵖ) ↦
          LinearMap (R := (End (unop (op G)))ᵐᵒᵖ) (RingHom.id (End (unop (op G)))ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v))
          (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
          (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier)) ↔
    Functor.Faithful.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)
⊢ IsSeparator.{v, u} G ↔ Functor.Faithful.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)

Tactic:
rw [isSeparator_iff_faithful_preadditiveCoyoneda, preadditiveCoyoneda_obj]

Premises used: CategoryTheory.isSeparator_iff_faithful_preadditiveCoyoneda, CategoryTheory.preadditiveCoyoneda_obj
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
⊢ Functor.Faithful
      (preadditiveCoyonedaObj (unop (op G)) ⋙
        forget₂ (ModuleCat (End (unop (op G)))ᵐᵒᵖ) (FC := fun (x1 x2 : ModuleCat (End (unop (op G)))ᵐᵒᵖ) ↦
          LinearMap (R := (End (unop (op G)))ᵐᵒᵖ) (RingHom.id (End (unop (op G)))ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v))
          (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
          (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier)) ↔
    Functor.Faithful.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)

Tactic:
⟨fun h => Functor.Faithful.of_comp _ (forget₂ _ AddCommGrpCat.{v}),
    fun h => Functor.Faithful.comp _ _⟩

Premises used: ModuleCat, MulOpposite, CategoryTheory.Functor.Faithful.of_comp, CategoryTheory.preadditiveCoyonedaObj, CategoryTheory.End, CategoryTheory.forget₂, AddCommGrpCat, CategoryTheory.Functor.Faithful.comp, Opposite.op, Iff.intro, Opposite.unop
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
⊢ Functor.Faithful
      (preadditiveCoyonedaObj (unop (op G)) ⋙
        forget₂ (ModuleCat (End (unop (op G)))ᵐᵒᵖ) (FC := fun (x1 x2 : ModuleCat (End (unop (op G)))ᵐᵒᵖ) ↦
          LinearMap (R := (End (unop (op G)))ᵐᵒᵖ) (RingHom.id (End (unop (op G)))ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v))
          (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
          (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier)) ↔
    Functor.Faithful.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)

Tactic:
exact ⟨fun h => Functor.Faithful.of_comp _ (forget₂ _ AddCommGrpCat.{v}),
    fun h => Functor.Faithful.comp _ _⟩
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
rw :
  Functor.Faithful
      (Functor.obj preadditiveYoneda G ⋙
        forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier)) ↔
    Functor.Faithful.{v, v, u, v + 1} (Functor.obj preadditiveYoneda G)
⊢ IsCoseparator.{v, u} G ↔ Functor.Faithful.{v, v, u, v + 1} (Functor.obj preadditiveYoneda G)

Tactic:
rw [isCoseparator_iff_faithful_yoneda_obj, ← whiskering_preadditiveYoneda, Functor.comp_obj,
    Functor.whiskeringRight_obj_obj]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.whiskering_preadditiveYoneda, CategoryTheory.isCoseparator_iff_faithful_yoneda_obj, CategoryTheory.Functor.whiskeringRight_obj_obj