[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
let G : (⟨X⟩ : ModuleCat ℤ) ⟶ ⟨A⟩ :=
  { g with
    map_smul' := by
      intros
      dsimp
      rw [map_zsmul] }
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
⊢ ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
    AddHom.toFun
        { toFun := g.toFun,
          map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
        (r • x) =
      ↑(RingHom.id ℤ) r •
        AddHom.toFun
          { toFun := g.toFun,
            map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
          x
[PROOFSTEP]
intros
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
r✝ : ℤ
x✝ : ↑(ModuleCat.mk ↑X)
⊢ AddHom.toFun
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
      (r✝ • x✝) =
    ↑(RingHom.id ℤ) r✝ •
      AddHom.toFun
        { toFun := g.toFun,
          map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
        x✝
[PROOFSTEP]
dsimp
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
r✝ : ℤ
x✝ : ↑(ModuleCat.mk ↑X)
⊢ ↑g (r✝ • x✝) = r✝ • ↑g x✝
[PROOFSTEP]
rw [map_zsmul]
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
let F : (⟨X⟩ : ModuleCat ℤ) ⟶ ⟨Y⟩ :=
  { f with
    map_smul' := by
      intros
      dsimp
      rw [map_zsmul] }
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
⊢ ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
    AddHom.toFun
        { toFun := f.toFun,
          map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
        (r • x) =
      ↑(RingHom.id ℤ) r •
        AddHom.toFun
          { toFun := f.toFun,
            map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
          x
[PROOFSTEP]
intros
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
r✝ : ℤ
x✝ : ↑(ModuleCat.mk ↑X)
⊢ AddHom.toFun
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
      (r✝ • x✝) =
    ↑(RingHom.id ℤ) r✝ •
      AddHom.toFun
        { toFun := f.toFun,
          map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
        x✝
[PROOFSTEP]
dsimp
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
r✝ : ℤ
x✝ : ↑(ModuleCat.mk ↑X)
⊢ ↑f (r✝ • x✝) = r✝ • ↑f x✝
[PROOFSTEP]
rw [map_zsmul]
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
have : Mono F :=
  by
  refine'
    ⟨fun {Z} α β eq1 => _⟩
      -- Porting note: trouble getting to ℤ-module from ModuleCat ℤ
              -- AddCommGroup.intModule not defeq to .isModule
  let α' : AddCommGroupCat.of Z ⟶ X := @LinearMap.toAddMonoidHom _ _ _ _ _ _ _ _ (_) _ _ α
  let β' : AddCommGroupCat.of Z ⟶ X := @LinearMap.toAddMonoidHom _ _ _ _ _ _ _ _ (_) _ _ β
  have eq2 : α' ≫ f = β' ≫ f := by
    ext x
    simp only [CategoryTheory.comp_apply, LinearMap.toAddMonoidHom_coe]
    simpa only [ModuleCat.coe_comp, LinearMap.coe_mk, Function.comp_apply] using FunLike.congr_fun eq1 x
  rw [cancel_mono] at eq2
  have : ⇑α' = ⇑β' := congrArg _ eq2
  ext x
  apply congrFun this _
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
⊢ Mono F
[PROOFSTEP]
refine'
  ⟨fun {Z} α β eq1 => _⟩
    -- Porting note: trouble getting to ℤ-module from ModuleCat ℤ
            -- AddCommGroup.intModule not defeq to .isModule
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
Z : ModuleCat ℤ
α β : Z ⟶ ModuleCat.mk ↑X
eq1 : α ≫ F = β ≫ F
⊢ α = β
[PROOFSTEP]
let α' : AddCommGroupCat.of Z ⟶ X := @LinearMap.toAddMonoidHom _ _ _ _ _ _ _ _ (_) _ _ α
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
Z : ModuleCat ℤ
α β : Z ⟶ ModuleCat.mk ↑X
eq1 : α ≫ F = β ≫ F
α' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom α
⊢ α = β
[PROOFSTEP]
let β' : AddCommGroupCat.of Z ⟶ X := @LinearMap.toAddMonoidHom _ _ _ _ _ _ _ _ (_) _ _ β
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
Z : ModuleCat ℤ
α β : Z ⟶ ModuleCat.mk ↑X
eq1 : α ≫ F = β ≫ F
α' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom α
β' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom β
⊢ α = β
[PROOFSTEP]
have eq2 : α' ≫ f = β' ≫ f := by
  ext x
  simp only [CategoryTheory.comp_apply, LinearMap.toAddMonoidHom_coe]
  simpa only [ModuleCat.coe_comp, LinearMap.coe_mk, Function.comp_apply] using FunLike.congr_fun eq1 x
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
Z : ModuleCat ℤ
α β : Z ⟶ ModuleCat.mk ↑X
eq1 : α ≫ F = β ≫ F
α' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom α
β' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom β
⊢ α' ≫ f = β' ≫ f
[PROOFSTEP]
ext x
[GOAL]
case w
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
Z : ModuleCat ℤ
α β : Z ⟶ ModuleCat.mk ↑X
eq1 : α ≫ F = β ≫ F
α' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom α
β' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom β
x : ↑(of ↑Z)
⊢ ↑(α' ≫ f) x = ↑(β' ≫ f) x
[PROOFSTEP]
simp only [CategoryTheory.comp_apply, LinearMap.toAddMonoidHom_coe]
[GOAL]
case w
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
Z : ModuleCat ℤ
α β : Z ⟶ ModuleCat.mk ↑X
eq1 : α ≫ F = β ≫ F
α' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom α
β' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom β
x : ↑(of ↑Z)
⊢ ↑(LinearMap.toAddMonoidHom α ≫ f) x = ↑(LinearMap.toAddMonoidHom β ≫ f) x
[PROOFSTEP]
simpa only [ModuleCat.coe_comp, LinearMap.coe_mk, Function.comp_apply] using FunLike.congr_fun eq1 x
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
Z : ModuleCat ℤ
α β : Z ⟶ ModuleCat.mk ↑X
eq1 : α ≫ F = β ≫ F
α' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom α
β' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom β
eq2 : α' ≫ f = β' ≫ f
⊢ α = β
[PROOFSTEP]
rw [cancel_mono] at eq2
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
Z : ModuleCat ℤ
α β : Z ⟶ ModuleCat.mk ↑X
eq1 : α ≫ F = β ≫ F
α' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom α
β' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom β
eq2 : α' = β'
⊢ α = β
[PROOFSTEP]
have : ⇑α' = ⇑β' := congrArg _ eq2
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
Z : ModuleCat ℤ
α β : Z ⟶ ModuleCat.mk ↑X
eq1 : α ≫ F = β ≫ F
α' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom α
β' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom β
eq2 : α' = β'
this : ↑α' = ↑β'
⊢ α = β
[PROOFSTEP]
ext x
[GOAL]
case h
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
Z : ModuleCat ℤ
α β : Z ⟶ ModuleCat.mk ↑X
eq1 : α ≫ F = β ≫ F
α' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom α
β' : of ↑Z ⟶ X := LinearMap.toAddMonoidHom β
eq2 : α' = β'
this : ↑α' = ↑β'
x : ↑Z
⊢ ↑α x = ↑β x
[PROOFSTEP]
apply congrFun this _
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
this : Mono F
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
refine' ⟨(Injective.factorThru G F).toAddMonoidHom, _⟩
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
this : Mono F
⊢ f ≫ LinearMap.toAddMonoidHom (Injective.factorThru G F) = g
[PROOFSTEP]
ext x
[GOAL]
case w
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (ModuleCat.mk A)
X Y : Bundled AddCommGroup
g : X ⟶ Bundled.mk A
f : X ⟶ Y
m : Mono f
G : ModuleCat.mk ↑X ⟶ ModuleCat.mk A :=
  {
    toAddHom :=
      { toFun := g.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := g.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := g.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑g) (x + y) = ZeroHom.toFun (↑g) x + ZeroHom.toFun (↑g) y) }
                x) }
F : ModuleCat.mk ↑X ⟶ ModuleCat.mk ↑Y :=
  {
    toAddHom :=
      { toFun := f.toFun,
        map_add' := (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) },
    map_smul' :=
      (_ :
        ∀ (r : ℤ) (x : ↑(ModuleCat.mk ↑X)),
          AddHom.toFun
              { toFun := f.toFun,
                map_add' :=
                  (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
              (r • x) =
            ↑(RingHom.id ℤ) r •
              AddHom.toFun
                { toFun := f.toFun,
                  map_add' :=
                    (_ : ∀ (x y : ↑X), ZeroHom.toFun (↑f) (x + y) = ZeroHom.toFun (↑f) x + ZeroHom.toFun (↑f) y) }
                x) }
this : Mono F
x : (forget (Bundled AddCommGroup)).obj X
⊢ ↑(f ≫ LinearMap.toAddMonoidHom (Injective.factorThru G F)) x = ↑g x
[PROOFSTEP]
convert FunLike.congr_fun (Injective.comp_factorThru G F) x
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
let G : (⟨X, inferInstance⟩ : AddCommGroupCat) ⟶ ⟨A, inferInstance⟩ :=
  @LinearMap.toAddMonoidHom _ _ _ _ _ _ _ _ (_) _ _ g
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
let F : (⟨X, inferInstance⟩ : AddCommGroupCat) ⟶ ⟨Y, inferInstance⟩ :=
  @LinearMap.toAddMonoidHom _ _ _ _ _ _ _ _ (_) (_) _ f
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
have : Mono F := by
  rw [mono_iff_injective]
  intro _ _ h
  exact ((ModuleCat.mono_iff_injective f).mp m) h
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
⊢ Mono F
[PROOFSTEP]
rw [mono_iff_injective]
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
⊢ Function.Injective ↑F
[PROOFSTEP]
intro _ _ h
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
a₁✝ a₂✝ : ↑(Bundled.mk ↑X)
h : ↑F a₁✝ = ↑F a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
exact ((ModuleCat.mono_iff_injective f).mp m) h
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
⊢ ∃ h, f ≫ h = g
[PROOFSTEP]
refine ⟨@LinearMap.mk _ _ _ _ _ _ _ _ _ (_) _ (Injective.factorThru G F).toAddHom ?_, ?_⟩
[GOAL]
case refine_1
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
⊢ ∀ (r : ℤ) (x : ↑Y),
    AddHom.toFun (↑(Injective.factorThru G F)) (r • x) =
      ↑(RingHom.id ℤ) r • AddHom.toFun (↑(Injective.factorThru G F)) x
case refine_2
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
⊢ f ≫ { toAddHom := ↑(Injective.factorThru G F), map_smul' := ?refine_1 } = g
[PROOFSTEP]
change ∀ r, ∀ x, (Injective.factorThru G F).toFun _ = _ • (Injective.factorThru G F).toFun _
[GOAL]
case refine_1
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
⊢ ∀ (r : ℤ) (x : ↑Y),
    ZeroHom.toFun (↑(Injective.factorThru G F)) (r • x) =
      ↑(RingHom.id ℤ) r • ZeroHom.toFun (↑(Injective.factorThru G F)) x
[PROOFSTEP]
intro m x
[GOAL]
case refine_1
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m✝ : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
m : ℤ
x : ↑Y
⊢ ZeroHom.toFun (↑(Injective.factorThru G F)) (m • x) =
    ↑(RingHom.id ℤ) m • ZeroHom.toFun (↑(Injective.factorThru G F)) x
[PROOFSTEP]
rw [AddMonoidHom.toFun_eq_coe, RingHom.id_apply]
[GOAL]
case refine_1
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m✝ : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
m : ℤ
x : ↑Y
⊢ ↑(Injective.factorThru G F) (m • x) = m • ↑(Injective.factorThru G F) x
[PROOFSTEP]
induction' m using Int.induction_on with n hn n hn
[GOAL]
case refine_1.hz
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
⊢ ↑(Injective.factorThru G F) (0 • x) = 0 • ↑(Injective.factorThru G F) x
[PROOFSTEP]
rw [zero_smul]
[GOAL]
case refine_1.hz
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
⊢ ↑(Injective.factorThru G F) (0 • x) = 0
[PROOFSTEP]
convert
  map_zero (M := Y) (N := A) (F := Y →+ A)
    _
      -- Porting note: hell of non-defeq instances; somehow this worked
[GOAL]
case h.e'_2.h.e'_6
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
⊢ 0 • x = 0
[PROOFSTEP]
refine @zero_smul ℤ Y (MonoidWithZero.toZero) (AddMonoid.toZero) ?_ x
[GOAL]
case refine_1.hp
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (↑n • x) = ↑n • ↑(Injective.factorThru G F) x
⊢ ↑(Injective.factorThru G F) ((↑n + 1) • x) = (↑n + 1) • ↑(Injective.factorThru G F) x
[PROOFSTEP]
conv_rhs => rw [add_smul]
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (↑n • x) = ↑n • ↑(Injective.factorThru G F) x
| (↑n + 1) • ↑(Injective.factorThru G F) x
[PROOFSTEP]
rw [add_smul]
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (↑n • x) = ↑n • ↑(Injective.factorThru G F) x
| (↑n + 1) • ↑(Injective.factorThru G F) x
[PROOFSTEP]
rw [add_smul]
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (↑n • x) = ↑n • ↑(Injective.factorThru G F) x
| (↑n + 1) • ↑(Injective.factorThru G F) x
[PROOFSTEP]
rw [add_smul]
[GOAL]
case refine_1.hp
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (↑n • x) = ↑n • ↑(Injective.factorThru G F) x
⊢ ↑(Injective.factorThru G F) ((↑n + 1) • x) = ↑n • ↑(Injective.factorThru G F) x + 1 • ↑(Injective.factorThru G F) x
[PROOFSTEP]
rw [← hn, one_smul, ← map_add]
[GOAL]
case refine_1.hp
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (↑n • x) = ↑n • ↑(Injective.factorThru G F) x
⊢ ↑(Injective.factorThru G F) ((↑n + 1) • x) = ↑(Injective.factorThru G F) (↑n • x + x)
[PROOFSTEP]
congr
[GOAL]
case refine_1.hp.h.e_6.h
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (↑n • x) = ↑n • ↑(Injective.factorThru G F) x
⊢ (↑n + 1) • x = ↑n • x + x
[PROOFSTEP]
convert @add_smul ℤ Y _ _ ?_ n 1 x
[GOAL]
case h.e'_3.h.e'_6
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (↑n • x) = ↑n • ↑(Injective.factorThru G F) x
⊢ x = 1 • x
[PROOFSTEP]
refine @one_smul ℤ Y _ ?_ x |>.symm
[GOAL]
case refine_1.hn
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (-↑n • x) = -↑n • ↑(Injective.factorThru G F) x
⊢ ↑(Injective.factorThru G F) ((-↑n - 1) • x) = (-↑n - 1) • ↑(Injective.factorThru G F) x
[PROOFSTEP]
conv_rhs => rw [sub_smul]
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (-↑n • x) = -↑n • ↑(Injective.factorThru G F) x
| (-↑n - 1) • ↑(Injective.factorThru G F) x
[PROOFSTEP]
rw [sub_smul]
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (-↑n • x) = -↑n • ↑(Injective.factorThru G F) x
| (-↑n - 1) • ↑(Injective.factorThru G F) x
[PROOFSTEP]
rw [sub_smul]
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (-↑n • x) = -↑n • ↑(Injective.factorThru G F) x
| (-↑n - 1) • ↑(Injective.factorThru G F) x
[PROOFSTEP]
rw [sub_smul]
[GOAL]
case refine_1.hn
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (-↑n • x) = -↑n • ↑(Injective.factorThru G F) x
⊢ ↑(Injective.factorThru G F) ((-↑n - 1) • x) = -↑n • ↑(Injective.factorThru G F) x - 1 • ↑(Injective.factorThru G F) x
[PROOFSTEP]
rw [← hn, one_smul, ← map_sub]
[GOAL]
case refine_1.hn
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (-↑n • x) = -↑n • ↑(Injective.factorThru G F) x
⊢ ↑(Injective.factorThru G F) ((-↑n - 1) • x) = ↑(Injective.factorThru G F) (-↑n • x - x)
[PROOFSTEP]
congr
[GOAL]
case refine_1.hn.h.e_6.h
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (-↑n • x) = -↑n • ↑(Injective.factorThru G F) x
⊢ (-↑n - 1) • x = -↑n • x - x
[PROOFSTEP]
convert @sub_smul ℤ Y _ _ ?_ (-n) 1 x
[GOAL]
case h.e'_3.h.e'_6
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑Y
n : ℕ
hn : ↑(Injective.factorThru G F) (-↑n • x) = -↑n • ↑(Injective.factorThru G F) x
⊢ x = 1 • x
[PROOFSTEP]
refine @one_smul ℤ Y _ ?_ x |>.symm
[GOAL]
case refine_2
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
⊢ f ≫
      { toAddHom := ↑(Injective.factorThru G F),
        map_smul' :=
          (_ :
            ∀ (r : ℤ) (x : ↑Y),
              ZeroHom.toFun (↑(Injective.factorThru G F)) (r • x) =
                ↑(RingHom.id ℤ) r • ZeroHom.toFun (↑(Injective.factorThru G F)) x) } =
    g
[PROOFSTEP]
ext x
[GOAL]
case refine_2.h
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this : Mono F
x : ↑X
⊢ ↑(f ≫
          { toAddHom := ↑(Injective.factorThru G F),
            map_smul' :=
              (_ :
                ∀ (r : ℤ) (x : ↑Y),
                  ZeroHom.toFun (↑(Injective.factorThru G F)) (r • x) =
                    ↑(RingHom.id ℤ) r • ZeroHom.toFun (↑(Injective.factorThru G F)) x) })
      x =
    ↑g x
[PROOFSTEP]
have := congrFun (congrArg (fun H => H.toFun) (Injective.comp_factorThru G F)) x
[GOAL]
case refine_2.h
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this✝ : Mono F
x : ↑X
this : (fun H => H.toFun) (F ≫ Injective.factorThru G F) x = (fun H => H.toFun) G x
⊢ ↑(f ≫
          { toAddHom := ↑(Injective.factorThru G F),
            map_smul' :=
              (_ :
                ∀ (r : ℤ) (x : ↑Y),
                  ZeroHom.toFun (↑(Injective.factorThru G F)) (r • x) =
                    ↑(RingHom.id ℤ) r • ZeroHom.toFun (↑(Injective.factorThru G F)) x) })
      x =
    ↑g x
[PROOFSTEP]
simp only [ModuleCat.coe_comp, Function.comp_apply] at this
[GOAL]
case refine_2.h
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : Injective (Bundled.mk A)
X Y : ModuleCat ℤ
g : X ⟶ ModuleCat.mk A
f : X ⟶ Y
m : Mono f
G : Bundled.mk ↑X ⟶ Bundled.mk A := LinearMap.toAddMonoidHom g
F : Bundled.mk ↑X ⟶ Bundled.mk ↑Y := LinearMap.toAddMonoidHom f
this✝ : Mono F
x : ↑X
this :
  ZeroHom.toFun
      (↑(LinearMap.toAddMonoidHom f ≫ Injective.factorThru (LinearMap.toAddMonoidHom g) (LinearMap.toAddMonoidHom f)))
      x =
    ZeroHom.toFun (↑(LinearMap.toAddMonoidHom g)) x
⊢ ↑(f ≫
          { toAddHom := ↑(Injective.factorThru G F),
            map_smul' :=
              (_ :
                ∀ (r : ℤ) (x : ↑Y),
                  ZeroHom.toFun (↑(Injective.factorThru G F)) (r • x) =
                    ↑(RingHom.id ℤ) r • ZeroHom.toFun (↑(Injective.factorThru G F)) x) })
      x =
    ↑g x
[PROOFSTEP]
apply this
[GOAL]
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
I : Ideal ℤ
g : { x // x ∈ I } →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ I), ↑g' x = ↑g { val := x, property := mem }
[PROOFSTEP]
rcases IsPrincipalIdealRing.principal I with ⟨m, rfl⟩
[GOAL]
case mk.intro
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), ↑g' x = ↑g { val := x, property := mem }
[PROOFSTEP]
by_cases m_eq_zero : m = 0
[GOAL]
case pos
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : m = 0
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), ↑g' x = ↑g { val := x, property := mem }
[PROOFSTEP]
subst m_eq_zero
[GOAL]
case pos
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : { x // x ∈ Submodule.span ℤ {0} } →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {0}), ↑g' x = ↑g { val := x, property := mem }
[PROOFSTEP]
refine'
  ⟨{  toFun := _
      map_add' := _
      map_smul' := _ }, fun n hn => _⟩
[GOAL]
case pos.refine'_1
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : { x // x ∈ Submodule.span ℤ {0} } →ₗ[ℤ] A
⊢ ℤ → A
[PROOFSTEP]
intro _
[GOAL]
case pos.refine'_1
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : { x // x ∈ Submodule.span ℤ {0} } →ₗ[ℤ] A
a✝ : ℤ
⊢ A
[PROOFSTEP]
exact g 0
[GOAL]
case pos.refine'_2
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : { x // x ∈ Submodule.span ℤ {0} } →ₗ[ℤ] A
⊢ ℤ → ℤ → ↑g 0 = ↑g 0 + ↑g 0
[PROOFSTEP]
intro _ _
[GOAL]
case pos.refine'_2
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : { x // x ∈ Submodule.span ℤ {0} } →ₗ[ℤ] A
x✝ y✝ : ℤ
⊢ ↑g 0 = ↑g 0 + ↑g 0
[PROOFSTEP]
simp only [map_zero, add_zero]
[GOAL]
case pos.refine'_3
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : { x // x ∈ Submodule.span ℤ {0} } →ₗ[ℤ] A
⊢ ∀ (r x : ℤ),
    AddHom.toFun { toFun := fun a => ↑g 0, map_add' := (_ : ℤ → ℤ → ↑g 0 = ↑g 0 + ↑g 0) } (r • x) =
      ↑(RingHom.id ℤ) r • AddHom.toFun { toFun := fun a => ↑g 0, map_add' := (_ : ℤ → ℤ → ↑g 0 = ↑g 0 + ↑g 0) } x
[PROOFSTEP]
intro n1 _
[GOAL]
case pos.refine'_3
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : { x // x ∈ Submodule.span ℤ {0} } →ₗ[ℤ] A
n1 x✝ : ℤ
⊢ AddHom.toFun { toFun := fun a => ↑g 0, map_add' := (_ : ℤ → ℤ → ↑g 0 = ↑g 0 + ↑g 0) } (n1 • x✝) =
    ↑(RingHom.id ℤ) n1 • AddHom.toFun { toFun := fun a => ↑g 0, map_add' := (_ : ℤ → ℤ → ↑g 0 = ↑g 0 + ↑g 0) } x✝
[PROOFSTEP]
simp only [map_zero, smul_zero]
[GOAL]
case pos.refine'_4
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : { x // x ∈ Submodule.span ℤ {0} } →ₗ[ℤ] A
n : ℤ
hn : n ∈ Submodule.span ℤ {0}
⊢ ↑{ toAddHom := { toFun := fun a => ↑g 0, map_add' := (_ : ℤ → ℤ → ↑g 0 = ↑g 0 + ↑g 0) },
          map_smul' := (_ : ∀ (n1 : ℤ), ℤ → ↑g 0 = ↑(RingHom.id ℤ) n1 • ↑g 0) }
      n =
    ↑g { val := n, property := hn }
[PROOFSTEP]
rw [Submodule.span_singleton_eq_bot.mpr rfl, Submodule.mem_bot] at hn
[GOAL]
case pos.refine'_4
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : { x // x ∈ Submodule.span ℤ {0} } →ₗ[ℤ] A
n : ℤ
hn✝ : n ∈ Submodule.span ℤ {0}
hn : n = 0
⊢ ↑{ toAddHom := { toFun := fun a => ↑g 0, map_add' := (_ : ℤ → ℤ → ↑g 0 = ↑g 0 + ↑g 0) },
          map_smul' := (_ : ∀ (n1 : ℤ), ℤ → ↑g 0 = ↑(RingHom.id ℤ) n1 • ↑g 0) }
      n =
    ↑g { val := n, property := hn✝ }
[PROOFSTEP]
simp only [hn, map_zero]
[GOAL]
case pos.refine'_4
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : { x // x ∈ Submodule.span ℤ {0} } →ₗ[ℤ] A
n : ℤ
hn✝ : n ∈ Submodule.span ℤ {0}
hn : n = 0
⊢ 0 = ↑g { val := 0, property := (_ : (fun x => x ∈ Submodule.span ℤ {0}) 0) }
[PROOFSTEP]
symm
[GOAL]
case pos.refine'_4
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : { x // x ∈ Submodule.span ℤ {0} } →ₗ[ℤ] A
n : ℤ
hn✝ : n ∈ Submodule.span ℤ {0}
hn : n = 0
⊢ ↑g { val := 0, property := (_ : (fun x => x ∈ Submodule.span ℤ {0}) 0) } = 0
[PROOFSTEP]
convert map_zero g
[GOAL]
case neg
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), ↑g' x = ↑g { val := x, property := mem }
[PROOFSTEP]
set gₘ := g ⟨m, Submodule.subset_span (Set.mem_singleton _)⟩ with gm_eq
[GOAL]
case neg
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ Submodule.span ℤ {m}), ↑g' x = ↑g { val := x, property := mem }
[PROOFSTEP]
refine'
  ⟨{  toFun := _
      map_add' := _
      map_smul' := _ }, fun n hn => _⟩
[GOAL]
case neg.refine'_1
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
⊢ ℤ → A
[PROOFSTEP]
intro n
[GOAL]
case neg.refine'_1
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n : ℤ
⊢ A
[PROOFSTEP]
exact n • DivisibleBy.div gₘ m
[GOAL]
case neg.refine'_2
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
⊢ ∀ (x y : ℤ), (x + y) • DivisibleBy.div gₘ m = x • DivisibleBy.div gₘ m + y • DivisibleBy.div gₘ m
[PROOFSTEP]
intro n1 n2
[GOAL]
case neg.refine'_2
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n1 n2 : ℤ
⊢ (n1 + n2) • DivisibleBy.div gₘ m = n1 • DivisibleBy.div gₘ m + n2 • DivisibleBy.div gₘ m
[PROOFSTEP]
simp only [add_smul]
[GOAL]
case neg.refine'_3
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
⊢ ∀ (r x : ℤ),
    AddHom.toFun
        { toFun := fun n => n • DivisibleBy.div gₘ m,
          map_add' :=
            (_ :
              ∀ (n1 n2 : ℤ),
                (n1 + n2) • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                  n1 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                    n2 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m) }
        (r • x) =
      ↑(RingHom.id ℤ) r •
        AddHom.toFun
          { toFun := fun n => n • DivisibleBy.div gₘ m,
            map_add' :=
              (_ :
                ∀ (n1 n2 : ℤ),
                  (n1 + n2) • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                    n1 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                      n2 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m) }
          x
[PROOFSTEP]
intro n1 n2
[GOAL]
case neg.refine'_3
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n1 n2 : ℤ
⊢ AddHom.toFun
      { toFun := fun n => n • DivisibleBy.div gₘ m,
        map_add' :=
          (_ :
            ∀ (n1 n2 : ℤ),
              (n1 + n2) • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                n1 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                  n2 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m) }
      (n1 • n2) =
    ↑(RingHom.id ℤ) n1 •
      AddHom.toFun
        { toFun := fun n => n • DivisibleBy.div gₘ m,
          map_add' :=
            (_ :
              ∀ (n1 n2 : ℤ),
                (n1 + n2) • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                  n1 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                    n2 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m) }
        n2
[PROOFSTEP]
dsimp
[GOAL]
case neg.refine'_3
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n1 n2 : ℤ
⊢ (n1 * n2) • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
    n1 • n2 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m
[PROOFSTEP]
rw [mul_smul]
[GOAL]
case neg.refine'_4
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n : ℤ
hn : n ∈ Submodule.span ℤ {m}
⊢ ↑{
          toAddHom :=
            { toFun := fun n => n • DivisibleBy.div gₘ m,
              map_add' :=
                (_ :
                  ∀ (n1 n2 : ℤ),
                    (n1 + n2) • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                      n1 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                        n2 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m) },
          map_smul' :=
            (_ :
              ∀ (n1 n2 : ℤ),
                AddHom.toFun
                    { toFun := fun n => n • DivisibleBy.div gₘ m,
                      map_add' :=
                        (_ :
                          ∀ (n1 n2 : ℤ),
                            (n1 + n2) •
                                DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                              n1 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                                n2 •
                                  DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m) }
                    (n1 • n2) =
                  ↑(RingHom.id ℤ) n1 •
                    AddHom.toFun
                      { toFun := fun n => n • DivisibleBy.div gₘ m,
                        map_add' :=
                          (_ :
                            ∀ (n1 n2 : ℤ),
                              (n1 + n2) •
                                  DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                                n1 •
                                    DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                                  n2 •
                                    DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) })
                                      m) }
                      n2) }
      n =
    ↑g { val := n, property := hn }
[PROOFSTEP]
rw [Submodule.mem_span_singleton] at hn
[GOAL]
case neg.refine'_4
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n : ℤ
hn✝ : n ∈ Submodule.span ℤ {m}
hn : ∃ a, a • m = n
⊢ ↑{
          toAddHom :=
            { toFun := fun n => n • DivisibleBy.div gₘ m,
              map_add' :=
                (_ :
                  ∀ (n1 n2 : ℤ),
                    (n1 + n2) • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                      n1 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                        n2 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m) },
          map_smul' :=
            (_ :
              ∀ (n1 n2 : ℤ),
                AddHom.toFun
                    { toFun := fun n => n • DivisibleBy.div gₘ m,
                      map_add' :=
                        (_ :
                          ∀ (n1 n2 : ℤ),
                            (n1 + n2) •
                                DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                              n1 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                                n2 •
                                  DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m) }
                    (n1 • n2) =
                  ↑(RingHom.id ℤ) n1 •
                    AddHom.toFun
                      { toFun := fun n => n • DivisibleBy.div gₘ m,
                        map_add' :=
                          (_ :
                            ∀ (n1 n2 : ℤ),
                              (n1 + n2) •
                                  DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                                n1 •
                                    DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                                  n2 •
                                    DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) })
                                      m) }
                      n2) }
      n =
    ↑g { val := n, property := hn✝ }
[PROOFSTEP]
rcases hn with ⟨n, rfl⟩
[GOAL]
case neg.refine'_4.intro
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n : ℤ
hn : n • m ∈ Submodule.span ℤ {m}
⊢ ↑{
          toAddHom :=
            { toFun := fun n => n • DivisibleBy.div gₘ m,
              map_add' :=
                (_ :
                  ∀ (n1 n2 : ℤ),
                    (n1 + n2) • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                      n1 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                        n2 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m) },
          map_smul' :=
            (_ :
              ∀ (n1 n2 : ℤ),
                AddHom.toFun
                    { toFun := fun n => n • DivisibleBy.div gₘ m,
                      map_add' :=
                        (_ :
                          ∀ (n1 n2 : ℤ),
                            (n1 + n2) •
                                DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                              n1 • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                                n2 •
                                  DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m) }
                    (n1 • n2) =
                  ↑(RingHom.id ℤ) n1 •
                    AddHom.toFun
                      { toFun := fun n => n • DivisibleBy.div gₘ m,
                        map_add' :=
                          (_ :
                            ∀ (n1 n2 : ℤ),
                              (n1 + n2) •
                                  DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
                                n1 •
                                    DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m +
                                  n2 •
                                    DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) })
                                      m) }
                      n2) }
      (n • m) =
    ↑g { val := n • m, property := hn }
[PROOFSTEP]
simp only [gm_eq, Algebra.id.smul_eq_mul, LinearMap.coe_mk]
[GOAL]
case neg.refine'_4.intro
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n : ℤ
hn : n • m ∈ Submodule.span ℤ {m}
⊢ ↑{ toFun := fun n => n • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m,
          map_add' :=
            (_ :
              ∀ (x y : ℤ),
                (fun n => n • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m)
                    (x + y) =
                  (fun n => n • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m) x +
                    (fun n => n • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m)
                      y) }
      (n * m) =
    ↑g { val := n * m, property := (_ : (fun x => x ∈ Submodule.span ℤ {m}) (n * m)) }
[PROOFSTEP]
dsimp
[GOAL]
case neg.refine'_4.intro
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n : ℤ
hn : n • m ∈ Submodule.span ℤ {m}
⊢ (n * m) • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
    ↑g { val := n * m, property := hn }
[PROOFSTEP]
rw [mul_smul]
  -- Porting note: used to be able to just rw [Div...]
[GOAL]
case neg.refine'_4.intro
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n : ℤ
hn : n • m ∈ Submodule.span ℤ {m}
⊢ n • m • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
    ↑g { val := n * m, property := hn }
[PROOFSTEP]
have s := congrArg (fun l => n • l) <| DivisibleBy.div_cancel gₘ m_eq_zero
[GOAL]
case neg.refine'_4.intro
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n : ℤ
hn : n • m ∈ Submodule.span ℤ {m}
s : (fun l => n • l) (m • DivisibleBy.div gₘ m) = (fun l => n • l) gₘ
⊢ n • m • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
    ↑g { val := n * m, property := hn }
[PROOFSTEP]
dsimp at s
[GOAL]
case neg.refine'_4.intro
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n : ℤ
hn : n • m ∈ Submodule.span ℤ {m}
s :
  n • m • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
    n • ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
⊢ n • m • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
    ↑g { val := n * m, property := hn }
[PROOFSTEP]
rw [s, ← LinearMap.map_smul]
[GOAL]
case neg.refine'_4.intro
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : { x // x ∈ Submodule.span ℤ {m} } →ₗ[ℤ] A
m_eq_zero : ¬m = 0
gₘ : A := ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
gm_eq : gₘ = ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
n : ℤ
hn : n • m ∈ Submodule.span ℤ {m}
s :
  n • m • DivisibleBy.div (↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) m =
    n • ↑g { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }
⊢ ↑g (n • { val := m, property := (_ : m ∈ ↑(Submodule.span ℤ {m})) }) = ↑g { val := n * m, property := hn }
[PROOFSTEP]
congr


[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ GroupCatMax
j : J
⊢ Group ((F ⋙ forget GroupCat).obj j)
[PROOFSTEP]
change Group (F.obj j)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ GroupCatMax
j : J
⊢ Group ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ GroupCat
src✝ : Submonoid ((j : J) → ↑((F ⋙ forget₂ GroupCat MonCat).obj j)) :=
  MonCat.sectionsSubmonoid (F ⋙ forget₂ GroupCat MonCat)
a : (j : J) → ↑(F.obj j)
ah :
  a ∈
    {
          toSubsemigroup :=
            { carrier := Functor.sections (F ⋙ forget GroupCat),
              mul_mem' :=
                (_ : ∀ {a b : (j : J) → ↑(F.obj j)}, a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) },
          one_mem' :=
            (_ :
              ∀ {j j' : J} (f : j ⟶ j'),
                ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).map f (OfNat.ofNat 1 j) =
                  OfNat.ofNat 1 j') }.toSubsemigroup.carrier
j j' : J
f : j ⟶ j'
⊢ (F ⋙ forget GroupCat).map f (a⁻¹ j) = a⁻¹ j'
[PROOFSTEP]
simp only [Functor.comp_map, Pi.inv_apply, MonoidHom.map_inv, inv_inj]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ GroupCat
src✝ : Submonoid ((j : J) → ↑((F ⋙ forget₂ GroupCat MonCat).obj j)) :=
  MonCat.sectionsSubmonoid (F ⋙ forget₂ GroupCat MonCat)
a : (j : J) → ↑(F.obj j)
ah :
  a ∈
    {
          toSubsemigroup :=
            { carrier := Functor.sections (F ⋙ forget GroupCat),
              mul_mem' :=
                (_ : ∀ {a b : (j : J) → ↑(F.obj j)}, a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) },
          one_mem' :=
            (_ :
              ∀ {j j' : J} (f : j ⟶ j'),
                ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat).map f (OfNat.ofNat 1 j) =
                  OfNat.ofNat 1 j') }.toSubsemigroup.carrier
j j' : J
f : j ⟶ j'
⊢ (forget GroupCat).map (F.map f) (a j)⁻¹ = (a j')⁻¹
[PROOFSTEP]
dsimp [Functor.sections] at ah ⊢
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ GroupCat
src✝ : Submonoid ((j : J) → ↑((F ⋙ forget₂ GroupCat MonCat).obj j)) :=
  MonCat.sectionsSubmonoid (F ⋙ forget₂ GroupCat MonCat)
a : (j : J) → ↑(F.obj j)
ah : a ∈ {u | ∀ {j j' : J} (f : j ⟶ j'), ↑(F.map f) (u j) = u j'}
j j' : J
f : j ⟶ j'
⊢ ↑(F.map f) (a j)⁻¹ = (a j')⁻¹
[PROOFSTEP]
rw [(F.map f).map_inv (a j), ah f]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ GroupCatMax
⊢ Group (Types.limitCone (F ⋙ forget GroupCat)).pt
[PROOFSTEP]
change Group (sectionsSubgroup.{v, u} F)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ GroupCatMax
⊢ Group { x // x ∈ sectionsSubgroup F }
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ GroupCatMax
this : ReflectsIsomorphisms (forget₂ GroupCatMax MonCatMax) := reflectsIsomorphisms_forget₂ GroupCatMax MonCatMax
c' : Cone (F ⋙ forget₂ GroupCat MonCat)
t : IsLimit c'
⊢ (forget₂ GroupCat MonCat).mapCone
      { pt := of (Types.limitCone (F ⋙ forget GroupCatMax)).pt,
        π := NatTrans.mk (MonCat.limitπMonoidHom (F ⋙ forget₂ GroupCatMax MonCatMax)) } ≅
    c'
[PROOFSTEP]
apply IsLimit.uniqueUpToIso (MonCat.HasLimits.limitConeIsLimit.{v, u} _) t
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommGroupCatMax
j : J
⊢ CommGroup ((F ⋙ forget CommGroupCatMax).obj j)
[PROOFSTEP]
change CommGroup (F.obj j)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommGroupCatMax
j : J
⊢ CommGroup ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommGroupCatMax
this : ReflectsIsomorphisms (forget₂ CommGroupCatMax GroupCatMax) :=
  reflectsIsomorphisms_forget₂ CommGroupCatMax GroupCatMax
c' : Cone (F ⋙ forget₂ CommGroupCat GroupCatMax)
t : IsLimit c'
⊢ (forget₂ CommGroupCat GroupCatMax).mapCone
      { pt := of (Types.limitCone (F ⋙ forget CommGroupCat)).pt,
        π := NatTrans.mk (MonCat.limitπMonoidHom (F ⋙ forget₂ CommGroupCat GroupCat ⋙ forget₂ GroupCat MonCat)) } ≅
    c'
[PROOFSTEP]
apply IsLimit.uniqueUpToIso (GroupCat.limitConeIsLimit _) t
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommGroupCatMax
this : ReflectsIsomorphisms (forget₂ CommGroupCatMax GroupCatMax) :=
  reflectsIsomorphisms_forget₂ CommGroupCatMax GroupCatMax
c' : Cone (F ⋙ forget₂ CommGroupCat GroupCatMax)
t : IsLimit c'
⊢ IsLimit
    ((forget₂ CommGroupCatMax GroupCat ⋙ forget₂ GroupCat MonCat).mapCone
      {
          liftedCone :=
            { pt := of (Types.limitCone (F ⋙ forget CommGroupCat)).pt,
              π := NatTrans.mk (MonCat.limitπMonoidHom (F ⋙ forget₂ CommGroupCat GroupCat ⋙ forget₂ GroupCat MonCat)) },
          validLift :=
            IsLimit.uniqueUpToIso (GroupCat.limitConeIsLimit (F ⋙ forget₂ CommGroupCat GroupCatMax)) t }.liftedCone)
[PROOFSTEP]
apply MonCat.HasLimits.limitConeIsLimit _
[GOAL]
J✝ : Type v
inst✝ : SmallCategory J✝
J : Type v
𝒥 : Category.{v, v} J
F : J ⥤ CommGroupCatMax
⊢ PreservesLimit F (forget₂ CommGroupCatMax GroupCatMax)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
f : ℕ → AddCommGroupCat
⊢ HasProduct f
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
⊢ (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0
[PROOFSTEP]
refine Subtype.ext ?_
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
⊢ ↑((fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0) = ↑0
[PROOFSTEP]
simp [(AddSubgroup.coe_zero _).symm]
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
g g' : ↑(kernel f)
⊢ ZeroHom.toFun
      { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
        map_zero' := (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
      (g + g') =
    ZeroHom.toFun
        { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
          map_zero' := (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
        g +
      ZeroHom.toFun
        { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
          map_zero' := (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
        g'
[PROOFSTEP]
refine Subtype.ext ?_
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
g g' : ↑(kernel f)
⊢ ↑(ZeroHom.toFun
        { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
          map_zero' := (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
        (g + g')) =
    ↑(ZeroHom.toFun
          { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
            map_zero' :=
              (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
          g +
        ZeroHom.toFun
          { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
            map_zero' :=
              (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
          g')
[PROOFSTEP]
change _ = _ + _
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
g g' : ↑(kernel f)
⊢ ↑(ZeroHom.toFun
        { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
          map_zero' := (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
        (g + g')) =
    ↑(ZeroHom.toFun
          { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
            map_zero' :=
              (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
          g) +
      ↑(ZeroHom.toFun
          { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
            map_zero' :=
              (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
          g')
[PROOFSTEP]
dsimp
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
g g' : ↑(kernel f)
⊢ ↑(kernel.ι f) (g + g') = ↑(kernel.ι f) g + ↑(kernel.ι f) g'
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
⊢ AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0
[PROOFSTEP]
refine FunLike.ext _ _ ?_
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
⊢ ∀ (x : ↑(of { x // x ∈ AddMonoidHom.ker f })), ↑(AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f) x = ↑0 x
[PROOFSTEP]
rintro ⟨x, (hx : f _ = 0)⟩
[GOAL]
case mk
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
hx : ↑f x = 0
⊢ ↑(AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f) { val := x, property := hx } = ↑0 { val := x, property := hx }
[PROOFSTEP]
exact hx
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
⊢ {
        toZeroHom :=
          { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
            map_zero' :=
              (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) },
        map_add' :=
          (_ :
            ∀ (g g' : ↑(kernel f)),
              ZeroHom.toFun
                  { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                    map_zero' :=
                      (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
                  (g + g') =
                ZeroHom.toFun
                    { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                      map_zero' :=
                        (_ :
                          (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
                    g +
                  ZeroHom.toFun
                    { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                      map_zero' :=
                        (_ :
                          (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
                    g') } ≫
      kernel.lift f (AddSubgroup.subtype (AddMonoidHom.ker f)) (_ : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0) =
    𝟙 (kernel f)
[PROOFSTEP]
refine equalizer.hom_ext ?_
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
⊢ ({
          toZeroHom :=
            { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
              map_zero' :=
                (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) },
          map_add' :=
            (_ :
              ∀ (g g' : ↑(kernel f)),
                ZeroHom.toFun
                    { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                      map_zero' :=
                        (_ :
                          (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
                    (g + g') =
                  ZeroHom.toFun
                      { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                        map_zero' :=
                          (_ :
                            (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
                      g +
                    ZeroHom.toFun
                      { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                        map_zero' :=
                          (_ :
                            (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
                      g') } ≫
        kernel.lift f (AddSubgroup.subtype (AddMonoidHom.ker f))
          (_ : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0)) ≫
      equalizer.ι f 0 =
    𝟙 (kernel f) ≫ equalizer.ι f 0
[PROOFSTEP]
ext x
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x : ↑(kernel f)
⊢ ↑(({
              toZeroHom :=
                { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                  map_zero' :=
                    (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) },
              map_add' :=
                (_ :
                  ∀ (g g' : ↑(kernel f)),
                    ZeroHom.toFun
                        { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                          map_zero' :=
                            (_ :
                              (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 =
                                0) }
                        (g + g') =
                      ZeroHom.toFun
                          { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                            map_zero' :=
                              (_ :
                                (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 =
                                  0) }
                          g +
                        ZeroHom.toFun
                          { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                            map_zero' :=
                              (_ :
                                (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 =
                                  0) }
                          g') } ≫
            kernel.lift f (AddSubgroup.subtype (AddMonoidHom.ker f))
              (_ : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0)) ≫
          equalizer.ι f 0)
      x =
    ↑(𝟙 (kernel f) ≫ equalizer.ι f 0) x
[PROOFSTEP]
dsimp
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x : ↑(kernel f)
⊢ ↑(kernel.ι f)
      (↑(kernel.lift f (AddSubgroup.subtype (AddMonoidHom.ker f))
            (_ : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0))
        { val := ↑(kernel.ι f) x, property := (_ : ↑(kernel.ι f ≫ f) x = ↑0 x) }) =
    ↑(kernel.ι f) x
[PROOFSTEP]
generalize_proofs _ h1 h2
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x : ↑(kernel f)
h✝ : HasKernel f
h1 : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0
h2 : ↑(kernel.ι f ≫ f) x = ↑0 x
⊢ ↑(kernel.ι f)
      (↑(kernel.lift f (AddSubgroup.subtype (AddMonoidHom.ker f)) h1) { val := ↑(kernel.ι f) x, property := h2 }) =
    ↑(kernel.ι f) x
[PROOFSTEP]
erw [FunLike.congr_fun (kernel.lift_ι f _ h1) ⟨_, h2⟩]
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x : ↑(kernel f)
h✝ : HasKernel f
h1 : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0
h2 : ↑(kernel.ι f ≫ f) x = ↑0 x
⊢ ↑(AddSubgroup.subtype (AddMonoidHom.ker f)) { val := ↑(kernel.ι f) x, property := h2 } = ↑(kernel.ι f) x
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
⊢ kernel.lift f (AddSubgroup.subtype (AddMonoidHom.ker f)) (_ : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0) ≫
      {
        toZeroHom :=
          { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
            map_zero' :=
              (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) },
        map_add' :=
          (_ :
            ∀ (g g' : ↑(kernel f)),
              ZeroHom.toFun
                  { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                    map_zero' :=
                      (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
                  (g + g') =
                ZeroHom.toFun
                    { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                      map_zero' :=
                        (_ :
                          (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
                    g +
                  ZeroHom.toFun
                    { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                      map_zero' :=
                        (_ :
                          (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) }
                    g') } =
    𝟙 (of { x // x ∈ AddMonoidHom.ker f })
[PROOFSTEP]
apply AddCommGroupCat.ext
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
⊢ ∀ (x : ↑(of { x // x ∈ AddMonoidHom.ker f })),
    ↑(kernel.lift f (AddSubgroup.subtype (AddMonoidHom.ker f)) (_ : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0) ≫
            {
              toZeroHom :=
                { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                  map_zero' :=
                    (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) },
              map_add' :=
                (_ :
                  ∀ (g g' : ↑(kernel f)),
                    ZeroHom.toFun
                        { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                          map_zero' :=
                            (_ :
                              (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 =
                                0) }
                        (g + g') =
                      ZeroHom.toFun
                          { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                            map_zero' :=
                              (_ :
                                (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 =
                                  0) }
                          g +
                        ZeroHom.toFun
                          { toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
                            map_zero' :=
                              (_ :
                                (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 =
                                  0) }
                          g') })
        x =
      ↑(𝟙 (of { x // x ∈ AddMonoidHom.ker f })) x
[PROOFSTEP]
simp only [AddMonoidHom.coe_mk, coe_id, coe_comp]
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
⊢ ∀ (x : ↑(of { x // x ∈ AddMonoidHom.ker f })),
    (↑{ toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
              map_zero' :=
                (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) } ∘
          ↑(kernel.lift f (AddSubgroup.subtype (AddMonoidHom.ker f))
              (_ : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0)))
        x =
      id x
[PROOFSTEP]
rintro ⟨x, mem⟩
[GOAL]
case w.mk
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
mem : x ∈ AddMonoidHom.ker f
⊢ (↑{ toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
            map_zero' :=
              (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) } ∘
        ↑(kernel.lift f (AddSubgroup.subtype (AddMonoidHom.ker f))
            (_ : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0)))
      { val := x, property := mem } =
    id { val := x, property := mem }
[PROOFSTEP]
refine Subtype.ext ?_
[GOAL]
case w.mk
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
mem : x ∈ AddMonoidHom.ker f
⊢ ↑((↑{ toFun := fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) },
              map_zero' :=
                (_ : (fun g => { val := ↑(kernel.ι f) g, property := (_ : ↑(kernel.ι f ≫ f) g = ↑0 g) }) 0 = 0) } ∘
          ↑(kernel.lift f (AddSubgroup.subtype (AddMonoidHom.ker f))
              (_ : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0)))
        { val := x, property := mem }) =
    ↑(id { val := x, property := mem })
[PROOFSTEP]
simp only [ZeroHom.coe_mk, Function.comp_apply, id_eq]
[GOAL]
case w.mk
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
mem : x ∈ AddMonoidHom.ker f
⊢ ↑(kernel.ι f)
      (↑(kernel.lift f (AddSubgroup.subtype (AddMonoidHom.ker f))
            (_ : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0))
        { val := x, property := mem }) =
    x
[PROOFSTEP]
generalize_proofs _ h1 h2
[GOAL]
case w.mk
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
mem : x ∈ AddMonoidHom.ker f
h✝ : HasKernel f
h1 : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0
⊢ ↑(kernel.ι f) (↑(kernel.lift f (AddSubgroup.subtype (AddMonoidHom.ker f)) h1) { val := x, property := mem }) = x
[PROOFSTEP]
erw [FunLike.congr_fun (kernel.lift_ι f _ h1) ⟨_, mem⟩]
[GOAL]
case w.mk
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x : ↑G
mem : x ∈ AddMonoidHom.ker f
h✝ : HasKernel f
h1 : AddSubgroup.subtype (AddMonoidHom.ker f) ≫ f = 0
⊢ ↑(AddSubgroup.subtype (AddMonoidHom.ker f)) { val := x, property := mem } = x
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
⊢ (kernelIsoKer f).hom ≫ AddSubgroup.subtype (AddMonoidHom.ker f) = kernel.ι f
[PROOFSTEP]
ext
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x✝ : ↑(kernel f)
⊢ ↑((kernelIsoKer f).hom ≫ AddSubgroup.subtype (AddMonoidHom.ker f)) x✝ = ↑(kernel.ι f) x✝
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
⊢ (kernelIsoKer f).inv ≫ kernel.ι f = AddSubgroup.subtype (AddMonoidHom.ker f)
[PROOFSTEP]
ext
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x✝ : ↑(of { x // x ∈ AddMonoidHom.ker f })
⊢ ↑((kernelIsoKer f).inv ≫ kernel.ι f) x✝ = ↑(AddSubgroup.subtype (AddMonoidHom.ker f)) x✝
[PROOFSTEP]
simp [kernelIsoKer]