[GOAL]
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) (x + y) =
    (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) x +
      (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) y
[PROOFSTEP]
apply (mono_iff_injective F'.m).1
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ Mono F'.m
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ ↑F'.m
      ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
        (x + y)) =
    ↑F'.m
      ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) x +
        (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) y)
[PROOFSTEP]
infer_instance
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ ↑F'.m
      ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
        (x + y)) =
    ↑F'.m
      ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) x +
        (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) y)
[PROOFSTEP]
rw [LinearMap.map_add]
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ ↑F'.m
      ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
        (x + y)) =
    ↑F'.m
        ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) x) +
      ↑F'.m
        ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) y)
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = (F'.e ≫ F'.m) _ + (F'.e ≫ F'.m) _
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑(x + y)) (_ : ↑(x + y) ∈ LinearMap.range f)) =
    ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)) +
      ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑y) (_ : ↑y ∈ LinearMap.range f))
[PROOFSTEP]
simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ AddHom.toFun
      {
        toFun := fun x =>
          ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
        map_add' :=
          (_ :
            ∀ (x y : ↑(image f)),
              (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                  (x + y) =
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                    x +
                  (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                    y) }
      (c • x) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
          map_add' :=
            (_ :
              ∀ (x y : ↑(image f)),
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                    (x + y) =
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      x +
                    (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      y) }
        x
[PROOFSTEP]
apply (mono_iff_injective F'.m).1
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ Mono F'.m
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ ↑F'.m
      (AddHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
          map_add' :=
            (_ :
              ∀ (x y : ↑(image f)),
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                    (x + y) =
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      x +
                    (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      y) }
        (c • x)) =
    ↑F'.m
      (↑(RingHom.id R) c •
        AddHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
            map_add' :=
              (_ :
                ∀ (x y : ↑(image f)),
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      (x + y) =
                    (fun x =>
                          ↑F'.e
                            ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                        x +
                      (fun x =>
                          ↑F'.e
                            ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                        y) }
          x)
[PROOFSTEP]
infer_instance
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ ↑F'.m
      (AddHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
          map_add' :=
            (_ :
              ∀ (x y : ↑(image f)),
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                    (x + y) =
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      x +
                    (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      y) }
        (c • x)) =
    ↑F'.m
      (↑(RingHom.id R) c •
        AddHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
            map_add' :=
              (_ :
                ∀ (x y : ↑(image f)),
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      (x + y) =
                    (fun x =>
                          ↑F'.e
                            ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                        x +
                      (fun x =>
                          ↑F'.e
                            ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                        y) }
          x)
[PROOFSTEP]
rw [LinearMap.map_smul]
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ ↑F'.m
      (AddHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
          map_add' :=
            (_ :
              ∀ (x y : ↑(image f)),
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                    (x + y) =
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      x +
                    (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      y) }
        (c • x)) =
    ↑(RingHom.id R) c •
      ↑F'.m
        (AddHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
            map_add' :=
              (_ :
                ∀ (x y : ↑(image f)),
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      (x + y) =
                    (fun x =>
                          ↑F'.e
                            ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                        x +
                      (fun x =>
                          ↑F'.e
                            ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                        y) }
          x)
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = _ • (F'.e ≫ F'.m) _
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑(c • x)) (_ : ↑(c • x) ∈ LinearMap.range f)) =
    ↑(RingHom.id R) c •
      ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))
[PROOFSTEP]
simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ ↑(c • x) = ↑(RingHom.id R) c • ↑x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑(lift F' ≫ F'.m) x = ↑(ι f) x
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = _
[GOAL]
case h
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)) = ↑(ι f) x
[PROOFSTEP]
rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]
[GOAL]
case h
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑x = ↑(ι f) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
G✝ H✝ : ModuleCat R
f✝ : G✝ ⟶ H✝
G H : ModuleCat R
f : G ⟶ H
⊢ (imageIsoRange f).hom ≫ ofHom (Submodule.subtype (LinearMap.range f)) = Limits.image.ι f
[PROOFSTEP]
erw [← imageIsoRange_inv_image_ι f, Iso.hom_inv_id_assoc]
