[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
⊢ factorThruImage f ≫ ι f = f
[PROOFSTEP]
ext
[GOAL]
case w
G H : AddCommGroupCat
f : G ⟶ H
x✝ : ↑G
⊢ ↑(factorThruImage f ≫ ι f) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f))) 0 = 0
[PROOFSTEP]
haveI := F'.m_mono
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f))) 0 = 0
[PROOFSTEP]
apply injective_of_mono F'.m
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ ↑F'.m
      ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f))) 0) =
    ↑F'.m 0
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = _
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑0) (_ : ↑0 ∈ AddMonoidHom.range f)) = ↑F'.m 0
[PROOFSTEP]
rw [F'.fac, AddMonoidHom.map_zero]
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ ↑f ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑0) (_ : ↑0 ∈ AddMonoidHom.range f)) = 0
[PROOFSTEP]
exact (Classical.indefiniteDescription (fun y => f y = 0) _).2
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ ∀ (x y : ↑(image f)),
    ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        (x + y) =
      ZeroHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
            map_zero' :=
              (_ :
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                    0 =
                  0) }
          x +
        ZeroHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
            map_zero' :=
              (_ :
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                    0 =
                  0) }
          y
[PROOFSTEP]
intro x y
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ ZeroHom.toFun
      {
        toFun := fun x =>
          ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
        map_zero' :=
          (_ :
            (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                0 =
              0) }
      (x + y) =
    ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        x +
      ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        y
[PROOFSTEP]
haveI := F'.m_mono
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ZeroHom.toFun
      {
        toFun := fun x =>
          ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
        map_zero' :=
          (_ :
            (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                0 =
              0) }
      (x + y) =
    ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        x +
      ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        y
[PROOFSTEP]
apply injective_of_mono F'.m
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑F'.m
      (ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        (x + y)) =
    ↑F'.m
      (ZeroHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
            map_zero' :=
              (_ :
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                    0 =
                  0) }
          x +
        ZeroHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
            map_zero' :=
              (_ :
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                    0 =
                  0) }
          y)
[PROOFSTEP]
rw [AddMonoidHom.map_add]
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑F'.m
      (ZeroHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
          map_zero' :=
            (_ :
              (fun x =>
                    ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                  0 =
                0) }
        (x + y)) =
    ↑F'.m
        (ZeroHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
            map_zero' :=
              (_ :
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                    0 =
                  0) }
          x) +
      ↑F'.m
        (ZeroHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)),
            map_zero' :=
              (_ :
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)))
                    0 =
                  0) }
          y)
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = (F'.e ≫ F'.m) _ + (F'.e ≫ F'.m) _
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑(F'.e ≫ F'.m)
      ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑(x + y)) (_ : ↑(x + y) ∈ AddMonoidHom.range f)) =
    ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)) +
      ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑y) (_ : ↑y ∈ AddMonoidHom.range f))
[PROOFSTEP]
rw [F'.fac]
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑f ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑(x + y)) (_ : ↑(x + y) ∈ AddMonoidHom.range f)) =
    ↑f ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)) +
      ↑f ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑y) (_ : ↑y ∈ AddMonoidHom.range f))
[PROOFSTEP]
rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑(x + y) =
    ↑f ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)) +
      ↑f ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑y) (_ : ↑y ∈ AddMonoidHom.range f))
[PROOFSTEP]
rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑(x + y) = ↑x + ↑f ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑y) (_ : ↑y ∈ AddMonoidHom.range f))
[PROOFSTEP]
rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
[GOAL]
case a
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
this : Mono F'.m
⊢ ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
rfl
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f
[PROOFSTEP]
ext x
[GOAL]
case w
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑(lift F' ≫ F'.m) x = ↑(ι f) x
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = _
[GOAL]
case w
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ AddMonoidHom.range f)) = ↑(ι f) x
[PROOFSTEP]
rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]
[GOAL]
case w
G H : AddCommGroupCat
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑x = ↑(ι f) x
[PROOFSTEP]
rfl
