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
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
let G : (⟨X,inferInstance⟩ : AddCommGroupCat) ⟶ ⟨A,inferInstance⟩ :=
  @LinearMap.toAddMonoidHom _ _ _ _ _ _ _ _ (_) _ _ g
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
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
let F : (⟨X,inferInstance⟩ : AddCommGroupCat) ⟶ ⟨Y,inferInstance⟩ :=
  @LinearMap.toAddMonoidHom _ _ _ _ _ _ _ _ (_) (_) _ f
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
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
have : Mono F := by
  rw [mono_iff_injective]
  intro _ _ h
  exact ((ModuleCat.mono_iff_injective f).mp m) h
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
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
refine ⟨ @LinearMap.mk _ _ _ _ _ _ _ _ _ (_) _ (Injective.factorThru G F).toAddHom ?_ , ?_⟩
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

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
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
change ∀ r, ∀ x, (Injective.factorThru G F).toFun _ = _ • (Injective.factorThru G F).toFun _
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
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
ext x
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
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
have := congrFun (congrArg (fun H => H.toFun) (Injective.comp_factorThru G F)) x
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
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
simp only [ModuleCat.coe_comp, Function.comp_apply] at this
no goals
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
apply this
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
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
rw [mono_iff_injective]
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₂✝
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
intro _ _ h
no goals
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₂✝
exact ((ModuleCat.mono_iff_injective f).mp m) h
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
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
intro m x
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
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
rw [AddMonoidHom.toFun_eq_coe, RingHom.id_apply]
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

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

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
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
induction' m using Int.induction_on with n hn n hn
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
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
rw [zero_smul]
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
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
convert map_zero (M := Y) (N := A) (F := Y →+ A) _
no goals
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
refine @zero_smul ℤ Y (MonoidWithZero.toZero) (AddMonoid.toZero) ?_ x
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
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
conv_rhs => rw [add_smul]
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)
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
rw [← hn, one_smul, ←map_add]
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
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)
congr
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
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
convert @add_smul ℤ Y _ _ ?_ n 1 x
no goals
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
refine @one_smul ℤ Y _ ?_ x|>.symm
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
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
conv_rhs => rw [sub_smul]
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)
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
rw [← hn, one_smul, ←map_sub]
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
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)
congr
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
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
convert @sub_smul ℤ Y _ _ ?_ (-n) 1 x
no goals
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
refine @one_smul ℤ Y _ ?_ x|>.symm