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

State before:
n : Nat
⊢ 2 ∣ n ↔ Even n
Tactic:
unfold Even
State after:
n : Nat
⊢ 2 ∣ n ↔ ∃ r, n = r + r

State before:
n : Nat
⊢ 2 ∣ n ↔ ∃ r, n = r + r
Tactic:
simp only [← Nat.two_mul]
State after:
n : Nat
⊢ 2 ∣ n ↔ ∃ r, n = 2 * r

State before:
n : Nat
⊢ 2 ∣ n ↔ ∃ r, n = 2 * r
Tactic:
constructor
State after:
case mp
n : Nat
⊢ 2 ∣ n → ∃ r, n = 2 * r

case mpr
n : Nat
⊢ (∃ r, n = 2 * r) → 2 ∣ n

State before:
case mp
n : Nat
⊢ 2 ∣ n → ∃ r, n = 2 * r

case mpr
n : Nat
⊢ (∃ r, n = 2 * r) → 2 ∣ n
Tactic:
all_goals
  intro heven
  rcases heven with ⟨i, hi⟩
  exists i
State after:
no goals

State before:
case mpr
n : Nat
⊢ (∃ r, n = 2 * r) → 2 ∣ n
Tactic:
intro heven
State after:
case mpr
n : Nat
heven : ∃ r, n = 2 * r
⊢ 2 ∣ n

State before:
case mpr
n : Nat
heven : ∃ r, n = 2 * r
⊢ 2 ∣ n
Tactic:
rcases heven with ⟨i, hi⟩
State after:
case mpr.intro
n i : Nat
hi : n = 2 * i
⊢ 2 ∣ n

State before:
case mpr.intro
n i : Nat
hi : n = 2 * i
⊢ 2 ∣ n
Tactic:
exists i
State after:
no goals