awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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)

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

Premises used: CategoryTheory.preadditiveYoneda, CategoryTheory.Functor.Faithful.of_comp, AddCommGrpCat, CategoryTheory.Functor.Faithful.comp, Iff.intro, CategoryTheory.forget, 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 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)

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
      (preadditiveYonedaObj G ⋙
        forget₂ (ModuleCat (End G)) (FC := fun (x1 x2 : ModuleCat (End G)) ↦
          LinearMap (R := End G) (RingHom.id (End 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)) (preadditiveYonedaObj G)
⊢ IsCoseparator.{v, u} G ↔ Functor.Faithful.{v, v, u, v + 1} (D := ModuleCat (End G)) (preadditiveYonedaObj G)

Tactic:
rw [isCoseparator_iff_faithful_preadditiveYoneda, preadditiveYoneda_obj]

Premises used: CategoryTheory.isCoseparator_iff_faithful_preadditiveYoneda, CategoryTheory.preadditiveYoneda_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
      (preadditiveYonedaObj G ⋙
        forget₂ (ModuleCat (End G)) (FC := fun (x1 x2 : ModuleCat (End G)) ↦
          LinearMap (R := End G) (RingHom.id (End 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)) (preadditiveYonedaObj G)

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

Premises used: ModuleCat, CategoryTheory.Functor.Faithful.of_comp, CategoryTheory.End, CategoryTheory.forget₂, AddCommGrpCat, CategoryTheory.Functor.Faithful.comp, Iff.intro, CategoryTheory.preadditiveYonedaObj
-- Module: Mathlib.CategoryTheory.Generator.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
⊢ Functor.Faithful
      (preadditiveYonedaObj G ⋙
        forget₂ (ModuleCat (End G)) (FC := fun (x1 x2 : ModuleCat (End G)) ↦
          LinearMap (R := End G) (RingHom.id (End 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)) (preadditiveYonedaObj G)

Tactic:
exact ⟨fun h => Functor.Faithful.of_comp _ (forget₂ _ AddCommGrpCat.{v}),
    fun h => Functor.Faithful.comp _ _⟩
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
X : C
M : A
F : Functor.{v, v', u, u'} Cᵒᵖ A
g : M ⟶ F.obj (op X)
x x_1 : Cᵒᵖ
x_2 : x ⟶ x_1
⊢ ∀ (b : Functor.obj (Functor.obj yoneda X) x),
    Eq (α := M ⟶ F.obj x_1)
      (CategoryStruct.comp (Y := sigmaObj.{v, v', u'} fun (i : Functor.obj (Functor.obj yoneda X) x) ↦ M)
          (Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) x) ↦ M) b :
            M ⟶ sigmaObj.{v, v', u'} fun (i : Functor.obj (Functor.obj yoneda X) x) ↦ M)
          (Functor.map (freeYoneda X M) x_2 ≫
              Sigma.desc fun (φ : Functor.obj (Functor.obj yoneda X) x_1) ↦ g ≫ F.map (Quiver.Hom.op φ) :
            Functor.obj.{v, v', u, u'} (freeYoneda X M) x ⟶ F.obj x_1) :
        M ⟶ F.obj x_1)
      (CategoryStruct.comp (Y := sigmaObj.{v, v', u'} fun (i : Functor.obj (Functor.obj yoneda X) x) ↦ M)
          (Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) x) ↦ M) b)
          ((Sigma.desc fun (φ : Functor.obj (Functor.obj yoneda X) x) ↦ g ≫ F.map (Quiver.Hom.op φ)) ≫ F.map x_2) :
        M ⟶ F.obj x_1)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
X : C
M : A
F : Functor.{v, v', u, u'} Cᵒᵖ A
f : freeYoneda X M ⟶ F
w :
  ∀ (Y : Cᵒᵖ),
    NatTrans.app
        ((fun (g : M ⟶ F.obj (op X)) ↦
            ({
                app := fun (Y : Cᵒᵖ) ↦
                  Sigma.desc fun (φ : Functor.obj (Functor.obj yoneda X) Y) ↦ g ≫ F.map (Quiver.Hom.op φ),
                naturality := ⋯ } :
              NatTrans (freeYoneda X M) F))
          ((fun (f : freeYoneda X M ⟶ F) ↦
              Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) (op X)) ↦ M) (𝟙 (unop (op X))) ≫
                f.app (op X))
            f))
        Y =
      f.app Y
