∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : MulOneClass β],
  WithOne.lift =
    { toFun := fun f => { toFun := fun x => Option.casesOn x 1 ⇑f, map_one' := ⋯, map_mul' := ⋯ },
      invFun := fun F => (↑F).comp WithOne.coeMulHom, left_inv := ⋯, right_inv := ⋯ }