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
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)
this : Epi.{v, u} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
⊢ Eq (α :=
    kernel.{v, u} (X := ∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : Type v)) ↦ G)
        (d (𝟙 (ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A))) :
          (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : Type v)) ↦ G) ⟶ A) ⟶
      B)
    (CategoryStruct.comp (Y := ∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : Type v)) ↦ G)
        (kernel.ι (d (𝟙 (ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)))) :
          Quiver.Hom.{v, u} (V := C)
            (kernel.{v, u} (X := ∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : Type v)) ↦ G)
              (d (𝟙 (ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A))) :
                (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : Type v)) ↦ G) ⟶ A))
            (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : Type v)) ↦ G))
        (d f : (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : Type v)) ↦ G) ⟶ B) :
      kernel.{v, u} (X := ∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : Type v)) ↦ G)
          (d (𝟙 (ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A))) :
            (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : Type v)) ↦ G) ⟶ A) ⟶
        B)
    (0 :
      kernel.{v, u} (X := ∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : Type v)) ↦ G)
          (d (𝟙 (ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A))) :
            (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)) : Type v)) ↦ G) ⟶ A) ⟶
        B)

Tactic:
have h := kernel_ι_d_comp_d hG (𝟙 _) inferInstance f
-- 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)
this : Epi.{v, u} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
h :
  Eq.{v + 1} (α := kernel.{v, u} (X := ∐ fun (x : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (m : G ⟶ A) ↦ m) ⟶ B)
    (kernel.ι (Sigma.desc fun (m : G ⟶ A) ↦ m) ≫
      Sigma.desc fun (m : G ⟶ A) ↦
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (End G)ᵐᵒᵖ) ↦
              LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
              ModuleCat.carrier) f :
            (a : G ⟶ A) → G ⟶ B)
          m)
    0
⊢ ∃ (a : A ⟶ B), Functor.map (preadditiveCoyonedaObj G) a = f

Tactic:
⟨epiDesc _ _ h, ?_⟩

Premises used: CategoryTheory.Abelian.epiDesc, Exists.intro
-- 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)
this : Epi.{v, u} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
h :
  Eq.{v + 1} (α := kernel.{v, u} (X := ∐ fun (x : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (m : G ⟶ A) ↦ m) ⟶ B)
    (kernel.ι (Sigma.desc fun (m : G ⟶ A) ↦ m) ≫
      Sigma.desc fun (m : G ⟶ A) ↦
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (End G)ᵐᵒᵖ) ↦
              LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
              ModuleCat.carrier) f :
            (a : G ⟶ A) → G ⟶ B)
          m)
    0
refine :
  Functor.map (preadditiveCoyonedaObj G)
      (epiDesc (Sigma.desc fun (m : G ⟶ A) ↦ m)
        (Sigma.desc fun (m : G ⟶ A) ↦
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (End G)ᵐᵒᵖ) ↦
                LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
                ModuleCat.carrier) f :
              (a : G ⟶ A) → G ⟶ B)
            m)
        h) =
    f
⊢ ∃ (a : A ⟶ B), Functor.map (preadditiveCoyonedaObj G) a = f

Tactic:
refine ⟨epiDesc _ _ h, ?_⟩
-- 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)
this : Epi.{v, u} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
h :
  Eq.{v + 1} (α := kernel.{v, u} (X := ∐ fun (x : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (m : G ⟶ A) ↦ m) ⟶ B)
    (kernel.ι (Sigma.desc fun (m : G ⟶ A) ↦ m) ≫
      Sigma.desc fun (m : G ⟶ A) ↦
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (End G)ᵐᵒᵖ) ↦
              LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
              ModuleCat.carrier) f :
            (a : G ⟶ A) → G ⟶ B)
          m)
    0
