Theorem: equiv_if_evens (meetings/ex4.lean)

State before:
x y : ℤ
⊢ Even x → Even y → equiv_rel x y
Tactic:
intros ex ey
State after:
x y : ℤ
ex : Even x
ey : Even y
⊢ equiv_rel x y

State before:
x y : ℤ
ex : Even x
ey : Even y
⊢ equiv_rel x y
Tactic:
simp [equiv_rel, Even] at *
State after:
x y : ℤ
ex : ∃ r, x = r + r
ey : ∃ r, y = r + r
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r

State before:
x y : ℤ
ex : ∃ r, x = r + r
ey : ∃ r, y = r + r
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Tactic:
rcases ex with ⟨a, ha⟩
State after:
case intro
x y : ℤ
ey : ∃ r, y = r + r
a : ℤ
ha : x = a + a
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r

State before:
case intro
x y : ℤ
ey : ∃ r, y = r + r
a : ℤ
ha : x = a + a
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Tactic:
rcases ey with ⟨b, hb⟩
State after:
case intro.intro
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r

State before:
case intro.intro
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Tactic:
rw [ha, hb]
State after:
case intro.intro
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ ∃ r, (a + a) ^ 2 + (b + b) ^ 2 = r + r

State before:
case intro.intro
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ ∃ r, (a + a) ^ 2 + (b + b) ^ 2 = r + r
Tactic:
use (2 * a ^ 2 + 2 * b ^ 2)
State after:
case h
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ (a + a) ^ 2 + (b + b) ^ 2 = 2 * a ^ 2 + 2 * b ^ 2 + (2 * a ^ 2 + 2 * b ^ 2)

State before:
case h
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ (a + a) ^ 2 + (b + b) ^ 2 = 2 * a ^ 2 + 2 * b ^ 2 + (2 * a ^ 2 + 2 * b ^ 2)
Tactic:
ring_nf
State after:
no goals