awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
rw : (↑(p ^ e * M') : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
⊢ (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)

Tactic:
rw [← hdecomp]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
⊢ (↑(p ^ e * M') : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
⊢ (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)

Tactic:
have hM_eq : (M : ℚ) = ↑(p ^ e) * ↑M' := by rw [← hdecomp]; simp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
rw :
  HPow.hPow (α := ℚ) (↑p : ℚ) N / HPow.hPow (α := ℚ) (↑p : ℚ) e / (↑M' : ℚ) =
    HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)

Tactic:
rw [hM_eq, Nat.cast_pow, div_mul_eq_div_div]

Premises used: Nat.cast_pow, div_mul_eq_div_div
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
e_a : HPow.hPow (α := ℚ) (↑p : ℚ) N / HPow.hPow (α := ℚ) (↑p : ℚ) e = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) N / HPow.hPow (α := ℚ) (↑p : ℚ) e / (↑M' : ℚ) =
    HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
e_a : HPow.hPow (α := ℚ) (↑p : ℚ) N = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) * HPow.hPow (α := ℚ) (↑p : ℚ) e
e_a₁ : HPow.hPow (α := ℚ) (↑p : ℚ) N = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e + e)
e_a₂ e_a₃ : HPow.hPow (α := ℚ) (↑p : ℚ) N = HPow.hPow (α := ℚ) (↑p : ℚ) N
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) N / HPow.hPow (α := ℚ) (↑p : ℚ) e = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e)

Tactic:
rw [div_eq_iff (pow_ne_zero e hp_ne), ← pow_add, Nat.sub_add_cancel hv]

Premises used: pow_add, pow_ne_zero, div_eq_iff, Nat.sub_add_cancel
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)

Tactic:
have hrw : (p : ℚ) ^ N / M = (p : ℚ) ^ (N - e) / M' := by
    rw [hM_eq, Nat.cast_pow, div_mul_eq_div_div]
    congr 1
    rw [div_eq_iff (pow_ne_zero e hp_ne), ← pow_add, Nat.sub_add_cancel hv]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
norm_cast : HDiv.hDiv (α := ℚ) (↑(p ^ (N - e)) : ℚ) (↑M' : ℚ) = (↑(NNRat.divNat (p ^ (N - e)) M') : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ) = Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(p ^ (N - e)) : ℚ) (↑M' : ℚ) = (↑(NNRat.divNat (p ^ (N - e)) M') : ℚ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ) = Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)

Tactic:
have hM'_eq : ((p : ℚ) ^ (N - e) / (M' : ℚ)) = Rat.divInt (p ^ (N - e) : ℤ) (M' : ℤ) := by
    norm_cast
    simp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
hM'_eq : HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ) = Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)
rw : pIntegral p (HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ))
⊢ pIntegral p (HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ))

Tactic:
rw [hrw]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
hM'_eq : HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ) = Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)
rw : (Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)).den ∣ M'
⊢ (HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)).den ∣ M'

Tactic:
rw [hM'_eq]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
hM'_eq : HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ) = Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)
⊢ (Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)).den ∣ M'

Tactic:
Int.natCast_dvd_natCast.mp (Rat.den_dvd _ _)

Premises used: Iff.mp, Rat.den_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
hM'_eq : HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ) = Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)
⊢ (Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)).den ∣ M'

Tactic:
exact Int.natCast_dvd_natCast.mp (Rat.den_dvd _ _)

Premises used: Iff.mp, Rat.den_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
hM'_eq : HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ) = Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)
⊢ pIntegral p (HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ))

