awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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 (α := (↑(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
have 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))
Tactic: simp only [← map_smul, ← map_sum]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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 ⟶ 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))
have suffices : Eq (α := (↑M : Type v)) (∑ x ∈ F.attach, r x • (↑x : Discrete (↑M : Type v)).as) 0
Tactic: suffices ∑ x ∈ F.attach, r x • x.1.as = 0 by simp [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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 (α := (↑M : Type v)) (∑ x ∈ F.attach, r x • (↑x : Discrete (↑M : Type v)).as) 0
have 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
Tactic: simp only [← g.hom.map_eq_zero_iff ((ModuleCat.mono_iff_injective _).1 hg), map_sum, map_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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,
      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
have 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
Tactic: simp only [← ι_d g, End.smul_left, MulOpposite.unop_op, Category.assoc, r]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (hypothesis)
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)
⊢ ∃ (a : A ⟶ B), Functor.map (preadditiveCoyonedaObj G) a = f
have this : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (hypothesis)
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)
⊢ ∃ (a : A ⟶ B), Functor.map (preadditiveCoyonedaObj G) a = f
have h : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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
have 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
Tactic: refine ⟨epiDesc _ _ h, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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
⊢ 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
have 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))
Tactic: ext q
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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
⊢ Injective.{v, v + 1} (C := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (preadditiveCoyonedaObj G) B)
have rw : Module.Injective.{v, v} (End G)ᵐᵒᵖ
  (↑((preadditiveCoyonedaObj G : Functor.{v, v, u, v + 1} C (ModuleCat (End G)ᵐᵒᵖ)).1 B) : Type v)
Tactic: rw [← Module.injective_iff_injective_object]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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)ᵐᵒᵖ
    (↑((preadditiveCoyonedaObj G : Functor.{v, v, u, v + 1} C (ModuleCat (End G)ᵐᵒᵖ)).1 B) : Type v)
have simp : Module.Injective.{v, v} (End G)ᵐᵒᵖ (G ⟶ B)
Tactic: simp only [preadditiveCoyonedaObj_obj_carrier]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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)
have 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)
Tactic: refine Module.Baer.injective (fun M g => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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)
⊢ ∃ (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)
have 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' := sorry, map_smul' := sorry }) ≫
            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: 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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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)
⊢ ∃ (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)
have 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' := sorry, map_smul' := sorry })
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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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)
⊢ ∃ (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)
have 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' := sorry, map_smul' := sorry }) ≫
          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: obtain ⟨l, hl⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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)
have 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)
Tactic: refine ⟨((preadditiveCoyonedaObj G).map l).hom ∘ₗ
        (Preadditive.homSelfLinearEquivEndMulOpposite G).symm.toLinearMap, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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)
⊢ 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' := ⋯ })
have 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' := sorry, map_smul' := sorry })) :
    (a : (↑(ModuleCat.of (End G)ᵐᵒᵖ ↥M) : Type v)) → (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ G)) : Type v))
Tactic: rw [ModuleCat.mono_iff_injective]