∀ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst_1 : Group β] (x : WithZero α ≃* WithZero β),
  (fun e =>
        { toFun := ⇑(WithZero.map' ↑e), invFun := ⇑(WithZero.map' ↑e.symm), left_inv := ⋯, right_inv := ⋯,
          map_mul' := ⋯ })
      ((fun e =>
          { toFun := fun x => WithZero.unzero ⋯, invFun := fun x => WithZero.unzero ⋯, left_inv := ⋯, right_inv := ⋯,
            map_mul' := ⋯ })
        x) =
    x