awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Odd (HPow.hPow (β := ℕ) x 2)
⊢ ¬2 ∣ HPow.hPow (β := ℕ) x 2

Tactic:
rw [← even_iff_two_dvd, Int.not_even_iff_odd]

Premises used: Int.not_even_iff_odd, even_iff_two_dvd
-- 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
ha : Odd x
⊢ Odd (HPow.hPow (β := ℕ) x 2)

Tactic:
apply Odd.pow

Premises used: Odd.pow
-- 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
⊢ 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
n : ℕ
hn : Even n
inl :
  ∀ (hyx : y ≤ x),
    emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
inr :
  ∀ (hyx : x ≤ y),
    emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
obtain hyx | hyx := le_total y x

Premises used: le_total
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
inl :
  emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
rw [← Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
inl :
  emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
    emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x + y) : ℤ) + emultiplicity 2 (x - y) + emultiplicity 2 n
⊢ emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
rw [← Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
inl :
  emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
    emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x + y) : ℤ) + emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x - y) : ℤ) + emultiplicity 2 n
⊢ emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
    emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x + y) : ℤ) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
rw [← Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
inl :
  emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
    emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x + y) : ℤ) + emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x - y) : ℤ) + emultiplicity 2 n
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
iterate 3 rw [← Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
inl :
  emultiplicity (↑2 : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
    emultiplicity (↑2 : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
        emultiplicity (↑2 : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
      emultiplicity 2 n
⊢ emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
    emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x + y) : ℤ) + emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x - y) : ℤ) + emultiplicity 2 n

