Theorem: Misc.Nat.mod_two_ne_zero (LeanSAT/Util/Misc.lean)

State before:
n : Nat
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
rcases Nat.mod_two_eq_zero_or_one n with h | h
State after:
case inl
n : Nat
h : n % 2 = 0
⊢ ¬n % 2 = 0 ↔ n % 2 = 1

case inr
n : Nat
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1

State before:
case inl
n : Nat
h : n % 2 = 0
⊢ ¬n % 2 = 0 ↔ n % 2 = 1

case inr
n : Nat
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
. simp (config := { decide := true}) only [h]
State after:
case inr
n : Nat
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1

State before:
case inr
n : Nat
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
. simp (config := { decide := true}) only [h]
State after:
no goals

State before:
case inl
n : Nat
h : n % 2 = 0
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
simp (config := { decide := true}) only [h]
State after:
no goals

State before:
case inr
n : Nat
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
simp (config := { decide := true}) only [h]
State after:
no goals