Theorem: even_of_even_sqr (MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean)

State before:
m : ℕ
h : 2 ∣ m ^ 2
⊢ 2 ∣ m
Tactic:
rw [pow_two, Nat.prime_two.dvd_mul] at h
State after:
m : ℕ
h : 2 ∣ m ∨ 2 ∣ m
⊢ 2 ∣ m

State before:
m : ℕ
h : 2 ∣ m ∨ 2 ∣ m
⊢ 2 ∣ m
Tactic:
cases h <;> assumption
State after:
no goals