Theorem: Nat.even_add (Smt/Reconstruct/Int/Lemmas.lean)

State before:
m n : Nat
⊢ (m + n) % 2 = 0 ↔ (m % 2 = 0 ↔ n % 2 = 0)
Tactic:
cases Nat.mod_two_eq_zero_or_one m <;> rename_i h₁ <;> cases Nat.mod_two_eq_zero_or_one n <;> rename_i h₂ <;>
  simp [h₁, h₂, Nat.add_mod]
State after:
no goals