Theorem: nequiv_if_diff_parity (meetings/ex4.lean)

State before:
x y : ℤ
⊢ Odd x → Even y → ¬equiv_rel x y
Tactic:
intros ex ey equiv
State after:
x y : ℤ
ex : Odd x
ey : Even y
equiv : equiv_rel x y
⊢ False

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

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

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

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

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

State before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : (2 * a + 1) ^ 2 + (b + b) ^ 2 = e + e
⊢ False
Tactic:
ring_nf at he
State after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = e * 2
⊢ False

State before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = e * 2
⊢ False
Tactic:
symm at he
State after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : e * 2 = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ False

State before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : e * 2 = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ False
Tactic:
rw [mul_comm] at he
State after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ False

State before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ False
Tactic:
have two_dvd := dvd_of_mul_right_eq e he
State after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ False

State before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ False
Tactic:
have hring :
  1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
  = 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1 := by
  ring_nf
State after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
hring : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
⊢ False

State before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
hring : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
⊢ False
Tactic:
rw [hring] at two_dvd
State after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
hring : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
⊢ False

State before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
hring : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
⊢ False
Tactic:
exact Int.two_not_dvd_two_mul_add_one _ two_dvd
State after:
no goals

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