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