awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
rwa : ¬Even x
rwa₁ rwa₂ rwa₃ rwa₄ : ¬2 ∣ x
⊢ Odd x

Tactic:
rwa [← Int.not_even_iff_odd, even_iff_two_dvd]

Premises used: Int.not_even_iff_odd, even_iff_two_dvd
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
⊢ Odd x

Tactic:
have hx_odd : Odd x := by rwa [← Int.not_even_iff_odd, even_iff_two_dvd]
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
⊢ Dvd.dvd (α := ℤ) 2 4

Tactic:
decide
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
⊢ Even (x - y)

Tactic:
have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by decide) hxy)
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
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

Premises used: Odd.sub_even
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ Odd y

Tactic:
have hy_odd : Odd y := by simpa using hx_odd.sub_even hxy_even
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
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 ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i) = (↑1 : ℕ∞)

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

Premises used: Iff.mpr, And.intro, emultiplicity_eq_coe
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
refine_1 : HPow.hPow (α := ℤ) (β := ℕ) 2 1 ∣ x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i
refine_2 : ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣ x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i
⊢ emultiplicity 2 (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i) = (↑1 : ℕ∞)

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

Premises used: Iff.mpr, And.intro, emultiplicity_eq_coe
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
refine_1 : Even (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)
⊢ HPow.hPow (α := ℤ) (β := ℕ) 2 1 ∣ x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i

Tactic:
rw [pow_one, ← even_iff_two_dvd]

Premises used: pow_one, even_iff_two_dvd
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
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 ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)

Tactic:
hx_odd.pow.add_odd hy_odd.pow

Premises used: Odd.add_odd, Odd.pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
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 ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)

Tactic:
exact hx_odd.pow.add_odd hy_odd.pow

Premises used: Odd.add_odd, Odd.pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
refine_2 :
  ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣
      x ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0 + y ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0
refine_2₁ :
  ∀ (i : ℕ),
    ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣ x ^ HPow.hPow (α := ℕ) 2 (i + 1) + y ^ HPow.hPow (α := ℕ) 2 (i + 1)
⊢ ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣ x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i

Tactic:
rcases i with - | i
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣
      x ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0 + y ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
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 ^ HPow.hPow (α := ℕ) 2 (i + 1) % 4 = 1
⊢ HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) = 4

Tactic:
simp
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
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 ^ HPow.hPow (α := ℕ) 2 (i + 1) % 4 = 1
rw : ¬HAdd.hAdd (α := ℤ) 1 1 % 4 = 0
⊢ ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣ x ^ HPow.hPow (α := ℕ) 2 (i + 1) + y ^ HPow.hPow (α := ℕ) 2 (i + 1)

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

Premises used: Int.add_emod, Int.dvd_iff_emod_eq_zero
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
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 ^ HPow.hPow (α := ℕ) 2 (i + 1) % 4 = 1
⊢ ¬HAdd.hAdd (α := ℤ) 1 1 % 4 = 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
refine_2 : ∀ (x : ℤ), Odd x → x ^ HPow.hPow (α := ℕ) 2 (i + 1) % 4 = 1
⊢ ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣ x ^ HPow.hPow (α := ℕ) 2 (i + 1) + y ^ HPow.hPow (α := ℕ) 2 (i + 1)

Tactic:
suffices ∀ x : ℤ, Odd x → x ^ 2 ^ (i + 1) % 4 = 1 by
    rw [show (2 ^ (1 + 1) : ℤ) = 4 by simp, Int.dvd_iff_emod_eq_zero, Int.add_emod,
      this _ hx_odd, this _ hy_odd]
    decide
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x_1 y : ℤ
hx_1 : ¬2 ∣ x_1
hxy : 4 ∣ x_1 - y
hx_odd : Odd x_1
hxy_even : Even (x_1 - y)
hy_odd : Odd y
i : ℕ
x : ℤ
hx : Odd x
refine_2 : x ^ (2 * HPow.hPow (α := ℕ) 2 i) % 4 = 1
refine_2₁ : x ^ (HPow.hPow (α := ℕ) 2 i * 2) % 4 = 1
refine_2₂ : HPow.hPow (β := ℕ) (x ^ HPow.hPow (α := ℕ) 2 i) 2 % 4 = 1
refine_2₃ refine_2₄ : Eq (α := ℤ) 1 1
⊢ x ^ HPow.hPow (α := ℕ) 2 (i + 1) % 4 = 1

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

