`cases` and `induction` don't respect `Multiplicative`

Trying to add a recursor for WithZero (Multiplicative M), I discovered that my recursor was actually firing on WithZero M because Multiplicative is too reducible for induction.

import Mathlib

open scoped WithZero

variable {M : Type*}

@[induction_eliminator, cases_eliminator]
def expRecOn {motive : Mᵐ⁰ → Sort*} (x : Mᵐ⁰) (zero : motive 0) (exp : ∀ a, motive (.exp a)) :
    motive x := Option.recOn x zero exp

example (a : WithZero M) : a = a := by
  induction a with
  | zero => rfl
  -- This should be `coe` instead.
  | exp => rfl

example (a : WithZero M) : a = a := by
  cases a with
  | zero => rfl
  -- This should be `coe` instead.
  | exp => rfl

It is not clear to me whether this is intended on the part of cases and induction. If so, that means we need to make Multiplicative into a one-field structure, which looks like a big undertaking...

Start by reproducing the two examples with Mathlib, focusing on the expRecOn eliminator and how cases and induction handle WithZero (Multiplicative M). Read the behavior around Multiplicative, WithZero, and the cases/induction entry points; done means the examples select the expected constructor behavior or the intended limitation is documented.