[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