Premises used: pow_mul, Odd.pow, mul_comm, Int.sq_mod_four_eq_one_of_odd, pow_succ'
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ emultiplicity 2 (x ^ HPow.hPow (α := ℕ) 2 n - y ^ HPow.hPow (α := ℕ) 2 n) = emultiplicity 2 (x - y) + (↑n : ℕ∞)

Tactic:
simp only [pow_two_pow_sub_pow_two_pow n, emultiplicity_mul Int.prime_two,
    Finset.emultiplicity_prod Int.prime_two, add_comm, Nat.cast_one, Finset.sum_const,
    Finset.card_range, nsmul_one, Int.two_pow_two_pow_add_two_pow_two_pow hx hxy]

Premises used: Finset.emultiplicity_prod, Int.prime_two, Finset.card_range, Int.two_pow_two_pow_add_two_pow_two_pow, add_comm, nsmul_one, Nat.cast_one, pow_two_pow_sub_pow_two_pow, emultiplicity_mul, Finset.sum_const
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
rwa : ¬Even x
rwa₁ rwa₂ rwa₃ rwa₄ : ¬2 ∣ x
⊢ Odd x

Tactic:
rwa [← Int.not_even_iff_odd, even_iff_two_dvd]

Premises used: Int.not_even_iff_odd, even_iff_two_dvd
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ Odd x

Tactic:
have hx_odd : Odd x := by rwa [← Int.not_even_iff_odd, even_iff_two_dvd]
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
⊢ Dvd.dvd (α := ℤ) 2 4

Tactic:
decide
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
⊢ Even (x - y)

Tactic:
have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by decide) hxy)
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ Odd y

Tactic:
simpa using hx_odd.sub_even hxy_even

Premises used: Odd.sub_even
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ Odd y

Tactic:
have hy_odd : Odd y := by simpa using hx_odd.sub_even hxy_even
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
zero :
  emultiplicity 2 (HPow.hPow (β := ℕ) x 0 - HPow.hPow (β := ℕ) y 0) =
    emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑0 : ℤ)
succ :
  ∀ (n : ℕ),
    emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
⊢ emultiplicity 2 (x ^ n - y ^ n) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑n : ℤ)

Tactic:
rcases n with - | n
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ emultiplicity 2 (HPow.hPow (β := ℕ) x 0 - HPow.hPow (β := ℕ) y 0) =
    emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑0 : ℤ)

Tactic:
simp only [pow_zero, sub_self, emultiplicity_zero, Int.ofNat_zero, add_top]

Premises used: add_top, sub_self, emultiplicity_zero, pow_zero, Int.ofNat_zero
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
⊢ Ne (α := ℕ) 2 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
⊢ FiniteMultiplicity 2 n.succ

Tactic:
have h : FiniteMultiplicity 2 n.succ := Nat.finiteMultiplicity_iff.mpr ⟨by simp, n.succ_pos⟩
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
succ :
  ∀ (hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1) (k : ℕ)
    (hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k),
    emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)

Tactic:
rcases emultiplicity_eq_coe.mp h.emultiplicity_eq_multiplicity with ⟨⟨k, hk⟩, hpn⟩

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Iff.mp, emultiplicity_eq_coe
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
succ :
  emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) =
    emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
succ₁ : Prime (M := ℤ) 2
succ₂ : 2 ∣ x ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) - y ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1))
succ₃ : ¬2 ∣ x ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1))
succ₄ : ¬Dvd.dvd (α := ℤ) 2 (↑k : ℤ)
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)

Tactic:
rw [hk, pow_mul, pow_mul, emultiplicity_pow_sub_pow_of_prime,
    Int.two_pow_two_pow_sub_pow_two_pow _ hxy hx, ← hk]

