[GOAL]
⊢ ∀ {X' X : Type u} {Y : AddCommGroupCat} (f : X' ⟶ X) (g : X ⟶ (forget AddCommGroupCat).obj Y),
    ↑((fun X G => FreeAbelianGroup.lift.symm) X' Y).symm (f ≫ g) =
      free.map f ≫ ↑((fun X G => FreeAbelianGroup.lift.symm) X Y).symm g
[PROOFSTEP]
intros
[GOAL]
X'✝ X✝ : Type u
Y✝ : AddCommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget AddCommGroupCat).obj Y✝
⊢ ↑((fun X G => FreeAbelianGroup.lift.symm) X'✝ Y✝).symm (f✝ ≫ g✝) =
    free.map f✝ ≫ ↑((fun X G => FreeAbelianGroup.lift.symm) X✝ Y✝).symm g✝
[PROOFSTEP]
ext
[GOAL]
case w
X'✝ X✝ : Type u
Y✝ : AddCommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget AddCommGroupCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ ↑(↑((fun X G => FreeAbelianGroup.lift.symm) X'✝ Y✝).symm (f✝ ≫ g✝)) x✝ =
    ↑(free.map f✝ ≫ ↑((fun X G => FreeAbelianGroup.lift.symm) X✝ Y✝).symm g✝) x✝
[PROOFSTEP]
simp only [Equiv.symm_symm]
[GOAL]
case w
X'✝ X✝ : Type u
Y✝ : AddCommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget AddCommGroupCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ ↑(↑FreeAbelianGroup.lift (f✝ ≫ g✝)) x✝ = ↑(free.map f✝ ≫ ↑FreeAbelianGroup.lift g✝) x✝
[PROOFSTEP]
apply FreeAbelianGroup.lift_comp
[GOAL]
⊢ ∀ (X : Type u),
    { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map (𝟙 X) =
      𝟙 ({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X)
[PROOFSTEP]
intros
[GOAL]
X✝ : Type u
⊢ { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map (𝟙 X✝) =
    𝟙 ({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
[PROOFSTEP]
ext1
[GOAL]
case w
X✝ : Type u
x✝ : ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
⊢ ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map (𝟙 X✝)) x✝ =
    ↑(𝟙 ({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)) x✝
[PROOFSTEP]
rw [← FreeGroup.map.unique]
[GOAL]
case w.hg
X✝ : Type u
x✝ : ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
⊢ ∀ (x : X✝),
    ↑(𝟙 ({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)) (FreeGroup.of x) =
      FreeGroup.of (𝟙 X✝ x)
[PROOFSTEP]
intros
[GOAL]
case w.hg
X✝ : Type u
x✝¹ : ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
x✝ : X✝
⊢ ↑(𝟙 ({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)) (FreeGroup.of x✝) =
    FreeGroup.of (𝟙 X✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map (f ≫ g) =
      { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map f ≫
        { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map g
[PROOFSTEP]
intros
[GOAL]
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map (f✝ ≫ g✝) =
    { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map f✝ ≫
      { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map g✝
[PROOFSTEP]
ext1
[GOAL]
case w
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
⊢ ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map (f✝ ≫ g✝)) x✝ =
    ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map f✝ ≫
          { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map g✝)
      x✝
[PROOFSTEP]
rw [← FreeGroup.map.unique]
[GOAL]
case w.hg
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
⊢ ∀ (x : X✝),
    ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map f✝ ≫
            { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map g✝)
        (FreeGroup.of x) =
      FreeGroup.of ((f✝ ≫ g✝) x)
[PROOFSTEP]
intros
[GOAL]
case w.hg
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝¹ : ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
x✝ : X✝
⊢ ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map f✝ ≫
          { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map g✝)
      (FreeGroup.of x✝) =
    FreeGroup.of ((f✝ ≫ g✝) x✝)
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {X' X : Type u} {Y : GroupCat} (f : X' ⟶ X) (g : X ⟶ (forget GroupCat).obj Y),
    ↑((fun X G => FreeGroup.lift.symm) X' Y).symm (f ≫ g) = free.map f ≫ ↑((fun X G => FreeGroup.lift.symm) X Y).symm g
[PROOFSTEP]
intros
[GOAL]
X'✝ X✝ : Type u
Y✝ : GroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GroupCat).obj Y✝
⊢ ↑((fun X G => FreeGroup.lift.symm) X'✝ Y✝).symm (f✝ ≫ g✝) =
    free.map f✝ ≫ ↑((fun X G => FreeGroup.lift.symm) X✝ Y✝).symm g✝
[PROOFSTEP]
ext1
[GOAL]
case w
X'✝ X✝ : Type u
Y✝ : GroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GroupCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ ↑(↑((fun X G => FreeGroup.lift.symm) X'✝ Y✝).symm (f✝ ≫ g✝)) x✝ =
    ↑(free.map f✝ ≫ ↑((fun X G => FreeGroup.lift.symm) X✝ Y✝).symm g✝) x✝
[PROOFSTEP]
simp only [Equiv.symm_symm]
[GOAL]
case w
X'✝ X✝ : Type u
Y✝ : GroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GroupCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ ↑(↑FreeGroup.lift (f✝ ≫ g✝)) x✝ = ↑(free.map f✝ ≫ ↑FreeGroup.lift g✝) x✝
[PROOFSTEP]
apply Eq.symm
[GOAL]
case w.h
X'✝ X✝ : Type u
Y✝ : GroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GroupCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ ↑(free.map f✝ ≫ ↑FreeGroup.lift g✝) x✝ = ↑(↑FreeGroup.lift (f✝ ≫ g✝)) x✝
[PROOFSTEP]
apply FreeGroup.lift.unique
[GOAL]
case w.h.hg
X'✝ X✝ : Type u
Y✝ : GroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GroupCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ ∀ (x : X'✝), ↑(free.map f✝ ≫ ↑FreeGroup.lift g✝) (FreeGroup.of x) = (f✝ ≫ g✝) x
[PROOFSTEP]
intros
[GOAL]
case w.h.hg
X'✝ X✝ : Type u
Y✝ : GroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GroupCat).obj Y✝
x✝¹ : ↑(free.obj X'✝)
x✝ : X'✝
⊢ ↑(free.map f✝ ≫ ↑FreeGroup.lift g✝) (FreeGroup.of x✝) = (f✝ ≫ g✝) x✝
[PROOFSTEP]
apply FreeGroup.lift.of
[GOAL]
G : GroupCat
⊢ CommGroup (Abelianization ↑G)
[PROOFSTEP]
infer_instance
[GOAL]
X✝ Y✝ : GroupCat
f : X✝ ⟶ Y✝
⊢ (fun x => ↑Abelianization.of (↑f x)) 1 = 1
[PROOFSTEP]
simp
[GOAL]
X✝ Y✝ : GroupCat
f : X✝ ⟶ Y✝
⊢ ∀ (x y : ↑X✝),
    OneHom.toFun { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) }
        (x * y) =
      OneHom.toFun { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) } x *
        OneHom.toFun { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) } y
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ (X : GroupCat),
    { obj := fun G => Bundled.mk (Abelianization ↑G),
            map := fun {X Y} f =>
              ↑Abelianization.lift
                {
                  toOneHom :=
                    { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a a_1 : ↑X),
                        ↑Abelianization.of (↑f (a * a_1)) =
                          ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
        (𝟙 X) =
      𝟙
        ({ obj := fun G => Bundled.mk (Abelianization ↑G),
              map := fun {X Y} f =>
                ↑Abelianization.lift
                  {
                    toOneHom :=
                      { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (a a_1 : ↑X),
                          ↑Abelianization.of (↑f (a * a_1)) =
                            ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.obj
          X)
[PROOFSTEP]
intros
[GOAL]
X✝ : GroupCat
⊢ { obj := fun G => Bundled.mk (Abelianization ↑G),
          map := fun {X Y} f =>
            ↑Abelianization.lift
              {
                toOneHom :=
                  { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a a_1 : ↑X),
                      ↑Abelianization.of (↑f (a * a_1)) =
                        ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
      (𝟙 X✝) =
    𝟙
      ({ obj := fun G => Bundled.mk (Abelianization ↑G),
            map := fun {X Y} f =>
              ↑Abelianization.lift
                {
                  toOneHom :=
                    { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a a_1 : ↑X),
                        ↑Abelianization.of (↑f (a * a_1)) =
                          ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.obj
        X✝)
[PROOFSTEP]
simp only [MonoidHom.mk_coe, coe_id]
[GOAL]
X✝ : GroupCat
⊢ ↑Abelianization.lift
      {
        toOneHom :=
          { toFun := fun x => ↑Abelianization.of (↑(𝟙 X✝) x), map_one' := (_ : ↑Abelianization.of (↑(𝟙 X✝) 1) = 1) },
        map_mul' :=
          (_ :
            ∀ (a a_1 : ↑X✝),
              ↑Abelianization.of (↑(𝟙 X✝) (a * a_1)) =
                ↑Abelianization.of (↑(𝟙 X✝) a) * ↑Abelianization.of (↑(𝟙 X✝) a_1)) } =
    𝟙 (Bundled.mk (Abelianization ↑X✝))
[PROOFSTEP]
apply (Equiv.apply_eq_iff_eq_symm_apply Abelianization.lift).mpr
[GOAL]
X✝ : GroupCat
⊢ {
      toOneHom :=
        { toFun := fun x => ↑Abelianization.of (↑(𝟙 X✝) x), map_one' := (_ : ↑Abelianization.of (↑(𝟙 X✝) 1) = 1) },
      map_mul' :=
        (_ :
          ∀ (a a_1 : ↑X✝),
            ↑Abelianization.of (↑(𝟙 X✝) (a * a_1)) =
              ↑Abelianization.of (↑(𝟙 X✝) a) * ↑Abelianization.of (↑(𝟙 X✝) a_1)) } =
    ↑Abelianization.lift.symm (𝟙 (Bundled.mk (Abelianization ↑X✝)))
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {X Y Z : GroupCat} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun G => Bundled.mk (Abelianization ↑G),
            map := fun {X Y} f =>
              ↑Abelianization.lift
                {
                  toOneHom :=
                    { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a a_1 : ↑X),
                        ↑Abelianization.of (↑f (a * a_1)) =
                          ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
        (f ≫ g) =
      { obj := fun G => Bundled.mk (Abelianization ↑G),
              map := fun {X Y} f =>
                ↑Abelianization.lift
                  {
                    toOneHom :=
                      { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (a a_1 : ↑X),
                          ↑Abelianization.of (↑f (a * a_1)) =
                            ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
          f ≫
        { obj := fun G => Bundled.mk (Abelianization ↑G),
              map := fun {X Y} f =>
                ↑Abelianization.lift
                  {
                    toOneHom :=
                      { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (a a_1 : ↑X),
                          ↑Abelianization.of (↑f (a * a_1)) =
                            ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
          g
[PROOFSTEP]
intros
[GOAL]
X✝ Y✝ Z✝ : GroupCat
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun G => Bundled.mk (Abelianization ↑G),
          map := fun {X Y} f =>
            ↑Abelianization.lift
              {
                toOneHom :=
                  { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a a_1 : ↑X),
                      ↑Abelianization.of (↑f (a * a_1)) =
                        ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
      (f✝ ≫ g✝) =
    { obj := fun G => Bundled.mk (Abelianization ↑G),
            map := fun {X Y} f =>
              ↑Abelianization.lift
                {
                  toOneHom :=
                    { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a a_1 : ↑X),
                        ↑Abelianization.of (↑f (a * a_1)) =
                          ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
        f✝ ≫
      { obj := fun G => Bundled.mk (Abelianization ↑G),
            map := fun {X Y} f =>
              ↑Abelianization.lift
                {
                  toOneHom :=
                    { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a a_1 : ↑X),
                        ↑Abelianization.of (↑f (a * a_1)) =
                          ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
        g✝
[PROOFSTEP]
simp only [coe_comp]
[GOAL]
X✝ Y✝ Z✝ : GroupCat
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ ↑Abelianization.lift
      {
        toOneHom :=
          { toFun := fun x => ↑Abelianization.of (↑(f✝ ≫ g✝) x),
            map_one' := (_ : ↑Abelianization.of (↑(f✝ ≫ g✝) 1) = 1) },
        map_mul' :=
          (_ :
            ∀ (a a_1 : ↑X✝),
              ↑Abelianization.of (↑(f✝ ≫ g✝) (a * a_1)) =
                ↑Abelianization.of (↑(f✝ ≫ g✝) a) * ↑Abelianization.of (↑(f✝ ≫ g✝) a_1)) } =
    ↑Abelianization.lift
        {
          toOneHom :=
            { toFun := fun x => ↑Abelianization.of (↑f✝ x), map_one' := (_ : ↑Abelianization.of (↑f✝ 1) = 1) },
          map_mul' :=
            (_ :
              ∀ (a a_1 : ↑X✝),
                ↑Abelianization.of (↑f✝ (a * a_1)) = ↑Abelianization.of (↑f✝ a) * ↑Abelianization.of (↑f✝ a_1)) } ≫
      ↑Abelianization.lift
        {
          toOneHom :=
            { toFun := fun x => ↑Abelianization.of (↑g✝ x), map_one' := (_ : ↑Abelianization.of (↑g✝ 1) = 1) },
          map_mul' :=
            (_ :
              ∀ (a a_1 : ↑Y✝),
                ↑Abelianization.of (↑g✝ (a * a_1)) = ↑Abelianization.of (↑g✝ a) * ↑Abelianization.of (↑g✝ a_1)) }
[PROOFSTEP]
apply (Equiv.apply_eq_iff_eq_symm_apply Abelianization.lift).mpr
[GOAL]
X✝ Y✝ Z✝ : GroupCat
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ {
      toOneHom :=
        { toFun := fun x => ↑Abelianization.of (↑(f✝ ≫ g✝) x),
          map_one' := (_ : ↑Abelianization.of (↑(f✝ ≫ g✝) 1) = 1) },
      map_mul' :=
        (_ :
          ∀ (a a_1 : ↑X✝),
            ↑Abelianization.of (↑(f✝ ≫ g✝) (a * a_1)) =
              ↑Abelianization.of (↑(f✝ ≫ g✝) a) * ↑Abelianization.of (↑(f✝ ≫ g✝) a_1)) } =
    ↑Abelianization.lift.symm
      (↑Abelianization.lift
          {
            toOneHom :=
              { toFun := fun x => ↑Abelianization.of (↑f✝ x), map_one' := (_ : ↑Abelianization.of (↑f✝ 1) = 1) },
            map_mul' :=
              (_ :
                ∀ (a a_1 : ↑X✝),
                  ↑Abelianization.of (↑f✝ (a * a_1)) = ↑Abelianization.of (↑f✝ a) * ↑Abelianization.of (↑f✝ a_1)) } ≫
        ↑Abelianization.lift
          {
            toOneHom :=
              { toFun := fun x => ↑Abelianization.of (↑g✝ x), map_one' := (_ : ↑Abelianization.of (↑g✝ 1) = 1) },
            map_mul' :=
              (_ :
                ∀ (a a_1 : ↑Y✝),
                  ↑Abelianization.of (↑g✝ (a * a_1)) = ↑Abelianization.of (↑g✝ a) * ↑Abelianization.of (↑g✝ a_1)) })
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {X' X : GroupCat} {Y : CommGroupCat} (f : X' ⟶ X) (g : X ⟶ (forget₂ CommGroupCat GroupCat).obj Y),
    ↑((fun G A => Abelianization.lift.symm) X' Y).symm (f ≫ g) =
      abelianize.map f ≫ ↑((fun G A => Abelianization.lift.symm) X Y).symm g
[PROOFSTEP]
intros
[GOAL]
X'✝ X✝ : GroupCat
Y✝ : CommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGroupCat GroupCat).obj Y✝
⊢ ↑((fun G A => Abelianization.lift.symm) X'✝ Y✝).symm (f✝ ≫ g✝) =
    abelianize.map f✝ ≫ ↑((fun G A => Abelianization.lift.symm) X✝ Y✝).symm g✝
[PROOFSTEP]
ext1
[GOAL]
case w
X'✝ X✝ : GroupCat
Y✝ : CommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGroupCat GroupCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ ↑(↑((fun G A => Abelianization.lift.symm) X'✝ Y✝).symm (f✝ ≫ g✝)) x✝ =
    ↑(abelianize.map f✝ ≫ ↑((fun G A => Abelianization.lift.symm) X✝ Y✝).symm g✝) x✝
[PROOFSTEP]
simp only [Equiv.symm_symm]
[GOAL]
case w
X'✝ X✝ : GroupCat
Y✝ : CommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGroupCat GroupCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ ↑(↑Abelianization.lift (f✝ ≫ g✝)) x✝ = ↑(abelianize.map f✝ ≫ ↑Abelianization.lift g✝) x✝
[PROOFSTEP]
apply Eq.symm
[GOAL]
case w.h
X'✝ X✝ : GroupCat
Y✝ : CommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGroupCat GroupCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ ↑(abelianize.map f✝ ≫ ↑Abelianization.lift g✝) x✝ = ↑(↑Abelianization.lift (f✝ ≫ g✝)) x✝
[PROOFSTEP]
apply Abelianization.lift.unique
[GOAL]
case w.h.hφ
X'✝ X✝ : GroupCat
Y✝ : CommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGroupCat GroupCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ ∀ (x : ↑X'✝), ↑(abelianize.map f✝ ≫ ↑Abelianization.lift g✝) (↑Abelianization.of x) = ↑(f✝ ≫ g✝) x
[PROOFSTEP]
intros
[GOAL]
case w.h.hφ
X'✝ X✝ : GroupCat
Y✝ : CommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGroupCat GroupCat).obj Y✝
x✝¹ : ↑(abelianize.obj X'✝)
x✝ : ↑X'✝
⊢ ↑(abelianize.map f✝ ≫ ↑Abelianization.lift g✝) (↑Abelianization.of x✝) = ↑(f✝ ≫ g✝) x✝
[PROOFSTEP]
apply Abelianization.lift.of
[GOAL]
⊢ ∀ ⦃X Y : MonCat⦄ (f : X ⟶ Y),
    (MonCat.units ⋙ forget₂ GroupCat MonCat).map f ≫ (fun X => Units.coeHom ↑X) Y =
      (fun X => Units.coeHom ↑X) X ≫ (𝟭 MonCat).map f
[PROOFSTEP]
intros
[GOAL]
X✝ Y✝ : MonCat
f✝ : X✝ ⟶ Y✝
⊢ (MonCat.units ⋙ forget₂ GroupCat MonCat).map f✝ ≫ (fun X => Units.coeHom ↑X) Y✝ =
    (fun X => Units.coeHom ↑X) X✝ ≫ (𝟭 MonCat).map f✝
[PROOFSTEP]
exact MonoidHom.ext fun x => rfl
[GOAL]
⊢ ∀ ⦃X Y : CommMonCat⦄ (f : X ⟶ Y),
    (CommMonCat.units ⋙ forget₂ CommGroupCat CommMonCat).map f ≫ (fun X => Units.coeHom ↑X) Y =
      (fun X => Units.coeHom ↑X) X ≫ (𝟭 CommMonCat).map f
[PROOFSTEP]
intros
[GOAL]
X✝ Y✝ : CommMonCat
f✝ : X✝ ⟶ Y✝
⊢ (CommMonCat.units ⋙ forget₂ CommGroupCat CommMonCat).map f✝ ≫ (fun X => Units.coeHom ↑X) Y✝ =
    (fun X => Units.coeHom ↑X) X✝ ≫ (𝟭 CommMonCat).map f✝
[PROOFSTEP]
exact MonoidHom.ext fun x => rfl
