. simp (config := { decide := true}) only [h]
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
case inr
n : Nat
h : n % 2 = 1
⊢ ¬n % 2 = 0 ↔ n % 2 = 1