⊢ (fun (g : M ⟶ F.obj (op X)) ↦
        ({
            app := fun (Y : Cᵒᵖ) ↦
              Sigma.desc fun (φ : Functor.obj (Functor.obj yoneda X) Y) ↦ g ≫ F.map (Quiver.Hom.op φ),
            naturality := ⋯ } :
          NatTrans (freeYoneda X M) F))
      ((fun (f : freeYoneda X M ⟶ F) ↦
          Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) (op X)) ↦ M) (𝟙 (unop (op X))) ≫
            f.app (op X))
        f) =
    f

Tactic:
ext Y
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
X : C
M : A
F : Functor.{v, v', u, u'} Cᵒᵖ A
f : freeYoneda X M ⟶ F
Y : Cᵒᵖ
w :
  ∀ (φ : Functor.obj (Functor.obj yoneda X) Y),
    CategoryStruct.comp (Y := sigmaObj.{v, v', u'} fun (i : Functor.obj (Functor.obj yoneda X) Y) ↦ M)
        (Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) Y) ↦ M) φ :
          M ⟶ sigmaObj.{v, v', u'} fun (i : Functor.obj (Functor.obj yoneda X) Y) ↦ M)
        (NatTrans.app
            ((fun (g : M ⟶ F.obj (op X)) ↦
                ({
                    app := fun (Y : Cᵒᵖ) ↦
                      Sigma.desc fun (φ : Functor.obj (Functor.obj yoneda X) Y) ↦ g ≫ F.map (Quiver.Hom.op φ),
                    naturality := ⋯ } :
                  NatTrans (freeYoneda X M) F))
              ((fun (f : freeYoneda X M ⟶ F) ↦
                  Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) (op X)) ↦ M)
                      (𝟙 (unop (op X))) ≫
                    f.app (op X))
                f))
            Y :
          Functor.obj.{v, v', u, u'} (freeYoneda X M) Y ⟶ F.obj Y) =
      Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) Y) ↦ M) φ ≫ f.app Y
⊢ NatTrans.app
      ((fun (g : M ⟶ F.obj (op X)) ↦
          ({
              app := fun (Y : Cᵒᵖ) ↦
                Sigma.desc fun (φ : Functor.obj (Functor.obj yoneda X) Y) ↦ g ≫ F.map (Quiver.Hom.op φ),
              naturality := ⋯ } :
            NatTrans (freeYoneda X M) F))
        ((fun (f : freeYoneda X M ⟶ F) ↦
            Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) (op X)) ↦ M) (𝟙 (unop (op X))) ≫
              f.app (op X))
          f))
      Y =
    f.app Y

Tactic:
refine Sigma.hom_ext _ _ (fun φ ↦ ?_)

Premises used: CategoryTheory.Limits.Sigma.hom_ext
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
X : C
M : A
F : Functor.{v, v', u, u'} Cᵒᵖ A
f : freeYoneda X M ⟶ F
Y : Cᵒᵖ
φ : Functor.obj (Functor.obj yoneda X) Y
⊢ CategoryStruct.comp (Y := sigmaObj.{v, v', u'} fun (i : Functor.obj (Functor.obj yoneda X) Y) ↦ M)
      (Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) Y) ↦ M) φ :
        M ⟶ sigmaObj.{v, v', u'} fun (i : Functor.obj (Functor.obj yoneda X) Y) ↦ M)
      (NatTrans.app
          ((fun (g : M ⟶ F.obj (op X)) ↦
              ({
                  app := fun (Y : Cᵒᵖ) ↦
                    Sigma.desc fun (φ : Functor.obj (Functor.obj yoneda X) Y) ↦ g ≫ F.map (Quiver.Hom.op φ),
                  naturality := ⋯ } :
                NatTrans (freeYoneda X M) F))
            ((fun (f : freeYoneda X M ⟶ F) ↦
                Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) (op X)) ↦ M)
                    (𝟙 (unop (op X))) ≫
                  f.app (op X))
              f))
          Y :
        Functor.obj.{v, v', u, u'} (freeYoneda X M) Y ⟶ F.obj Y) =
    Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) Y) ↦ M) φ ≫ f.app Y

