Theorem: equiv_if_odds (meetings/ex4.lean)

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

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

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

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

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

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

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

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