Premises used: emultiplicity_pow_sub_pow_of_prime, pow_mul, Int.two_pow_two_pow_sub_pow_two_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
succ : emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) = emultiplicity 2 (x - y) + emultiplicity 2 (n + 1)
⊢ emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) =
    emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
succ succ₁ :
  emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) =
    emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞)
⊢ emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) = emultiplicity 2 (x - y) + emultiplicity 2 (n + 1)

Tactic:
rw [h.emultiplicity_eq_multiplicity]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
⊢ Prime (M := ℤ) 2

Tactic:
Int.prime_two

Premises used: Int.prime_two
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
⊢ Prime (M := ℤ) 2

Tactic:
exact Int.prime_two

Premises used: Int.prime_two
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
⊢ 2 ∣ x ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) - y ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1))

Tactic:
simpa only [even_iff_two_dvd] using hx_odd.pow.sub_odd hy_odd.pow

Premises used: Odd.sub_odd, Odd.pow, even_iff_two_dvd
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
⊢ ¬2 ∣ x ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1))

Tactic:
simpa only [even_iff_two_dvd, ← Int.not_even_iff_odd] using hx_odd.pow

Premises used: Int.not_even_iff_odd, Odd.pow, even_iff_two_dvd
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
succ : ¬2 ∣ k
⊢ ¬Dvd.dvd (α := ℤ) 2 (↑k : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
succ : ∀ (hpn : 2 ∣ k), HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
⊢ ¬2 ∣ k

Tactic:
contrapose hpn
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
hpn : 2 ∣ k
rw : HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
| n + 1

Tactic:
rw [hk]
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
hpn : 2 ∣ k
succ : HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * 2 ∣ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
⊢ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * 2 ∣ n + 1

Tactic:
conv_rhs => rw [hk]
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
hpn : 2 ∣ k
⊢ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * 2 ∣ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k

Tactic:
mul_dvd_mul_left _ hpn

Premises used: mul_dvd_mul_left
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
hpn : 2 ∣ k
⊢ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * 2 ∣ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k

Tactic:
exact mul_dvd_mul_left _ hpn

Premises used: mul_dvd_mul_left
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hn : Even n
⊢ Odd x

Tactic:
rw [← even_iff_two_dvd, Int.not_even_iff_odd] at hx

Premises used: Int.not_even_iff_odd, even_iff_two_dvd
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hn : Even n
hx₁ : Odd x
⊢ Even n

Tactic:
rw [← even_iff_two_dvd, Int.not_even_iff_odd] at hx

Premises used: Int.not_even_iff_odd, even_iff_two_dvd
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : Odd x
hn : Even n
⊢ Even (-(x - y))

Tactic:
replace hxy := (@even_neg _ _ (x - y)).mpr (even_iff_two_dvd.mpr hxy)
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hx : Odd x
hn : Even n
hxy : Even (-(x - y))
⊢ Odd (-(x - y) + x)

Tactic:
Even.add_odd hxy hx

Premises used: Even.add_odd
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hx : Odd x
hn : Even n
hxy : Even (-(x - y))
h : y = -(x - y) + x
⊢ Odd y

Tactic:
convert! Even.add_odd hxy hx

Premises used: Even.add_odd
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hx : Odd x
hn : Even n
hxy : Even (-(x - y))
⊢ y = -(x - y) + x

Tactic:
abel
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hn : Even n
⊢ Odd y

Tactic:
have hy : Odd y := by
    rw [← even_iff_two_dvd, Int.not_even_iff_odd] at hx
    replace hxy := (@even_neg _ _ (x - y)).mpr (even_iff_two_dvd.mpr hxy)
    convert! Even.add_odd hxy hx
    abel
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hn : Even n
hy : Odd y
obtain :
  ∀ (d : ℕ),
    emultiplicity 2 (x ^ (d + d) - y ^ (d + d)) + 1 =
      emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(d + d) : ℤ)
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑n : ℤ)

Tactic:
obtain ⟨d, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
simp :
  emultiplicity 2 (HPow.hPow (β := ℕ) x 2 ^ d - HPow.hPow (β := ℕ) y 2 ^ d) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(2 * d) : ℤ)
