∀ (X : AddCommMonCat),
  CategoryTheory.CategoryStruct.comp
      ({ obj := fun X => CommMonCat.of (Multiplicative ↑X),
            map := fun {X Y} f => CommMonCat.ofHom (AddMonoidHom.toMultiplicative (AddCommMonCat.Hom.hom f)),
            map_id := AddCommMonCat.equivalence._proof_1, map_comp := @AddCommMonCat.equivalence._proof_2 }.map
        ((CategoryTheory.Iso.refl (CategoryTheory.Functor.id AddCommMonCat)).hom.app X))
      ((CategoryTheory.Iso.refl
              ({ obj := fun X => AddCommMonCat.of (Additive ↑X),
                    map := fun {X Y} f => AddCommMonCat.ofHom (MonoidHom.toAdditive (CommMonCat.Hom.hom f)),
                    map_id := AddCommMonCat.equivalence._proof_3, map_comp := @AddCommMonCat.equivalence._proof_4 }.comp
                { obj := fun X => CommMonCat.of (Multiplicative ↑X),
                  map := fun {X Y} f => CommMonCat.ofHom (AddMonoidHom.toMultiplicative (AddCommMonCat.Hom.hom f)),
                  map_id := AddCommMonCat.equivalence._proof_1,
                  map_comp := @AddCommMonCat.equivalence._proof_2 })).hom.app
        ({ obj := fun X => CommMonCat.of (Multiplicative ↑X),
              map := fun {X Y} f => CommMonCat.ofHom (AddMonoidHom.toMultiplicative (AddCommMonCat.Hom.hom f)),
              map_id := AddCommMonCat.equivalence._proof_1, map_comp := @AddCommMonCat.equivalence._proof_2 }.obj
          X)) =
    CategoryTheory.CategoryStruct.id
      ({ obj := fun X => CommMonCat.of (Multiplicative ↑X),
            map := fun {X Y} f => CommMonCat.ofHom (AddMonoidHom.toMultiplicative (AddCommMonCat.Hom.hom f)),
            map_id := AddCommMonCat.equivalence._proof_1, map_comp := @AddCommMonCat.equivalence._proof_2 }.obj
        X)