hf :
  ∀ (q : (↑(Functor.obj (preadditiveCoyonedaObj G) A) : Type v)),
    Eq (α := (↑(Functor.obj (preadditiveCoyonedaObj G) B) : Type v))
      ((ModuleCat.Hom.hom
              (Functor.map (preadditiveCoyonedaObj G)
                (epiDesc (Sigma.desc fun (m : G ⟶ A) ↦ m)
                  (Sigma.desc fun (m : G ⟶ A) ↦
                    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (End G)ᵐᵒᵖ) ↦
                          LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
                          ModuleCat.carrier) f :
                        (a : G ⟶ A) → G ⟶ B)
                      m)
                  h)) :
            (a : (↑((preadditiveCoyonedaObj G).obj A) : Type v)) → (↑((preadditiveCoyonedaObj G).obj B) : Type v))
          q :
        (↑(Functor.obj (preadditiveCoyonedaObj G) B) : Type v))
      ((ModuleCat.Hom.hom f :
            (a : (↑((preadditiveCoyonedaObj G).obj A) : Type v)) → (↑((preadditiveCoyonedaObj G).obj B) : Type v))
          q :
        (↑(Functor.obj (preadditiveCoyonedaObj G) B) : Type v))
⊢ Functor.map (preadditiveCoyonedaObj G)
      (epiDesc (Sigma.desc fun (m : G ⟶ A) ↦ m)
        (Sigma.desc fun (m : G ⟶ A) ↦
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (End G)ᵐᵒᵖ) ↦
                LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
                ModuleCat.carrier) f :
              (a : G ⟶ A) → G ⟶ B)
            m)
        h) =
    f

Tactic:
ext q
-- 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)
this : Epi.{v, u} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
h :
  Eq.{v + 1} (α := kernel.{v, u} (X := ∐ fun (x : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (m : G ⟶ A) ↦ m) ⟶ B)
    (kernel.ι (Sigma.desc fun (m : G ⟶ A) ↦ m) ≫
      Sigma.desc fun (m : G ⟶ A) ↦
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (End G)ᵐᵒᵖ) ↦
              LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
              ModuleCat.carrier) f :
            (a : G ⟶ A) → G ⟶ B)
          m)
    0
q : (↑(Functor.obj (preadditiveCoyonedaObj G) A) : Type v)
⊢ Eq (α := (↑(Functor.obj (preadditiveCoyonedaObj G) B) : Type v))
    ((ModuleCat.Hom.hom
            (Functor.map (preadditiveCoyonedaObj G)
              (epiDesc (Sigma.desc fun (m : G ⟶ A) ↦ m)
                (Sigma.desc fun (m : G ⟶ A) ↦
                  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (End G)ᵐᵒᵖ) ↦
                        LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
                        ModuleCat.carrier) f :
                      (a : G ⟶ A) → G ⟶ B)
                    m)
                h)) :
          (a : (↑((preadditiveCoyonedaObj G).obj A) : Type v)) → (↑((preadditiveCoyonedaObj G).obj B) : Type v))
        q :
      (↑(Functor.obj (preadditiveCoyonedaObj G) B) : Type v))
    ((ModuleCat.Hom.hom f :
          (a : (↑((preadditiveCoyonedaObj G).obj A) : Type v)) → (↑((preadditiveCoyonedaObj G).obj B) : Type v))
        q :
      (↑(Functor.obj (preadditiveCoyonedaObj G) B) : Type v))

Tactic:
simpa [-comp_epiDesc] using Sigma.ι _ q ≫= comp_epiDesc _ _ h

Premises used: CategoryTheory.Abelian.comp_epiDesc, CategoryTheory.Limits.Sigma.ι
-- 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
B : C
hB : Injective.{v, u} B
rw :
  Module.Injective.{v, v} (End G)ᵐᵒᵖ
    (↑((preadditiveCoyonedaObj G : Functor.{v, v, u, v + 1} C (ModuleCat (End G)ᵐᵒᵖ)).1 B) : Type v)
⊢ Injective.{v, v + 1} (C := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (preadditiveCoyonedaObj G) B)

Tactic:
rw [← Module.injective_iff_injective_object]

Premises used: Module.injective_iff_injective_object
-- 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
B : C
hB : Injective.{v, u} B
simp : Module.Injective.{v, v} (End G)ᵐᵒᵖ (G ⟶ B)
⊢ Module.Injective.{v, v} (End G)ᵐᵒᵖ
    (↑((preadditiveCoyonedaObj G : Functor.{v, v, u, v + 1} C (ModuleCat (End G)ᵐᵒᵖ)).1 B) : Type v)

Tactic:
simp only [preadditiveCoyonedaObj_obj_carrier]

Premises used: CategoryTheory.preadditiveCoyonedaObj_obj_carrier
-- 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
B : C
hB : Injective.{v, u} B
⊢ Module.Injective.{v, v} (End G)ᵐᵒᵖ (G ⟶ B)

