`casesm` changed behaviour, does not deconstruct inductive types

[LukasMias]

In lean 3:

inductive two_points
  | zero
  | one

namespace two_points
theorem mwe : ∀ (x : two_points), x = zero ∨ x = one := λ x, by casesm _; simp -- works
end two_points

In lean 4:

import Mathlib.Tactic.CasesM

inductive twoPoints
  | zero
  | one

namespace twoPoints
theorem mwe : ∀ (x : twoPoints), x = zero ∨ x = one := fun x ↦ by casesm _ <;> simp -- no match
end twoPoints

Not sure if this was intended behavior, but it was definitely used in mathlib3, e.g. data.sign, so some proofs break now. Related Zulip thread: here.

[kmill]

I'm not sure whether casesm _ is supposed to work or not, but at least there's a workaround here, if you know the name of the type:

theorem mwe : ∀ (x : twoPoints), x = zero ∨ x = one := fun x ↦ by cases_type twoPoints <;> simp