awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
⊢ Functor.IsLeftAdjoint.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)

Tactic:
(tensorObjPreadditiveCoyonedaObjAdjunction G).isLeftAdjoint

Premises used: CategoryTheory.IsGrothendieckAbelian.tensorObjPreadditiveCoyonedaObjAdjunction, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G A : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
m : (↑M : Type v)
⊢ CategoryStruct.comp (Y := ∐ fun (x : (↑M : Type v)) ↦ G)
      (Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) m : G ⟶ ∐ fun (x : (↑M : Type v)) ↦ G)
      (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) =
    (ModuleCat.Hom.hom g : (a : (↑M : Type v)) → (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : Type v)) m

Tactic:
simp [d]

Premises used: CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
⊢ Eq (α := kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶ B)
    (CategoryStruct.comp (Y := ∐ fun (x : (↑M : Type v)) ↦ G)
        (kernel.ι (d g) :
          kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
            ∐ fun (x : (↑M : Type v)) ↦ G)
        (d f : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ B) :
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶ B)
    (0 : kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶ B)

Tactic:
(isColimitFiniteSubproductsCocone (fun (_ : M) => G)).pullback_zero_ext (fun F => ?_)

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.CoproductsFromFiniteFiltered.isColimitFiniteSubproductsCocone, CategoryTheory.Limits.IsColimit.pullback_zero_ext, CategoryTheory.Limits.colimit, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
rw :
  Eq (α := G ⟶ B)
    (∑ j ∈ F.attach,
      CategoryStruct.comp (Y := ∐ fun (x : (↑M : Type v)) ↦ G)
        (h ≫
            pullback.fst
                (∑ a ∈ F.attach,
                  Sigma.π (fun (a : ↥F) ↦ G) a ≫
                    Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
                (kernel.ι (d g)) ≫
              Sigma.π (fun (a : ↥F) ↦ G) j ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑j : Discrete (↑M : Type v)).as :
          G ⟶ ∐ fun (x : (↑M : Type v)) ↦ G)
        (d f : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ B))
    0
⊢ h ≫
      pullback.fst
          (∑ a ∈ F.attach,
            Sigma.π (fun (a : ↥F) ↦ G) a ≫
              Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
          (kernel.ι (d g)) ≫
        CategoryStruct.comp (Y := ∐ fun (x : (↑M : Type v)) ↦ G)
          (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
            Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
          (d f : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ B) =
    0

Tactic:
rw [Preadditive.comp_sum_assoc, Preadditive.comp_sum_assoc, Preadditive.sum_comp]

Premises used: CategoryTheory.Preadditive.comp_sum_assoc, CategoryTheory.Preadditive.sum_comp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
simp :
  Eq (α := G ⟶ B)
    (∑ x ∈ F.attach,
      h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (a : ↥F) ↦ G) x ≫
            (ModuleCat.Hom.hom f : (a : (↑M : Type v)) → G ⟶ B) (↑x : Discrete (↑M : Type v)).as)
    0
⊢ Eq (α := G ⟶ B)
    (∑ j ∈ F.attach,
      CategoryStruct.comp (Y := ∐ fun (x : (↑M : Type v)) ↦ G)
        (h ≫
            pullback.fst
                (∑ a ∈ F.attach,
                  Sigma.π (fun (a : ↥F) ↦ G) a ≫
                    Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
                (kernel.ι (d g)) ≫
              Sigma.π (fun (a : ↥F) ↦ G) j ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑j : Discrete (↑M : Type v)).as :
          G ⟶ ∐ fun (x : (↑M : Type v)) ↦ G)
        (d f : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ B))
    0

Tactic:
simp only [Category.assoc, ι_d]

Premises used: CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d, CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
r : (x : ↥F) → (End G)ᵐᵒᵖ :=
  fun (x : ↥F) ↦
    MulOpposite.op
      (h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (x : ↥F) ↦ G) x)
this :
  Eq (α := (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v))
    (∑ x ∈ F.attach,
      HSMul.hSMul (β := (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v)) (r x)
        ((ModuleCat.Hom.hom f : (a : (↑M : Type v)) → (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v))
            (↑x : Discrete (↑M : Type v)).as :
          (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v)))
    0
⊢ Eq (α := G ⟶ B)
    (∑ x ∈ F.attach,
      h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (a : ↥F) ↦ G) x ≫
            (ModuleCat.Hom.hom f : (a : (↑M : Type v)) → G ⟶ B) (↑x : Discrete (↑M : Type v)).as)
    0

Tactic:
simpa [End.smul_left, r] using this

Premises used: CategoryTheory.End.smul_left
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
r : (x : ↥F) → (End G)ᵐᵒᵖ :=
  fun (x : ↥F) ↦
    MulOpposite.op
      (h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (x : ↥F) ↦ G) x)
suffices :
  Eq (α := (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v))
    (∑ x ∈ F.attach,
      HSMul.hSMul (β := (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v)) (r x)
        ((ModuleCat.Hom.hom f : (a : (↑M : Type v)) → (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v))
            (↑x : Discrete (↑M : Type v)).as :
          (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v)))
    0
⊢ Eq (α := G ⟶ B)
    (∑ x ∈ F.attach,
      h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (a : ↥F) ↦ G) x ≫
            (ModuleCat.Hom.hom f : (a : (↑M : Type v)) → G ⟶ B) (↑x : Discrete (↑M : Type v)).as)
    0

