Theorem: Nat.xor_mod2₀₁ (Lib.lean)

State before:
n m : ℕ
⊢ Bool.xor (decide (n % 2 = 0)) (decide (m % 2 = 1)) = decide ((n + m) % 2 = 0)
Tactic:
cases m using binaryRec with
| z => simp
| f b _ _ =>
  cases n using binaryRec with
  | z => cases b <;> simp [← Nat.two_mul]
  | f c _ _ =>
    cases b <;> cases c <;> simp [← Nat.two_mul, Nat.mul_add_mod, ← Nat.add_assoc]
State after:
no goals

State before:
case z
n : ℕ
⊢ Bool.xor (decide (n % 2 = 0)) (decide (0 % 2 = 1)) = decide ((n + 0) % 2 = 0)
Tactic:
simp
State after:
no goals

State before:
case f
n : ℕ
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → Bool.xor (decide (n % 2 = 0)) (decide (bit b n✝ % 2 = 1)) = decide ((n + bit b n✝) % 2 = 0)
⊢ Bool.xor (decide (n % 2 = 0)) (decide (bit b n✝ % 2 = 1)) = decide ((n + bit b n✝) % 2 = 0)
Tactic:
cases n using binaryRec with
| z => cases b <;> simp [← Nat.two_mul]
| f c _ _ =>
  cases b <;> cases c <;> simp [← Nat.two_mul, Nat.mul_add_mod, ← Nat.add_assoc]
State after:
no goals

State before:
case f.z
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → Bool.xor (decide (0 % 2 = 0)) (decide (bit b n✝ % 2 = 1)) = decide ((0 + bit b n✝) % 2 = 0)
⊢ Bool.xor (decide (0 % 2 = 0)) (decide (bit b n✝ % 2 = 1)) = decide ((0 + bit b n✝) % 2 = 0)
Tactic:
cases b <;> simp [← Nat.two_mul]
State after:
no goals

State before:
case f.f
b : Bool
n✝¹ : ℕ
c : Bool
n✝ : ℕ
a✝¹ :
  bit b n✝¹ = n✝¹ →
    Bool.xor (decide (bit c n✝ % 2 = 0)) (decide (bit b n✝¹ % 2 = 1)) = decide ((bit c n✝ + bit b n✝¹) % 2 = 0)
a✝ :
  bit c n✝ = n✝ →
    Bool.xor (decide (bit c n✝ % 2 = 0)) (decide (bit b n✝¹ % 2 = 1)) = decide ((bit c n✝ + bit b n✝¹) % 2 = 0)
⊢ Bool.xor (decide (bit c n✝ % 2 = 0)) (decide (bit b n✝¹ % 2 = 1)) = decide ((bit c n✝ + bit b n✝¹) % 2 = 0)
Tactic:
cases b <;> cases c <;> simp [← Nat.two_mul, Nat.mul_add_mod, ← Nat.add_assoc]
State after:
no goals