∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N)
  (hf : ∀ (x y : M), Commute (f x) (f y)),
  f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_one' := ⋯, map_mul' := ⋯ }