rcases ... with

Stream: new members

[Moti Ben-Ari]

Here is an expanded version of even_of_even_sqr from MiL 5.1

import Mathlib.Data.Nat.Prime
open Nat
example : 2 ∣ m ^ 2 →  2 ∣ m := by
  intro h
  rw [pow_two] at h
  rw [prime_two.dvd_mul] at h
  rcases h
  · assumption
  · assumption
  done

I would like to get it to work with the construct cases ... with like in

example : x < |y| → x < y ∨ x < -y := by
rcases le_or_gt 0 y with h | h

but whatever I put after rcases results in the error rcases tactic failed: x✝ : Prop is not an inductive datatype

example : 2 ∣ m ^ 2 →  2 ∣ m := by
  intro h
  rw [pow_two] at h
  rw [prime_two.dvd_mul] at h
  rcases Even m with h₁ | h₁

or

rcases 2 ∣ m with h₁ | h₁

Please explain the error and how to use rcases ... with

[Kevin Buzzard]

rcases h with h₁ | h₁