-- Mathlib/NumberTheory/Multiplicity.lean
theorem Int.two_pow_two_pow_add_two_pow_two_pow {x y : ℤ} (hx : ¬2 ∣ x) (hxy : 4 ∣ x - y) (i : ℕ) :
    emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑(1 : ℕ)

Proof state:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
⊢ Odd x

Tactic:
rwa [← Int.not_even_iff_odd, even_iff_two_dvd]

Result:
no goals

Proof state:
case refine_1
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)

Tactic:
exact hx_odd.pow.add_odd hy_odd.pow

Result:
no goals

Proof state:
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

Tactic:
decide

Result:
no goals

Proof state:
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 ^ 0 + y ^ 2 ^ 0
this : 2 * 2 ∣ 2 * x
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
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

Tactic:
norm_num

Result:
no goals

Proof state:
x y : ℤ
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hx : x % 2 = 1
hxy' : 4 ∣ x + y
this : 4 ∣ x + x
⊢ 4 ∣ 2 * x

Tactic:
rw [two_mul]

Result:
x y : ℤ
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hx : x % 2 = 1
hxy' : 4 ∣ x + y
this : 4 ∣ x + x
⊢ 4 ∣ x + x

Proof state:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1

Tactic:
have hy_odd : Odd y := by simpa using hx_odd.sub_even hxy_even

Result:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1

Proof state:
x y : ℤ
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
hx : x % 2 = 1
hxy' : 4 ∣ x + y
this : 4 ∣ x + x
⊢ 4 ∣ x + x

Tactic:
exact this

Result:
no goals

Proof state:
case refine_1
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

Tactic:
rw [pow_one, ← even_iff_two_dvd]

Result:
case refine_1
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)

Proof state:
case refine_2.zero
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 ^ 0 + y ^ 2 ^ 0
⊢ False

Tactic:
have : 2 * 2 ∣ 2 * x := by
  have := dvd_add hxy hxy'
  norm_num at *
  rw [two_mul]
  exact this

Result:
case refine_2.zero
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 ^ 0 + y ^ 2 ^ 0
this : 2 * 2 ∣ 2 * x
⊢ False

Proof state:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
⊢ emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1

Tactic:
have hx_odd : Odd x := by rwa [← Int.not_even_iff_odd, even_iff_two_dvd]

Result:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
⊢ emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1

Proof state:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ Odd y

Tactic:
simpa using hx_odd.sub_even hxy_even

Result:
no goals

Proof state:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
⊢ 2 ∣ 4

Tactic:
decide

Result:
no goals

Proof state:
case refine_2.succ
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

Tactic:
rw [pow_succ', mul_comm, pow_mul, Int.sq_mod_four_eq_one_of_odd hx.pow]

Result:
no goals

Proof state:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
⊢ emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1

Tactic:
have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by decide) hxy)

Result:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1

Proof state:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1

Tactic:
refine emultiplicity_eq_coe.mpr ⟨?_, ?_⟩

Result:
case refine_1
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
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

Proof state:
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 ^ (i + 1) + y ^ 2 ^ (i + 1)

Tactic:
rw [show (2 ^ (1 + 1) : ℤ) = 4 by norm_num, Int.dvd_iff_emod_eq_zero, Int.add_emod,
  this _ hx_odd, this _ hy_odd]

Result:
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

Proof state:
case refine_2.zero
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 ^ 0 + y ^ 2 ^ 0
this : 2 * 2 ∣ 2 * x
⊢ False

Tactic:
have : 2 ∣ x := (mul_dvd_mul_iff_left (by norm_num)).mp this

Result:
case refine_2.zero
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 ^ 0 + y ^ 2 ^ 0
this✝ : 2 * 2 ∣ 2 * x
this : 2 ∣ x
⊢ False

Proof state:
case refine_2
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

Tactic:
rcases i with - | i

Result:
case refine_2.zero
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 ^ 0 + y ^ 2 ^ 0

case refine_2.succ
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 ^ (i + 1) + y ^ 2 ^ (i + 1)

Proof state:
case refine_2.zero
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 ^ 0 + y ^ 2 ^ 0

Tactic:
intro hxy'

Result:
case refine_2.zero
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 ^ 0 + y ^ 2 ^ 0
⊢ False

Proof state:
case refine_2.succ
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

Tactic:
intro x hx

Result:
case refine_2.succ
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

Proof state:
case refine_2.zero
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 ^ 0 + y ^ 2 ^ 0
this✝ : 2 * 2 ∣ 2 * x
this : 2 ∣ x
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
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 ^ 0 + y ^ 2 ^ 0
⊢ 2 * 2 ∣ 2 * x

Tactic:
have := dvd_add hxy hxy'

Result:
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 ^ 0 + y ^ 2 ^ 0
this : 4 ∣ x - y + (x ^ 2 ^ 0 + y ^ 2 ^ 0)
⊢ 2 * 2 ∣ 2 * x

Proof state:
case refine_2.succ
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 ^ (i + 1) + y ^ 2 ^ (i + 1)

Tactic:
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]
  decide

Result:
case refine_2.succ
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