⊢ emultiplicity 2 (x ^ (d + d) - y ^ (d + d)) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(d + d) : ℤ)

Tactic:
simp only [← two_mul, pow_mul]

Premises used: two_mul, pow_mul
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
rw : HSub.hSub (α := ℤ) 1 1 % 4 = 0
rw₁ : Odd x
⊢ 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2

Tactic:
rw [Int.dvd_iff_emod_eq_zero, Int.sub_emod, Int.sq_mod_four_eq_one_of_odd _,
      Int.sq_mod_four_eq_one_of_odd hy]

Premises used: Int.sq_mod_four_eq_one_of_odd, Int.sub_emod, Int.dvd_iff_emod_eq_zero
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ HSub.hSub (α := ℤ) 1 1 % 4 = 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ Odd x

Tactic:
simp only [← Int.not_even_iff_odd, even_iff_two_dvd, hx, not_false_iff]

Premises used: Int.not_even_iff_odd, even_iff_two_dvd, not_false_iff
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2

Tactic:
have hxy4 : 4 ∣ x ^ 2 - y ^ 2 := by
    rw [Int.dvd_iff_emod_eq_zero, Int.sub_emod, Int.sq_mod_four_eq_one_of_odd _,
      Int.sq_mod_four_eq_one_of_odd hy]
    · simp
    · simp only [← Int.not_even_iff_odd, even_iff_two_dvd, hx, not_false_iff]
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
rw :
  emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) +
      (emultiplicity (α := ℤ) 2 (↑2 : ℤ) + emultiplicity (α := ℤ) 2 (↑d : ℤ))
rw₁ : ¬2 ∣ HPow.hPow (β := ℕ) x 2
⊢ emultiplicity 2 (HPow.hPow (β := ℕ) x 2 ^ d - HPow.hPow (β := ℕ) y 2 ^ d) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(2 * d) : ℤ)

Tactic:
rw [Int.two_pow_sub_pow' d hxy4 _, sq_sub_sq, ← Int.ofNat_mul_ofNat,
    emultiplicity_mul Int.prime_two, emultiplicity_mul Int.prime_two]

Premises used: Int.prime_two, Int.two_pow_sub_pow', Int.ofNat_mul_ofNat, emultiplicity_mul, sq_sub_sq
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
this : emultiplicity (α := ℤ) 2 (↑2 : ℤ) = 1
rw :
  emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (1 + emultiplicity (α := ℤ) 2 (↑d : ℤ))
rw₁ :
  emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1)
rw₂ rw₃ :
  emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1
⊢ emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) +
      (emultiplicity (α := ℤ) 2 (↑2 : ℤ) + emultiplicity (α := ℤ) 2 (↑d : ℤ))

Tactic:
rw [this, add_comm 1, ← add_assoc]

Premises used: add_assoc, add_comm, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
suffices : emultiplicity (α := ℤ) 2 (↑2 : ℤ) = 1
⊢ emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) +
      (emultiplicity (α := ℤ) 2 (↑2 : ℤ) + emultiplicity (α := ℤ) 2 (↑d : ℤ))

Tactic:
suffices emultiplicity (2 : ℤ) ↑(2 : ℕ) = 1 by rw [this, add_comm 1, ← add_assoc]
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
norm_cast : emultiplicity (α := ℕ) 2 2 = 1
⊢ emultiplicity (α := ℤ) 2 (↑2 : ℤ) = 1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
rw : FiniteMultiplicity (α := ℕ) 2 2
⊢ emultiplicity (α := ℕ) 2 2 = 1

Tactic:
rw [FiniteMultiplicity.emultiplicity_self]

Premises used: FiniteMultiplicity.emultiplicity_self
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
rw : Ne (α := ℕ) 2 1 ∧ LT.lt (α := ℕ) 0 2
⊢ FiniteMultiplicity (α := ℕ) 2 2

Tactic:
rw [Nat.finiteMultiplicity_iff]

Premises used: Nat.finiteMultiplicity_iff
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
⊢ Ne (α := ℕ) 2 1 ∧ LT.lt (α := ℕ) 0 2

Tactic:
decide