Tactic:
exact Rat.padicValuation_le_one_iff.2 ((Nat.Prime.coprime_iff_not_dvd Fact.out).1
    (hM'_cop.coprime_dvd_left (by
      rw [hM'_eq]; exact Int.natCast_dvd_natCast.mp (Rat.den_dvd _ _))).symm)

Premises used: Iff.mpr, Nat.Coprime.symm, Nat.Coprime.coprime_dvd_left, Iff.mp, Nat.Prime.coprime_iff_not_dvd, Fact.out, Rat.padicValuation_le_one_iff
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
pos : ∀ (hcase : p = 2 ∧ d = 2), ((d + 1).factorization : (a : ℕ) → ℕ) p ≤ d - 1
neg : ∀ (hcase : ¬(p = 2 ∧ d = 2)), ((d + 1).factorization : (a : ℕ) → ℕ) p ≤ d - 1
⊢ ((d + 1).factorization : (a : ℕ) → ℕ) p ≤ d - 1

Tactic:
by_cases hcase : p = 2 ∧ d = 2
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : p = 2 ∧ d = 2
pos :
  ∀ [Fact (Nat.Prime 2)] (hd : GE.ge (α := ℕ) 2 2),
    ((HAdd.hAdd (α := ℕ) 2 1).factorization : (a : ℕ) → ℕ) 2 ≤ HSub.hSub (α := ℕ) 2 1
⊢ ((d + 1).factorization : (a : ℕ) → ℕ) p ≤ d - 1

Tactic:
obtain ⟨rfl, rfl⟩ := hcase

Premises used: rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
inst : Fact (Nat.Prime 2)
hd : GE.ge (α := ℕ) 2 2
⊢ ¬Dvd.dvd (α := ℕ) 2 3

Tactic:
decide
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
inst : Fact (Nat.Prime 2)
hd : GE.ge (α := ℕ) 2 2
⊢ ((HAdd.hAdd (α := ℕ) 2 1).factorization : (a : ℕ) → ℕ) 2 ≤ HSub.hSub (α := ℕ) 2 1

Tactic:
simp [Nat.factorization_eq_zero_of_not_dvd (by decide : ¬(2 ∣ 3))]

Premises used: Nat.factorization_eq_zero_of_not_dvd
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
neg : d + 1 ≤ p ^ (d - 1)
⊢ ((d + 1).factorization : (a : ℕ) → ℕ) p ≤ d - 1

Tactic:
apply Nat.factorization_le_of_le_pow

Premises used: Nat.factorization_le_of_le_pow
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
⊢ 2 ≤ p

Tactic:
have hp2 := (Fact.out : p.Prime).two_le
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
neg : ∀ n ≥ 2, ¬(p = 2 ∧ n = 2) → n + 1 ≤ p ^ (n - 1)
⊢ d + 1 ≤ p ^ (d - 1)

Tactic:
suffices ∀ n : ℕ, n ≥ 2 → ¬(p = 2 ∧ n = 2) → n + 1 ≤ p ^ (n - 1) from this d hd hcase
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n : ℕ
hne' : ¬(p = 2 ∧ Eq (α := ℕ) 2 2)
neg : ∀ (hne' : ¬p = 2), 3 ≤ p
⊢ HAdd.hAdd (α := ℕ) 2 1 ≤ p ^ HSub.hSub (α := ℕ) 2 1

Tactic:
norm_num at hne' ⊢
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n : ℕ
hne' : ¬p = 2
⊢ 3 ≤ p

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
pos : ∀ (hm2 : p = 2 ∧ m = 2), m.succ + 1 ≤ p ^ (m.succ - 1)
neg : ∀ (hm2 : ¬(p = 2 ∧ m = 2)), m.succ + 1 ≤ p ^ (m.succ - 1)
⊢ m.succ + 1 ≤ p ^ (m.succ - 1)

Tactic:
by_cases hm2 : p = 2 ∧ m = 2
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : p = 2 ∧ m = 2
pos :
  ∀ [Fact (Nat.Prime 2)] (hcase : ¬(Eq (α := ℕ) 2 2 ∧ d = 2)) (hp2 : LE.le (α := ℕ) 2 2) (hm : Nat.le 2 2)
    (IH :
      ∀ (hne' : ¬(Eq (α := ℕ) 2 2 ∧ Eq (α := ℕ) 2 2)),
        HAdd.hAdd (α := ℕ) 2 1 ≤ HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 2 1))
    (hne' : ¬(Eq (α := ℕ) 2 2 ∧ succ 2 = 2)), succ 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (succ 2 - 1)
⊢ m.succ + 1 ≤ p ^ (m.succ - 1)

Tactic:
obtain ⟨rfl, rfl⟩ := hm2

Premises used: rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
d : ℕ
hd : d ≥ 2
n : ℕ
inst : Fact (Nat.Prime 2)
hcase : ¬(Eq (α := ℕ) 2 2 ∧ d = 2)
hp2 : LE.le (α := ℕ) 2 2
hm : Nat.le 2 2
IH :
  ∀ (hne' : ¬(Eq (α := ℕ) 2 2 ∧ Eq (α := ℕ) 2 2)),
    HAdd.hAdd (α := ℕ) 2 1 ≤ HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 2 1)
hne' : ¬(Eq (α := ℕ) 2 2 ∧ succ 2 = 2)
⊢ succ 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (succ 2 - 1)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
linarith :
  p ^ (m - 1) + 1 < m + 1 + 1 →
    -1 + (HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1) + 1 + 1 - (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 1)) +
        (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1)) =
      0
⊢ m + 1 + 1 ≤ p ^ (m - 1) + 1

Tactic:
linarith [IH hm2]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
⊢ 0 < p

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
nlinarith :
  p ^ (m - 1) * p < p ^ (m - 1) + 1 →
    HMul.hMul (α := ℤ) 2 (-1) + 2 * HSub.hSub (α := ℤ) 2 (↑p : ℤ) +
            2 * (HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1) * (↑p : ℤ) + 1 - (HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1) + 1)) +
          (0 - HSub.hSub (α := ℤ) 0 (↑p : ℤ) * (1 - HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1))) +
        (0 - HSub.hSub (α := ℤ) 2 (↑p : ℤ) * (1 - HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1))) =
      0