Tactic:
simpa using (Sigma.ι _ (𝟙 _) ≫= f.naturality φ.op).symm

Premises used: Quiver.Hom.op, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.Sigma.ι, CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.whisker_eq
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
X : C
M : A
F : Functor.{v, v', u, u'} Cᵒᵖ A
g : M ⟶ F.obj (op X)
⊢ (fun (f : freeYoneda X M ⟶ F) ↦
        Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) (op X)) ↦ M) (𝟙 (unop (op X))) ≫
          f.app (op X))
      ((fun (g : M ⟶ F.obj (op X)) ↦
          ({
              app := fun (Y : Cᵒᵖ) ↦
                Sigma.desc fun (φ : Functor.obj (Functor.obj yoneda X) Y) ↦ g ≫ F.map (Quiver.Hom.op φ),
              naturality := ⋯ } :
            NatTrans (freeYoneda X M) F))
        g) =
    g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
X : C
M : A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
α : freeYoneda X M ⟶ F
f : F ⟶ G
⊢ Eq.{v' + 1} (α := M ⟶ G.obj (op X))
    ((freeYonedaHomEquiv : (a : freeYoneda X M ⟶ G) → M ⟶ G.obj (op X)) (α ≫ f) : M ⟶ G.obj (op X))
    ((freeYonedaHomEquiv : (a : freeYoneda X M ⟶ F) → M ⟶ F.obj (op X)) α ≫ f.app (op X) : M ⟶ G.obj (op X))

Tactic:
simp [freeYonedaHomEquiv]

Premises used: CategoryTheory.Presheaf.freeYonedaHomEquiv
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
X : C
M : A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
α : M ⟶ F.obj (op X)
f : F ⟶ G
a :
  Eq.{v' + 1} (α := M ⟶ G.obj (op X))
    ((freeYonedaHomEquiv : (a : freeYoneda X M ⟶ G) → M ⟶ G.obj (op X))
        ((Equiv.symm freeYonedaHomEquiv : (a : M ⟶ F.obj (op X)) → freeYoneda X M ⟶ F) α ≫ f) :
      M ⟶ G.obj (op X))
    ((freeYonedaHomEquiv : (a : freeYoneda X M ⟶ G) → M ⟶ G.obj (op X))
        ((Equiv.symm freeYonedaHomEquiv : (a : M ⟶ G.obj (op X)) → freeYoneda X M ⟶ G) (α ≫ f.app (op X))) :
      M ⟶ G.obj (op X))
⊢ Eq (α := freeYoneda X M ⟶ G)
    ((Equiv.symm freeYonedaHomEquiv : (a : M ⟶ F.obj (op X)) → freeYoneda X M ⟶ F) α ≫ f : freeYoneda X M ⟶ G)
    ((Equiv.symm freeYonedaHomEquiv : (a : M ⟶ G.obj (op X)) → freeYoneda X M ⟶ G) (α ≫ f.app (op X)) :
      freeYoneda X M ⟶ G)

Tactic:
apply freeYonedaHomEquiv.injective

Premises used: CategoryTheory.Presheaf.freeYonedaHomEquiv, Equiv.injective
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
X : C
M : A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
α : M ⟶ F.obj (op X)
f : F ⟶ G
⊢ Eq.{v' + 1} (α := M ⟶ G.obj (op X))
    ((freeYonedaHomEquiv : (a : freeYoneda X M ⟶ G) → M ⟶ G.obj (op X))
        ((Equiv.symm freeYonedaHomEquiv : (a : M ⟶ F.obj (op X)) → freeYoneda X M ⟶ F) α ≫ f) :
      M ⟶ G.obj (op X))
    ((freeYonedaHomEquiv : (a : freeYoneda X M ⟶ G) → M ⟶ G.obj (op X))
        ((Equiv.symm freeYonedaHomEquiv : (a : M ⟶ G.obj (op X)) → freeYoneda X M ⟶ G) (α ≫ f.app (op X))) :
      M ⟶ G.obj (op X))

Tactic:
simp only [freeYonedaHomEquiv_comp, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, CategoryTheory.Presheaf.freeYonedaHomEquiv_comp
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f g : F ⟶ G
h :
  ∀ (G_1 : Functor.{v, v', u, u'} Cᵒᵖ A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) x with
          | (X, i) => freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
w : ∀ (X : C), Eq (α := F.obj (op X) ⟶ G.obj (op X)) (f.app (op X)) (g.app (op X))
⊢ f = g

Tactic:
ext ⟨X⟩
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f g : F ⟶ G
h :
  ∀ (G_1 : Functor.{v, v', u, u'} Cᵒᵖ A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) x with
          | (X, i) => freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
⊢ Eq (α := F.obj (op X) ⟶ G.obj (op X)) (f.app (op X)) (g.app (op X))

Tactic:
hS _ _ ?_
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f g : F ⟶ G
h :
  ∀ (G_1 : Functor.{v, v', u, u'} Cᵒᵖ A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) x with
          | (X, i) => freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
w :
  ∀ (G_1 : A), ObjectProperty.ofObj.{v', u', w} S G_1 → ∀ (h : G_1 ⟶ F.obj (op X)), h ≫ f.app (op X) = h ≫ g.app (op X)
⊢ Eq (α := F.obj (op X) ⟶ G.obj (op X)) (f.app (op X)) (g.app (op X))

Tactic:
refine hS _ _ ?_
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f g : F ⟶ G
h :
  ∀ (G_1 : Functor.{v, v', u, u'} Cᵒᵖ A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) x with
          | (X, i) => freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
α : S i ⟶ F.obj (op X)
w :
  Eq (α := freeYoneda X (S i) ⟶ G)
    ((Equiv.symm freeYonedaHomEquiv : (a : S i ⟶ G.obj (op X)) → freeYoneda X (S i) ⟶ G) (α ≫ f.app (op X)) :
      freeYoneda X (S i) ⟶ G)
    ((Equiv.symm freeYonedaHomEquiv : (a : S i ⟶ G.obj (op X)) → freeYoneda X (S i) ⟶ G) (α ≫ g.app (op X)) :
      freeYoneda X (S i) ⟶ G)
⊢ α ≫ f.app (op X) = α ≫ g.app (op X)

Tactic:
apply freeYonedaHomEquiv.symm.injective

Premises used: CategoryTheory.Presheaf.freeYonedaHomEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f g : F ⟶ G
h :
  ∀ (G_1 : Functor.{v, v', u, u'} Cᵒᵖ A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) x with
          | (X, i) => freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
α : S i ⟶ F.obj (op X)
⊢ Eq (α := freeYoneda X (S i) ⟶ G)
    ((Equiv.symm freeYonedaHomEquiv : (a : S i ⟶ G.obj (op X)) → freeYoneda X (S i) ⟶ G) (α ≫ f.app (op X)) :
      freeYoneda X (S i) ⟶ G)
    ((Equiv.symm freeYonedaHomEquiv : (a : S i ⟶ G.obj (op X)) → freeYoneda X (S i) ⟶ G) (α ≫ g.app (op X)) :
      freeYoneda X (S i) ⟶ G)

Tactic:
simpa only [freeYonedaHomEquiv_symm_comp] using
    h _ (ObjectProperty.ofObj_apply _ ⟨X, i⟩) (freeYonedaHomEquiv.symm α)

Premises used: CategoryTheory.Presheaf.freeYonedaHomEquiv, CategoryTheory.ObjectProperty.ofObj_apply, CategoryTheory.Presheaf.freeYonedaHomEquiv_symm_comp, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
inst_3 :
  HasCoproduct (C := Functor.{v, v', u, u'} Cᵒᵖ A) fun (x : C × ι) ↦
    match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) x with
    | (X, i) => freeYoneda X (S i)
inst_4 : HasZeroMorphisms.{v', u'} A
⊢ IsSeparator (C := Functor.{v, v', u, u'} Cᵒᵖ A)
    (∐ fun (x : C × ι) ↦
      match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) x with
      | (X, i) => freeYoneda X (S i))

Tactic:
(isSeparating C hS).isSeparator_coproduct

Premises used: CategoryTheory.Presheaf.isSeparating, CategoryTheory.ObjectProperty.IsSeparating.isSeparator_coproduct
-- Module: Mathlib.CategoryTheory.Generator.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
inst_3 : HasSeparator.{v', u'} A
inst_4 : HasZeroMorphisms.{v', u'} A
inst_5 : HasCoproducts.{u, v', u'} A
⊢ ObjectProperty.IsSeparating.{v', u'} (C := A) (ObjectProperty.ofObj fun (x : Unit) ↦ separator.{v', u'} A)

Tactic:
simpa using isSeparator_separator A

Premises used: CategoryTheory.isSeparator_separator
-- Module: Mathlib.CategoryTheory.Generator.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
inst_3 : HasWeakSheafify.{v, v', u, u'} J A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
F G : Sheaf.{v, v', u, u'} J A
f g : F ⟶ G
hfg :
  ∀ (G_1 : Sheaf.{v, v', u, u'} J A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Sheaf.{v, v', u, u'} J A) x with
          | (X, i) => freeYoneda J X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
⊢ f = g

Tactic:
(sheafToPresheaf J A).map_injective (Presheaf.isSeparating C hS _ _ ?_)

Premises used: CategoryTheory.Presheaf.isSeparating, CategoryTheory.Functor.map_injective, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Generator.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
inst_3 : HasWeakSheafify.{v, v', u, u'} J A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
F G : Sheaf.{v, v', u, u'} J A
f g : F ⟶ G
hfg :
  ∀ (G_1 : Sheaf.{v, v', u, u'} J A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Sheaf.{v, v', u, u'} J A) x with
          | (X, i) => freeYoneda J X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
refine :
  ∀ (G_1 : Functor.{v, v', u, u'} Cᵒᵖ A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) x with
          | (X, i) => Presheaf.freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ Functor.obj (sheafToPresheaf J A) F),
        h ≫ Functor.map (sheafToPresheaf J A) f = h ≫ Functor.map (sheafToPresheaf J A) g
⊢ f = g

Tactic:
refine (sheafToPresheaf J A).map_injective (Presheaf.isSeparating C hS _ _ ?_)

Premises used: CategoryTheory.Presheaf.isSeparating, CategoryTheory.Functor.map_injective, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Generator.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
inst_3 : HasWeakSheafify.{v, v', u, u'} J A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
F G : Sheaf.{v, v', u, u'} J A
f g : F ⟶ G
hfg :
  ∀ (G_1 : Sheaf.{v, v', u, u'} J A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Sheaf.{v, v', u, u'} J A) x with
          | (X, i) => freeYoneda J X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
a :
  (match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) (X, i) with
    | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
    Functor.obj (sheafToPresheaf J A) F
a₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J A)
        (match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) (X, i) with
        | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
      G)
    ((Equiv.symm
            (Adjunction.homEquiv (sheafificationAdjunction J A)
              (match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) (X, i) with
              | (X, i) => Presheaf.freeYoneda X (S i))
              G) :
          (a :
              (match (motive := C × ι → Cᵒᵖ ⥤ A) (X, i) with
                | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
                (sheafToPresheaf J A).obj G) →
            (presheafToSheaf J A).obj
                (match (motive := C × ι → Cᵒᵖ ⥤ A) (X, i) with
                | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
              G)
        (a ≫ Functor.map (sheafToPresheaf J A) f) :
      Functor.obj (presheafToSheaf J A)
          (match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) (X, i) with
          | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
        G)
    ((Equiv.symm
            (Adjunction.homEquiv (sheafificationAdjunction J A)
              (match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) (X, i) with
              | (X, i) => Presheaf.freeYoneda X (S i))
              G) :
          (a :
              (match (motive := C × ι → Cᵒᵖ ⥤ A) (X, i) with
                | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
                (sheafToPresheaf J A).obj G) →
            (presheafToSheaf J A).obj
                (match (motive := C × ι → Cᵒᵖ ⥤ A) (X, i) with
                | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
              G)
        (a ≫ Functor.map (sheafToPresheaf J A) g) :
      Functor.obj (presheafToSheaf J A)
          (match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) (X, i) with
          | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
        G)
⊢ a ≫ Functor.map (sheafToPresheaf J A) f = a ≫ Functor.map (sheafToPresheaf J A) g

Tactic:
apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective

Premises used: CategoryTheory.sheafificationAdjunction, CategoryTheory.Adjunction.homEquiv, Equiv.injective, Equiv.symm