Tactic:
suffices ∑ x ∈ F.attach, r x • f.hom x.1.as = 0 by simpa [End.smul_left, r] using this
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
r : (x : ↥F) → (End G)ᵐᵒᵖ :=
  fun (x : ↥F) ↦
    MulOpposite.op
      (h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (x : ↥F) ↦ G) x)
simp :
  Eq (α := G ⟶ B)
    ((ModuleCat.Hom.hom f : (a : (↑M : Type v)) → G ⟶ B) (∑ x ∈ F.attach, r x • (↑x : Discrete (↑M : Type v)).as) :
      G ⟶ B)
    (0 : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v))
⊢ Eq (α := (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v))
    (∑ x ∈ F.attach,
      HSMul.hSMul (β := (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v)) (r x)
        ((ModuleCat.Hom.hom f : (a : (↑M : Type v)) → (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v))
            (↑x : Discrete (↑M : Type v)).as :
          (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v)))
    0

Tactic:
simp only [← map_smul, ← map_sum]

Premises used: map_sum, map_smul
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
r : (x : ↥F) → (End G)ᵐᵒᵖ :=
  fun (x : ↥F) ↦
    MulOpposite.op
      (h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (x : ↥F) ↦ G) x)
this : Eq (α := (↑M : Type v)) (∑ x ∈ F.attach, r x • (↑x : Discrete (↑M : Type v)).as) 0
⊢ Eq (α := G ⟶ B)
    ((ModuleCat.Hom.hom f : (a : (↑M : Type v)) → G ⟶ B) (∑ x ∈ F.attach, r x • (↑x : Discrete (↑M : Type v)).as) :
      G ⟶ B)
    (0 : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v))

Tactic:
simp [this]
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
r : (x : ↥F) → (End G)ᵐᵒᵖ :=
  fun (x : ↥F) ↦
    MulOpposite.op
      (h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (x : ↥F) ↦ G) x)
suffices : Eq (α := (↑M : Type v)) (∑ x ∈ F.attach, r x • (↑x : Discrete (↑M : Type v)).as) 0
⊢ Eq (α := G ⟶ B)
    ((ModuleCat.Hom.hom f : (a : (↑M : Type v)) → G ⟶ B) (∑ x ∈ F.attach, r x • (↑x : Discrete (↑M : Type v)).as) :
      G ⟶ B)
    (0 : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v))

Tactic:
suffices ∑ x ∈ F.attach, r x • x.1.as = 0 by simp [this]
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
r : (x : ↥F) → (End G)ᵐᵒᵖ :=
  fun (x : ↥F) ↦
    MulOpposite.op
      (h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (x : ↥F) ↦ G) x)
simp :
  Eq (α := G ⟶ A)
    (∑ x ∈ F.attach,
      HSMul.hSMul (β := G ⟶ A) (r x)
        ((ModuleCat.Hom.hom g : (a : (↑M : Type v)) → G ⟶ A) (↑x : Discrete (↑M : Type v)).as : G ⟶ A))
    0
⊢ Eq (α := (↑M : Type v)) (∑ x ∈ F.attach, r x • (↑x : Discrete (↑M : Type v)).as) 0

Tactic:
simp only [← g.hom.map_eq_zero_iff ((ModuleCat.mono_iff_injective _).1 hg), map_sum, map_smul]

Premises used: ModuleCat.mono_iff_injective, map_sum, Iff.mp, ModuleCat.Hom.hom, LinearMap.map_eq_zero_iff, map_smul
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
r : (x : ↥F) → (End G)ᵐᵒᵖ :=
  fun (x : ↥F) ↦
    MulOpposite.op
      (h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (x : ↥F) ↦ G) x)
simp :
  Eq (α := G ⟶ A)
    (∑ x ∈ F.attach,
      h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (x : ↥F) ↦ G) x ≫
            CategoryStruct.comp (Y := ∐ fun (x : (↑M : Type v)) ↦ G)
              (Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑x : Discrete (↑M : Type v)).as :
                G ⟶ ∐ fun (x : (↑M : Type v)) ↦ G)
              (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A))
    0
⊢ Eq (α := G ⟶ A)
    (∑ x ∈ F.attach,
      HSMul.hSMul (β := G ⟶ A) (r x)
        ((ModuleCat.Hom.hom g : (a : (↑M : Type v)) → G ⟶ A) (↑x : Discrete (↑M : Type v)).as : G ⟶ A))
    0

Tactic:
simp only [← ι_d g, End.smul_left, MulOpposite.unop_op, Category.assoc, r]

Premises used: CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d, CategoryTheory.Category.assoc, CategoryTheory.End.smul_left, MulOpposite.unop_op
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
r : (x : ↥F) → (End G)ᵐᵒᵖ :=
  fun (x : ↥F) ↦
    MulOpposite.op
      (h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (x : ↥F) ↦ G) x)
⊢ Eq (α := G ⟶ A)
    (∑ x ∈ F.attach,
      h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (x : ↥F) ↦ G) x ≫
            CategoryStruct.comp (Y := ∐ fun (x : (↑M : Type v)) ↦ G)
              (Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑x : Discrete (↑M : Type v)).as :
                G ⟶ ∐ fun (x : (↑M : Type v)) ↦ G)
              (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A))
    0

Tactic:
simp [← Preadditive.comp_sum, ← Preadditive.sum_comp', pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Preadditive.sum_comp'
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
f :
  Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (preadditiveCoyonedaObj G) A)
    (Functor.obj (preadditiveCoyonedaObj G) B)
⊢ Epi.{v, u} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)

Tactic:
have := (isSeparator_iff_epi G).1 hG A