nlinarith₁ nlinarith₂ nlinarith₃ : p ^ (m - 1) * p < p ^ (m - 1) + 1 → GT.gt (α := ℤ) 2 0
⊢ p ^ (m - 1) + 1 ≤ p ^ (m - 1) * p

Tactic:
nlinarith [Nat.one_le_pow (m - 1) p (by lia)]

Premises used: HSub.hSub, Nat.one_le_pow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
⊢ m = m - 1 + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
rw : p ^ (m - 1 + 1 - 1) * p = p ^ (m - 1 + 1)
⊢ p ^ (m - 1) * p = p ^ m

Tactic:
rw [show m = m - 1 + 1 by lia]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
⊢ p ^ (m - 1 + 1 - 1) * p = p ^ (m - 1 + 1)

Tactic:
pow_succ ..

Premises used: pow_succ, Nat.pow, Nat.pred
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
⊢ p ^ (m - 1 + 1 - 1) * p = p ^ (m - 1 + 1)

Tactic:
exact pow_succ ..

Premises used: pow_succ
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
calc : m + 1 + 1 ≤ p ^ (m - 1) + 1
calc₁ : p ^ (m - 1) + 1 ≤ p ^ (m - 1) * p
calc₂ : p ^ (m - 1) * p = p ^ m
⊢ m.succ + 1 ≤ p ^ (m.succ - 1)

Tactic:
calc m + 1 + 1 ≤ p ^ (m - 1) + 1 := by linarith [IH hm2]
          _ ≤ p ^ (m - 1) * p := by nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
          _ = p ^ m := by rw [show m = m - 1 + 1 by lia]; exact pow_succ ..