Tactic:
simp only [Int.ofNat_sub hyx, Int.ofNat_sub (pow_le_pow_left' hyx _), Int.natCast_add,
      Int.natCast_pow]

Premises used: Int.ofNat_sub, Int.natCast_add, Int.natCast_pow, pow_le_pow_left'
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
inl :
  ∀ (hx : ¬Dvd.dvd (α := ℤ) (↑2 : ℤ) (↑x : ℤ)) {n : ℕ} (hn : Even n) (hyx : y ≤ x),
    emultiplicity (↑2 : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
      emultiplicity (↑2 : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
          emultiplicity (↑2 : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
        emultiplicity 2 n
⊢ emultiplicity (↑2 : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
    emultiplicity (↑2 : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
        emultiplicity (↑2 : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
      emultiplicity 2 n

Tactic:
rw [← Int.natCast_dvd_natCast] at hx

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬Dvd.dvd (α := ℤ) (↑2 : ℤ) (↑x : ℤ)
n : ℕ
hn : Even n
hyx : y ≤ x
inl :
  ∀ (hxy : (↑2 : ℤ) ∣ HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) (hx : ¬Dvd.dvd (α := ℤ) (↑2 : ℤ) (↑x : ℤ)) {n : ℕ}
    (hn : Even n) (hyx : y ≤ x),
    emultiplicity (↑2 : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
      emultiplicity (↑2 : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
          emultiplicity (↑2 : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
        emultiplicity 2 n
⊢ emultiplicity (↑2 : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
    emultiplicity (↑2 : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
        emultiplicity (↑2 : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
      emultiplicity 2 n

Tactic:
rw [← Int.natCast_dvd_natCast, Int.ofNat_sub hyx] at hxy

Premises used: Int.ofNat_sub, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hxy : (↑2 : ℤ) ∣ HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
hx : ¬Dvd.dvd (α := ℤ) (↑2 : ℤ) (↑x : ℤ)
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity 2 (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
    emultiplicity 2 (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) + emultiplicity 2 (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
      emultiplicity (α := ℤ) 2 (↑n : ℤ)

Tactic:
Int.two_pow_sub_pow hxy hx hn

Premises used: Int.two_pow_sub_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hxy : (↑2 : ℤ) ∣ HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
hx : ¬Dvd.dvd (α := ℤ) (↑2 : ℤ) (↑x : ℤ)
n : ℕ
hn : Even n
hyx : y ≤ x
h : emultiplicity 2 n = emultiplicity (α := ℤ) 2 (↑n : ℤ)
⊢ emultiplicity (↑2 : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
    emultiplicity (↑2 : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
        emultiplicity (↑2 : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
      emultiplicity 2 n

Tactic:
convert! Int.two_pow_sub_pow hxy hx hn using 2

Premises used: Int.two_pow_sub_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hxy : (↑2 : ℤ) ∣ HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
hx : ¬Dvd.dvd (α := ℤ) (↑2 : ℤ) (↑x : ℤ)
n : ℕ
hn : Even n
hyx : y ≤ x
h : emultiplicity (α := ℤ) (↑2 : ℤ) (↑n : ℤ) = emultiplicity (α := ℤ) 2 (↑n : ℤ)
⊢ emultiplicity 2 n = emultiplicity (α := ℤ) 2 (↑n : ℤ)

Tactic:
rw [← Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hxy : (↑2 : ℤ) ∣ HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
hx : ¬Dvd.dvd (α := ℤ) (↑2 : ℤ) (↑x : ℤ)
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (α := ℤ) (↑2 : ℤ) (↑n : ℤ) = emultiplicity (α := ℤ) 2 (↑n : ℤ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : x ≤ y
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
simp only [Nat.sub_eq_zero_iff_le.mpr hyx,
      Nat.sub_eq_zero_iff_le.mpr (pow_le_pow_left' hyx n), emultiplicity_zero,
      top_add, add_top]

Premises used: Iff.mpr, add_top, Nat.sub_eq_zero_iff_le, emultiplicity_zero, top_add, pow_le_pow_left'
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
simp :
  HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x ^ n - y ^ n)) : ℕ∞) (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
⊢ padicValNat 2 (x ^ n - y ^ n) + 1 = padicValNat 2 (x + y) + padicValNat 2 (x - y) + padicValNat 2 n

Tactic:
simp only [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]

Premises used: Nat.cast_inj, Nat.cast_add
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
rw :
  emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
rw₁ : x ^ n - y ^ n ≠ 0
⊢ HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x ^ n - y ^ n)) : ℕ∞) (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)

Tactic:
rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
rw :
  emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    emultiplicity 2 (x + y) + (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
rw₁ : x + y ≠ 0
⊢ emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)

Tactic:
rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
rw :
  emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (↑(padicValNat 2 n) : ℕ∞)
rw₁ : x - y ≠ 0
⊢ emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    emultiplicity 2 (x + y) + (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)

Tactic:
rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
rw : emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
rw₁ : n ≠ 0
⊢ emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (↑(padicValNat 2 n) : ℕ∞)

Tactic:
rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
iterate :
  emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
iterate₁ : n ≠ 0
iterate₂ : x - y ≠ 0
iterate₃ : x + y ≠ 0
iterate₄ : x ^ n - y ^ n ≠ 0
⊢ HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x ^ n - y ^ n)) : ℕ∞) (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)

Tactic:
iterate 4 rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
Nat.two_pow_sub_pow hxy hx hneven

Premises used: Nat.two_pow_sub_pow, WithTop.some
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
exact Nat.two_pow_sub_pow hxy hx hneven

Premises used: Nat.two_pow_sub_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ n ≠ 0

Tactic:
hn
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ n ≠ 0

Tactic:
exact hn
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x - y ≠ 0

Tactic:
Nat.sub_ne_zero_of_lt hyx

Premises used: Nat.sub_ne_zero_of_lt
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x - y ≠ 0

Tactic:
exact Nat.sub_ne_zero_of_lt hyx

Premises used: Nat.sub_ne_zero_of_lt
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x + y ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x ^ n - y ^ n ≠ 0

Tactic:
simp [← Nat.pos_iff_ne_zero, tsub_pos_iff_lt, Nat.pow_lt_pow_left hyx hn]

Premises used: tsub_pos_iff_lt, Nat.pos_iff_ne_zero, Nat.pow_lt_pow_left
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x n : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ 2 ∣ x - 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x n : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 (x ^ n - 1) + 1 = padicValNat 2 (x + 1) + padicValNat 2 (x - 1) + padicValNat 2 n

Tactic:
simpa using pow_two_sub_pow h1x (by grind) hx hn hneven

Premises used: padicValNat.pow_two_sub_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ (x + 1) * (x - 1) ≠ 0

Tactic:
grind [mul_ne_zero]

Premises used: mul_ne_zero
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
refine : HPow.hPow (α := ℕ) (β := ℕ) 2 3 ∣ (x + 1) * (x - 1)
⊢ padicValNat 2 ((x + 1) * (x - 1)) ≥ 3

Tactic:
refine (padicValNat_dvd_iff_le (by grind [mul_ne_zero])).mp ?_

Premises used: Iff.mp, padicValNat_dvd_iff_le
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
simp : 8 ∣ HPow.hPow (β := ℕ) x 2 - 1
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 3 ∣ (x + 1) * (x - 1)

Tactic:
simp [← Nat.pow_two_sub_pow_two x 1]

Premises used: Nat.pow_two_sub_pow_two, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ 8 ∣ HPow.hPow (β := ℕ) x 2 - 1

Tactic:
grind [Nat.eight_dvd_sq_sub_one_of_odd]

Premises used: Nat.eight_dvd_sq_sub_one_of_odd
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 ((x + 1) * (x - 1)) ≥ 3

Tactic:
have : padicValNat 2 ((x + 1) * (x - 1)) ≥ 3 := by
    refine (padicValNat_dvd_iff_le (by grind [mul_ne_zero])).mp ?_
    simp [← Nat.pow_two_sub_pow_two x 1]
    grind [Nat.eight_dvd_sq_sub_one_of_odd]
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
this : padicValNat 2 ((x + 1) * (x - 1)) ≥ 3
⊢ padicValNat 2 (x ^ n - 1) + 1 = padicValNat 2 (x + 1) + padicValNat 2 (x - 1) + padicValNat 2 n

Tactic:
have := pow_two_sub_one h1x hx hn hneven
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
this_1 : padicValNat 2 ((x + 1) * (x - 1)) ≥ 3
this : padicValNat 2 (x ^ n - 1) + 1 = padicValNat 2 (x + 1) + padicValNat 2 (x - 1) + padicValNat 2 n
⊢ padicValNat 2 n + 2 ≤ padicValNat 2 (x ^ n - 1)

Tactic:
grind [← padicValNat.mul]

Premises used: padicValNat.mul
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
rw :
  (↑(padicValNat p (x ^ n - y ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
⊢ padicValNat p (x ^ n - y ^ n) = padicValNat p (x - y) + padicValNat p n

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]

Premises used: Nat.cast_inj, Nat.cast_add
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
rw : emultiplicity p (x ^ n - y ^ n) = HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
rw₁ : x ^ n - y ^ n ≠ 0
⊢ (↑(padicValNat p (x ^ n - y ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)

Tactic:
rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
rw : emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + (↑(padicValNat p n) : ℕ∞)
rw₁ : x - y ≠ 0
⊢ emultiplicity p (x ^ n - y ^ n) = HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)

Tactic:
rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
rw : emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
rw₁ : n ≠ 0
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + (↑(padicValNat p n) : ℕ∞)

Tactic:
rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
iterate : emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
iterate₁ : n ≠ 0
iterate₂ : x - y ≠ 0
iterate₃ : x ^ n - y ^ n ≠ 0
⊢ (↑(padicValNat p (x ^ n - y ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)

Tactic:
iterate 3 rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n

Tactic:
Nat.emultiplicity_pow_sub_pow hp.out hp1 hxy hx n

Premises used: Nat.emultiplicity_pow_sub_pow, Fact.out
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n

Tactic:
exact Nat.emultiplicity_pow_sub_pow hp.out hp1 hxy hx n

Premises used: Nat.emultiplicity_pow_sub_pow, Fact.out
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ n ≠ 0

Tactic:
hn
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ n ≠ 0

Tactic:
exact hn
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ x - y ≠ 0

Tactic:
Nat.sub_ne_zero_of_lt hyx

Premises used: Nat.sub_ne_zero_of_lt
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ x - y ≠ 0

Tactic:
exact Nat.sub_ne_zero_of_lt hyx

Premises used: Nat.sub_ne_zero_of_lt
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ x ^ n - y ^ n ≠ 0

Tactic:
Nat.sub_ne_zero_of_lt (Nat.pow_lt_pow_left hyx hn)

Premises used: Nat.sub_ne_zero_of_lt, Nat.pow_lt_pow_left
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ x ^ n - y ^ n ≠ 0

Tactic:
exact Nat.sub_ne_zero_of_lt (Nat.pow_lt_pow_left hyx hn)

Premises used: Nat.sub_ne_zero_of_lt, Nat.pow_lt_pow_left
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
zero : ∀ (hxy : p ∣ x + 0), padicValNat p (x ^ n + HPow.hPow (α := ℕ) 0 n) = padicValNat p (x + 0) + padicValNat p n
succ :
  ∀ (y : ℕ) (hxy : p ∣ x + (y + 1)), padicValNat p (x ^ n + (y + 1) ^ n) = padicValNat p (x + (y + 1)) + padicValNat p n
⊢ padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) + padicValNat p n

Tactic:
rcases y with - | y
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
hxy : p ∣ x + 0
⊢ padicValNat p (x ^ n + HPow.hPow (α := ℕ) 0 n) = padicValNat p (x + 0) + padicValNat p n

Tactic:
contradiction
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
succ :
  (↑(padicValNat p (x ^ n + (y + 1) ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
⊢ padicValNat p (x ^ n + (y + 1) ^ n) = padicValNat p (x + (y + 1)) + padicValNat p n

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]

Premises used: Nat.cast_inj, Nat.cast_add
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
succ :
  emultiplicity p (x ^ n + (y + 1) ^ n) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
succ₁ : x ^ n + (y + 1) ^ n ≠ 0
⊢ (↑(padicValNat p (x ^ n + (y + 1) ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)

Tactic:
rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
succ : emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + (↑(padicValNat p n) : ℕ∞)
succ₁ : x + (y + 1) ≠ 0
⊢ emultiplicity p (x ^ n + (y + 1) ^ n) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)

Tactic:
rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
succ : emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n
succ₁ : n ≠ 0
⊢ emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + (↑(padicValNat p n) : ℕ∞)

Tactic:
rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
succ : emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n
succ₁ : n ≠ 0
succ₂ : x + (y + 1) ≠ 0
succ₃ : x ^ n + (y + 1) ^ n ≠ 0
⊢ (↑(padicValNat p (x ^ n + (y + 1) ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)

Tactic:
iterate 3 rw [padicValNat_eq_emultiplicity]

Premises used: padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n

Tactic:
Nat.emultiplicity_pow_add_pow hp.out hp1 hxy hx hn

Premises used: Nat.emultiplicity_pow_add_pow, Fact.out