Tactic:
Module.Baer.injective (fun M g => ?_)

Premises used: Module.Baer.injective
-- 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
B : C
hB : Injective.{v, u} B
refine :
  ∀ (M : Ideal (End G)ᵐᵒᵖ) (g : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↥M) (G ⟶ B)),
    ∃ (g' : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (End G)ᵐᵒᵖ (G ⟶ B)),
      ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M),
        Eq (α := G ⟶ B) ((g' : (a : (End G)ᵐᵒᵖ) → G ⟶ B) x : G ⟶ B)
          ((g : (a : ↥M) → G ⟶ B) (Subtype.mk (p := fun (x : (End G)ᵐᵒᵖ) ↦ x ∈ M) x mem) : G ⟶ B)
⊢ Module.Injective.{v, v} (End G)ᵐᵒᵖ (G ⟶ B)

Tactic:
refine Module.Baer.injective (fun M g => ?_)

Premises used: Module.Baer.injective
-- 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
B : C
hB : Injective.{v, u} B
M : Ideal (End G)ᵐᵒᵖ
g : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↥M) (G ⟶ B)
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (x y : ↥M),
    (fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ)) (x + y) =
      HAdd.hAdd (α := G ⟶ G) ((fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ)) x)
        ((fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ)) y)
⊢ ∀ (x y : ↥M),
    (fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ)) (x + y) =
      HAdd.hAdd (α := G ⟶ G) ((fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ)) x)
        ((fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ)) y)

Tactic:
cat_disch
-- 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
B : C
hB : Injective.{v, u} B
M : Ideal (End G)ᵐᵒᵖ
g : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↥M) (G ⟶ B)
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (m : (End G)ᵐᵒᵖ) (x : ↥M),
    AddHom.toFun { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯ } (m • x) =
      HSMul.hSMul (α := (End G)ᵐᵒᵖ) (β := G ⟶ G)
        ((RingHom.id (End G)ᵐᵒᵖ : (a : (End G)ᵐᵒᵖ) → (End G)ᵐᵒᵖ) m : (End G)ᵐᵒᵖ)
        (AddHom.toFun { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯ : ↥M →ₙ+ (G ⟶ G) } x)
⊢ ∀ (m : (End G)ᵐᵒᵖ) (x : ↥M),
    AddHom.toFun { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯ } (m • x) =
      HSMul.hSMul (α := (End G)ᵐᵒᵖ) (β := G ⟶ G)
        ((RingHom.id (End G)ᵐᵒᵖ : (a : (End G)ᵐᵒᵖ) → (End G)ᵐᵒᵖ) m : (End G)ᵐᵒᵖ)
        (AddHom.toFun { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯ : ↥M →ₙ+ (G ⟶ G) } x)