Premises used: HSub.hSub, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n : ℕ
hn : n ≥ 2
hne' : ¬(p = 2 ∧ n = 2)
neg : ∀ (hne' : ¬(p = 2 ∧ Eq (α := ℕ) 2 2)), HAdd.hAdd (α := ℕ) 2 1 ≤ p ^ HSub.hSub (α := ℕ) 2 1
neg₁ :
  ∀ {m : ℕ} (hm : Nat.le 2 m) (IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)) (hne' : ¬(p = 2 ∧ m.succ = 2)),
    m.succ + 1 ≤ p ^ (m.succ - 1)
⊢ n + 1 ≤ p ^ (n - 1)

Tactic:
induction hn with
    | refl => norm_num at hne' ⊢; lia
    | @step m hm IH =>
      by_cases hm2 : p = 2 ∧ m = 2
      · obtain ⟨rfl, rfl⟩ := hm2; norm_num
      · calc m + 1 + 1 ≤ p ^ (m - 1) + 1 := by linarith [IH hm2]
          _ ≤ p ^ (m - 1) * p := by nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
          _ = p ^ m := by rw [show m = m - 1 + 1 by lia]; exact pow_succ ..

Premises used: refl, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬False
⊢ HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1 ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
norm_cast : ¬Int.subNatNat (2 * k) (2 * m) + 1 = 0
⊢ HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
⊢ ¬Int.subNatNat (2 * k) (2 * m) + 1 = 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
rw :
  (↑((2 * k + 1).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1) * x =
    (↑((2 * k).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) * x
⊢ (↑((2 * k + 1).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
    (↑((2 * k).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1)

Tactic:
rw [div_eq_div_iff (by norm_cast) (by norm_cast; lia), mul_right_comm _ x, mul_right_comm _ x]

Premises used: div_eq_div_iff, mul_right_comm
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
⊢ (↑((2 * k + 1).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1) * x =
    (↑((2 * k).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) * x

Tactic:
congrArg (· * x) ?_

Premises used: HMul.hMul, congrArg
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
refine :
  (↑((2 * k + 1).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1) =
    (↑((2 * k).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
⊢ (↑((2 * k + 1).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1) * x =
    (↑((2 * k).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) * x

Tactic:
refine congrArg (· * x) ?_

Premises used: HMul.hMul, congrArg
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
norm_cast : Int.subNatNat (2 * k) (2 * m) + 1 = (↑(2 * k + 1 - 2 * m) : ℤ)
⊢ HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 = (↑(2 * k + 1 - 2 * m) : ℚ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
⊢ Int.subNatNat (2 * k) (2 * m) + 1 = (↑(2 * k + 1 - 2 * m) : ℤ)

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
rw :
  HMul.hMul (α := ℚ) (↑((2 * k + 1).choose (2 * m)) : ℚ) (↑(2 * k + 1 - 2 * m) : ℚ) =
    (↑((2 * k).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
⊢ (↑((2 * k + 1).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1) =
    (↑((2 * k).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)

Tactic:
rw [show (2 * (k : ℚ) - 2 * (m : ℚ) + 1) = (↑(2 * k + 1 - 2 * m) : ℚ) by norm_cast; lia]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
⊢ HMul.hMul (α := ℚ) (↑((2 * k + 1).choose (2 * m)) : ℚ) (↑(2 * k + 1 - 2 * m) : ℚ) =
    (↑((2 * k).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)

Tactic:
exact_mod_cast Nat.choose_mul_succ_eq (2 * k) (2 * m) |>.symm

Premises used: Nat.choose_mul_succ_eq, HMul.hMul, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
hd : 2 * k - 2 * m ≥ 2
set :
  let d := 2 * k - 2 * m;
  ∀ (hd : d ≥ 2) (hd_def : d = 2 * k - 2 * m),
    pIntegral p
      ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (d - 1) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
⊢ pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))

Tactic:
set d := 2 * k - 2 * m with hd_def
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
⊢ d + 1 ≠ 0 ∧ 2 * k - 2 * m - 1 = d - 1 ∧ 2 * m ≤ 2 * k

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
⊢ d + 1 ≠ 0

Tactic:
have ⟨hd_plus_one_ne_zero, h_exp, hkm⟩ :
      d + 1 ≠ 0 ∧ 2 * k - 2 * m - 1 = d - 1 ∧ 2 * m ≤ 2 * k := by lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
⊢ 2 * k - 2 * m - 1 = d - 1

Tactic:
have ⟨hd_plus_one_ne_zero, h_exp, hkm⟩ :
      d + 1 ≠ 0 ∧ 2 * k - 2 * m - 1 = d - 1 ∧ 2 * m ≤ 2 * k := by lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
⊢ 2 * m ≤ 2 * k

Tactic:
have ⟨hd_plus_one_ne_zero, h_exp, hkm⟩ :
      d + 1 ≠ 0 ∧ 2 * k - 2 * m - 1 = d - 1 ∧ 2 * m ≤ 2 * k := by lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
simp : HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 = (↑(2 * k - 2 * m + 1) : ℚ)
⊢ HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 = (↑(d + 1) : ℚ)

Tactic:
simp only [hd_def]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
push_cast :
  HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 =
    HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1
⊢ HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 = (↑(2 * k - 2 * m + 1) : ℚ)

Tactic:
push_cast [Nat.cast_sub hkm]

Premises used: Nat.cast_sub
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
⊢ HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 =
    HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1

Tactic:
ring