R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
⊢ multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
⊢ multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
have hx_odd : Odd x := by rwa [Int.odd_iff_not_even, even_iff_two_dvd]
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
⊢ multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by norm_num) hxy)
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
have hy_odd : Odd y := by simpa using hx_odd.sub_even hxy_even
case refine'_1
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ 2 ^ 1 ∣ x ^ 2 ^ i + y ^ 2 ^ i

case refine'_2
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ i + y ^ 2 ^ i
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
refine' multiplicity.eq_coe_iff.mpr ⟨_, _⟩
case refine'_2.zero
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero

case refine'_2.succ
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.succ i + y ^ 2 ^ Nat.succ i
case refine'_2
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ i + y ^ 2 ^ i
cases' i with i
case refine'_2.succ
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
⊢ ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
case refine'_2.succ
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.succ i + y ^ 2 ^ Nat.succ i
suffices ∀ x : ℤ, Odd x → x ^ 2 ^ (i + 1) % 4 = 1 by
  rw [show (2 ^ (1 + 1) : ℤ) = 4 by norm_num, Int.dvd_iff_emod_eq_zero, Int.add_emod,
    this _ hx_odd, this _ hy_odd]
  norm_num
case refine'_2.succ
R : Type ?u.851761
n : ℕ
x✝ y : ℤ
hx✝ : ¬2 ∣ x✝
hxy : 4 ∣ x✝ - y
hx_odd : Odd x✝
hxy_even : Even (x✝ - y)
hy_odd : Odd y
i : ℕ
x : ℤ
hx : Odd x
⊢ x ^ 2 ^ (i + 1) % 4 = 1
case refine'_2.succ
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
⊢ ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
intro x hx
no goals
case refine'_2.succ
R : Type ?u.851761
n : ℕ
x✝ y : ℤ
hx✝ : ¬2 ∣ x✝
hxy : 4 ∣ x✝ - y
hx_odd : Odd x✝
hxy_even : Even (x✝ - y)
hy_odd : Odd y
i : ℕ
x : ℤ
hx : Odd x
⊢ x ^ 2 ^ (i + 1) % 4 = 1
rw [pow_succ, mul_comm, pow_mul, Int.sq_mod_four_eq_one_of_odd hx.pow]
no goals
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
⊢ Odd x
rwa [Int.odd_iff_not_even, even_iff_two_dvd]
no goals
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
⊢ 2 ∣ 4
norm_num
no goals
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ Odd y
simpa using hx_odd.sub_even hxy_even
case refine'_1
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ Even (x ^ 2 ^ i + y ^ 2 ^ i)
case refine'_1
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ 2 ^ 1 ∣ x ^ 2 ^ i + y ^ 2 ^ i
rw [pow_one, ← even_iff_two_dvd]
no goals
case refine'_1
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ Even (x ^ 2 ^ i + y ^ 2 ^ i)
exact hx_odd.pow.add_odd hy_odd.pow
case refine'_2.zero
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hxy' : 2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero
⊢ False
case refine'_2.zero
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero
intro hxy'
case refine'_2.zero
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hxy' : 2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero
this : 2 * 2 ∣ 2 * x
⊢ False
case refine'_2.zero
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hxy' : 2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero
⊢ False
have : 2 * 2 ∣ 2 * x := by
  have := dvd_add hxy hxy'
  norm_num at *
  rw [two_mul]
  exact this
case refine'_2.zero
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hxy' : 2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero
this✝ : 2 * 2 ∣ 2 * x
this : 2 ∣ x
⊢ False
case refine'_2.zero
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hxy' : 2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero
this : 2 * 2 ∣ 2 * x
⊢ False
have : 2 ∣ x := (mul_dvd_mul_iff_left (by norm_num)).mp this
no goals
case refine'_2.zero
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hxy' : 2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero
this✝ : 2 * 2 ∣ 2 * x
this : 2 ∣ x
⊢ False
contradiction
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hxy' : 2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero
this : 4 ∣ x - y + (x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero)
⊢ 2 * 2 ∣ 2 * x
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hxy' : 2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero
⊢ 2 * 2 ∣ 2 * x
have := dvd_add hxy hxy'
R : Type ?u.851761
n : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hxy_even : Even (x - y)
hx : x % 2 = 1
hx_odd : ¬Even x
hy_odd : ¬Even y
hxy' : 4 ∣ x + y
this : 4 ∣ x + x
⊢ 4 ∣ 2 * x
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hxy' : 2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero
this : 4 ∣ x - y + (x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero)
⊢ 2 * 2 ∣ 2 * x
norm_num at *
R : Type ?u.851761
n : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hxy_even : Even (x - y)
hx : x % 2 = 1
hx_odd : ¬Even x
hy_odd : ¬Even y
hxy' : 4 ∣ x + y
this : 4 ∣ x + x
⊢ 4 ∣ x + x
R : Type ?u.851761
n : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hxy_even : Even (x - y)
hx : x % 2 = 1
hx_odd : ¬Even x
hy_odd : ¬Even y
hxy' : 4 ∣ x + y
this : 4 ∣ x + x
⊢ 4 ∣ 2 * x
rw [two_mul]
no goals
R : Type ?u.851761
n : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hxy_even : Even (x - y)
hx : x % 2 = 1
hx_odd : ¬Even x
hy_odd : ¬Even y
hxy' : 4 ∣ x + y
this : 4 ∣ x + x
⊢ 4 ∣ x + x
exact this
no goals
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hxy' : 2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.zero + y ^ 2 ^ Nat.zero
this : 2 * 2 ∣ 2 * x
⊢ 2 ≠ 0
norm_num
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ ¬(1 + 1) % 4 = 0
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ Nat.succ i + y ^ 2 ^ Nat.succ i
rw [show (2 ^ (1 + 1) : ℤ) = 4 by norm_num, Int.dvd_iff_emod_eq_zero, Int.add_emod,
  this _ hx_odd, this _ hy_odd]
no goals
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ ¬(1 + 1) % 4 = 0
norm_num
no goals
R : Type ?u.851761
n : ℕ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ 2 ^ (1 + 1) = 4
norm_num