Theorem: Nat.eq_mod2_of_decide (Algdata/Data/Nat/Bits.lean)

State before:
m n : Nat
⊢ decide (m % 2 = 1) = decide (n % 2 = 1) → m % 2 = n % 2
Tactic:
cases m.mod_two_eq_zero_or_one <;> cases n.mod_two_eq_zero_or_one
<;> rw [‹m%2=_›, ‹n%2=_›] <;> intro hdec <;> cases hdec <;> rfl
State after:
no goals