Tactic:
cat_disch
-- 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
B : C
hB : Injective.{v, u} B
M : Ideal (End G)ᵐᵒᵖ
g : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↥M) (G ⟶ B)
refine_2 :
  ∀
    (h :
      ∃ (l : G ⟶ B),
        Eq (α := (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
          (d
                (ModuleCat.ofHom
                  { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯, map_smul' := ⋯ }) ≫
              l :
            (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
          (d (ModuleCat.ofHom g) : (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)),
    ∃ (g' : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (End G)ᵐᵒᵖ (G ⟶ B)),
      ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M),
        Eq (α := G ⟶ B) ((g' : (a : (End G)ᵐᵒᵖ) → G ⟶ B) x : G ⟶ B)
          ((g : (a : ↥M) → G ⟶ B) (Subtype.mk (p := fun (x : (End G)ᵐᵒᵖ) ↦ x ∈ M) x mem) : G ⟶ B)
refine_1 :
  Mono.{v, v + 1} (C := ModuleCat (End G)ᵐᵒᵖ) (X := ModuleCat.of (End G)ᵐᵒᵖ ↥M) (Y := ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ G))
    (ModuleCat.ofHom { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯, map_smul' := ⋯ })
⊢ ∃ (g' : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (End G)ᵐᵒᵖ (G ⟶ B)),
    ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M),
      Eq (α := G ⟶ B) ((g' : (a : (End G)ᵐᵒᵖ) → G ⟶ B) x : G ⟶ B)
        ((g : (a : ↥M) → G ⟶ B) (Subtype.mk (p := fun (x : (End G)ᵐᵒᵖ) ↦ x ∈ M) x mem) : G ⟶ B)

Tactic:
have h := exists_d_comp_eq_d hG B (ModuleCat.ofHom
      ⟨⟨fun i => i.1.unop, by cat_disch⟩, by cat_disch⟩) ?_ (ModuleCat.ofHom g)
-- 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
B : C
hB : Injective.{v, u} B
M : Ideal (End G)ᵐᵒᵖ
g : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↥M) (G ⟶ B)
h :
  ∃ (l : G ⟶ B),
    Eq (α := (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
      (d
            (ModuleCat.ofHom
              { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯, map_smul' := ⋯ }) ≫
          l :
        (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
      (d (ModuleCat.ofHom g) : (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
refine_2 :
  ∀ (l : G ⟶ B)
    (hl :
      Eq (α := (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
        (d
              (ModuleCat.ofHom
                { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯, map_smul' := ⋯ }) ≫
            l :
          (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
        (d (ModuleCat.ofHom g) : (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)),
    ∃ (g' : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (End G)ᵐᵒᵖ (G ⟶ B)),
      ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M),
        Eq (α := G ⟶ B) ((g' : (a : (End G)ᵐᵒᵖ) → G ⟶ B) x : G ⟶ B)
          ((g : (a : ↥M) → G ⟶ B) (Subtype.mk (p := fun (x : (End G)ᵐᵒᵖ) ↦ x ∈ M) x mem) : G ⟶ B)
⊢ ∃ (g' : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (End G)ᵐᵒᵖ (G ⟶ B)),
    ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M),
      Eq (α := G ⟶ B) ((g' : (a : (End G)ᵐᵒᵖ) → G ⟶ B) x : G ⟶ B)
        ((g : (a : ↥M) → G ⟶ B) (Subtype.mk (p := fun (x : (End G)ᵐᵒᵖ) ↦ x ∈ M) x mem) : G ⟶ B)

Tactic:
obtain ⟨l, hl⟩ := h
-- 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
B : C
hB : Injective.{v, u} B
M : Ideal (End G)ᵐᵒᵖ
g : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↥M) (G ⟶ B)
l : G ⟶ B
hl :
  Eq (α := (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
    (d (ModuleCat.ofHom { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯, map_smul' := ⋯ }) ≫
        l :
      (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
    (d (ModuleCat.ofHom g) : (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
⊢ ∃ (g' : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (End G)ᵐᵒᵖ (G ⟶ B)),
    ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M),
      Eq (α := G ⟶ B) ((g' : (a : (End G)ᵐᵒᵖ) → G ⟶ B) x : G ⟶ B)
        ((g : (a : ↥M) → G ⟶ B) (Subtype.mk (p := fun (x : (End G)ᵐᵒᵖ) ↦ x ∈ M) x mem) : G ⟶ B)

Tactic:
⟨((preadditiveCoyonedaObj G).map l).hom ∘ₗ
        (Preadditive.homSelfLinearEquivEndMulOpposite G).symm.toLinearMap, ?_⟩

Premises used: LinearEquiv.symm, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite, CategoryTheory.preadditiveCoyonedaObj, CategoryTheory.Functor.map, LinearMap.comp, LinearEquiv.toLinearMap, Exists.intro, ModuleCat.Hom.hom
-- 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
B : C
hB : Injective.{v, u} B
M : Ideal (End G)ᵐᵒᵖ
g : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↥M) (G ⟶ B)
l : G ⟶ B
hl :
  Eq (α := (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
    (d (ModuleCat.ofHom { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯, map_smul' := ⋯ }) ≫
        l :
      (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
    (d (ModuleCat.ofHom g) : (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
refine_2 :
  ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M),
    Eq (α := G ⟶ B)
      (((ModuleCat.Hom.hom (Functor.map (preadditiveCoyonedaObj G) l) ∘ₗ
                (↑(LinearEquiv.symm (Preadditive.homSelfLinearEquivEndMulOpposite G)) :
                  (End G)ᵐᵒᵖ →ₗ[(End G)ᵐᵒᵖ] G ⟶ G) :
              LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (End G)ᵐᵒᵖ (G ⟶ B)) :
            (a : (End G)ᵐᵒᵖ) → G ⟶ B)
          x :
        G ⟶ B)
      ((g : (a : ↥M) → G ⟶ B) (Subtype.mk (p := fun (x : (End G)ᵐᵒᵖ) ↦ x ∈ M) x mem) : G ⟶ B)
⊢ ∃ (g' : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (End G)ᵐᵒᵖ (G ⟶ B)),
    ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M),
      Eq (α := G ⟶ B) ((g' : (a : (End G)ᵐᵒᵖ) → G ⟶ B) x : G ⟶ B)
        ((g : (a : ↥M) → G ⟶ B) (Subtype.mk (p := fun (x : (End G)ᵐᵒᵖ) ↦ x ∈ M) x mem) : G ⟶ B)

Tactic:
refine ⟨((preadditiveCoyonedaObj G).map l).hom ∘ₗ
        (Preadditive.homSelfLinearEquivEndMulOpposite G).symm.toLinearMap, ?_⟩
-- 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
B : C
hB : Injective.{v, u} B
M : Ideal (End G)ᵐᵒᵖ
g : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↥M) (G ⟶ B)
l : G ⟶ B
hl :
  Eq (α := (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
    (d (ModuleCat.ofHom { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯, map_smul' := ⋯ }) ≫
        l :
      (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
    (d (ModuleCat.ofHom g) : (∐ fun (x : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) ↦ G) ⟶ B)
f : (End G)ᵐᵒᵖ
hf : f ∈ M
⊢ Eq (α := G ⟶ B)
    (((ModuleCat.Hom.hom (Functor.map (preadditiveCoyonedaObj G) l) ∘ₗ
              (↑(LinearEquiv.symm (Preadditive.homSelfLinearEquivEndMulOpposite G)) : (End G)ᵐᵒᵖ →ₗ[(End G)ᵐᵒᵖ] G ⟶ G) :
            LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (End G)ᵐᵒᵖ (G ⟶ B)) :
          (a : (End G)ᵐᵒᵖ) → G ⟶ B)
        f :
      G ⟶ B)
    ((g : (a : ↥M) → G ⟶ B) (Subtype.mk (p := fun (x : (End G)ᵐᵒᵖ) ↦ x ∈ M) f hf) : G ⟶ B)

Tactic:
simpa [d] using Sigma.ι _ ⟨f, hf⟩ ≫= hl

Premises used: CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d, CategoryTheory.Limits.Sigma.ι
-- 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
B : C
hB : Injective.{v, u} B
M : Ideal (End G)ᵐᵒᵖ
g : LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↥M) (G ⟶ B)
refine_1 :
  Function.Injective (α := (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) (β :=
    (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ G)) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (End G)ᵐᵒᵖ) ↦
          LinearMap (R := (End G)ᵐᵒᵖ) (RingHom.id (End G)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC := ModuleCat.carrier)
          (X := ModuleCat.of (End G)ᵐᵒᵖ ↥M) (Y := ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ G))
          (ModuleCat.ofHom
            { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯, map_smul' := ⋯ })) :
      (a : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) → (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ G)) : Type v))
⊢ Mono.{v, v + 1} (C := ModuleCat (End G)ᵐᵒᵖ) (X := ModuleCat.of (End G)ᵐᵒᵖ ↥M) (Y := ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ G))
    (ModuleCat.ofHom { toFun := fun (i : ↥M) ↦ MulOpposite.unop (↑i : (End G)ᵐᵒᵖ), map_add' := ⋯, map_smul' := ⋯ })

Tactic:
rw [ModuleCat.mono_iff_injective]

Premises used: ModuleCat.mono_iff_injective
-- 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
⊢ Functor.PreservesInjectiveObjects.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)

Tactic:
have := preservesInjectiveObjects G hG
-- 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
this : Functor.PreservesInjectiveObjects.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)
⊢ Functor.PreservesMonomorphisms.{v, v, v + 1, u} (C := ModuleCat (End G)ᵐᵒᵖ) (tensorObj G)

Tactic:
have : (tensorObj G).PreservesMonomorphisms :=
    (tensorObj G).preservesMonomorphisms_of_adjunction_of_preservesInjectiveObjects
      (tensorObjPreadditiveCoyonedaObjAdjunction G)