awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun (t : ℕ) ↦ p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1
have inl : Finset.image (fun (t : ℕ) ↦ p ^ (t + 1)) (Finset.range (padicValNat p 0)) ⊆ (divisors 0).erase 1
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
inl : Finset.image (fun (t : ℕ) ↦ p ^ (t + 1)) (Finset.range (padicValNat p 0)) ⊆ (divisors 0).erase 1
⊢ Finset.image (fun (t : ℕ) ↦ p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1
have inr : ∀ (hn : n ≠ 0), Finset.image (fun (t : ℕ) ↦ p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : Membership.mem (γ := Finset ℕ) (Finset.image (fun (t : ℕ) ↦ p ^ (t + 1)) (Finset.range (padicValNat p n))) t
⊢ t ∈ n.divisors.erase 1
have ht₁ : ∃ a < padicValNat p n, p ^ (a + 1) = t
Tactic: simp only [Finset.mem_image, Finset.mem_range] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : ∃ a < padicValNat p n, p ^ (a + 1) = t
⊢ t ∈ n.divisors.erase 1
have inr : ∀ (k : ℕ) (hk : k < padicValNat p n), p ^ (k + 1) ∈ n.divisors.erase 1
Tactic: obtain ⟨k, hk, rfl⟩ := ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ∈ n.divisors.erase 1
have inr : p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∣ n ∧ n ≠ 0
Tactic: rw [Finset.mem_erase, Nat.mem_divisors]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∣ n ∧ n ≠ 0
have inr : p ^ (k + 1) ≠ 1
Tactic: refine ⟨?_, (pow_dvd_pow p <| succ_le_iff.2 hk).trans pow_padicValNat_dvd, hn⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * n)! = padicValNat p n ! + n
have a : Eq (α := ℕ∞) (↑(padicValNat p (p * n)!) : ℕ∞) (↑(padicValNat p n ! + n) : ℕ∞)
Tactic: apply Nat.cast_injective (R := ℕ∞)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := ℕ∞) (↑(padicValNat p (p * n)!) : ℕ∞) (↑(padicValNat p n ! + n) : ℕ∞)
have a : emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)
Tactic: rw [padicValNat_eq_emultiplicity <| factorial_ne_zero (p * n), Nat.cast_add,
      padicValNat_eq_emultiplicity <| factorial_ne_zero n]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p m : ℕ
hp : Fact (Nat.Prime p)
h : 0 < p
⊢ padicValNat p (p * m + 0)! = padicValNat p (p * m)!
have zero : padicValNat p (p * m)! = padicValNat p (p * m)!
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : ∀ (h : n < p), padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
⊢ padicValNat p (p * m + (n + 1))! = padicValNat p (p * m)!
have succ : padicValNat p (p * m + n).succ ! = padicValNat p (p * m)!
Tactic: rw [add_succ, factorial_succ,
      padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
      hn <| lt_of_succ_lt h, ← add_succ,
      padicValNat_eq_zero_of_mem_Ioo ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
        (Nat.mul_add _ _ _▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
      zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : ∀ (h : n < p), padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
succ : padicValNat p (p * m + n).succ ! = padicValNat p (p * m)!
⊢ padicValNat p (p * m + (n + 1))! = padicValNat p (p * m)!
have succ₁ : padicValNat p ((p * m + n + 1) * (p * m + n)!) = padicValNat p (p * m)!
Tactic: rw [add_succ, factorial_succ,
      padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
      hn <| lt_of_succ_lt h, ← add_succ,
      padicValNat_eq_zero_of_mem_Ioo ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
        (Nat.mul_add _ _ _▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
      zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : ∀ (h : n < p), padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
succ : padicValNat p (p * m + n).succ ! = padicValNat p (p * m)!
succ₁ : padicValNat p ((p * m + n + 1) * (p * m + n)!) = padicValNat p (p * m)!
⊢ padicValNat p (p * m + (n + 1))! = padicValNat p (p * m)!
have succ₂ : padicValNat p (p * m + n).succ + padicValNat p (p * m + n)! = padicValNat p (p * m)!
Tactic: rw [add_succ, factorial_succ,
      padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
      hn <| lt_of_succ_lt h, ← add_succ,
      padicValNat_eq_zero_of_mem_Ioo ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
        (Nat.mul_add _ _ _▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
      zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : ∀ (h : n < p), padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
succ : padicValNat p (p * m + n).succ ! = padicValNat p (p * m)!
succ₁ : padicValNat p ((p * m + n + 1) * (p * m + n)!) = padicValNat p (p * m)!
succ₂ : padicValNat p (p * m + n).succ + padicValNat p (p * m + n)! = padicValNat p (p * m)!
⊢ padicValNat p (p * m + (n + 1))! = padicValNat p (p * m)!
have succ₃ : padicValNat p (p * m + n).succ + padicValNat p (p * m)! = padicValNat p (p * m)!
Tactic: rw [add_succ, factorial_succ,
      padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
      hn <| lt_of_succ_lt h, ← add_succ,
      padicValNat_eq_zero_of_mem_Ioo ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
        (Nat.mul_add _ _ _▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
      zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : ∀ (h : n < p), padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
succ : padicValNat p (p * m + n).succ ! = padicValNat p (p * m)!
succ₁ : padicValNat p ((p * m + n + 1) * (p * m + n)!) = padicValNat p (p * m)!
succ₂ : padicValNat p (p * m + n).succ + padicValNat p (p * m + n)! = padicValNat p (p * m)!
succ₃ : padicValNat p (p * m + n).succ + padicValNat p (p * m)! = padicValNat p (p * m)!
⊢ padicValNat p (p * m + (n + 1))! = padicValNat p (p * m)!
have succ₄ : padicValNat p (p * m + n.succ) + padicValNat p (p * m)! = padicValNat p (p * m)!
Tactic: rw [add_succ, factorial_succ,
      padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
      hn <| lt_of_succ_lt h, ← add_succ,
      padicValNat_eq_zero_of_mem_Ioo ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
        (Nat.mul_add _ _ _▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
      zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : ∀ (h : n < p), padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
succ : padicValNat p (p * m + n).succ ! = padicValNat p (p * m)!
succ₁ : padicValNat p ((p * m + n + 1) * (p * m + n)!) = padicValNat p (p * m)!
succ₂ : padicValNat p (p * m + n).succ + padicValNat p (p * m + n)! = padicValNat p (p * m)!
succ₃ : padicValNat p (p * m + n).succ + padicValNat p (p * m)! = padicValNat p (p * m)!
succ₄ : padicValNat p (p * m + n.succ) + padicValNat p (p * m)! = padicValNat p (p * m)!
⊢ padicValNat p (p * m + (n + 1))! = padicValNat p (p * m)!
have succ₅ : 0 + padicValNat p (p * m)! = padicValNat p (p * m)!
Tactic: rw [add_succ, factorial_succ,
      padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
      hn <| lt_of_succ_lt h, ← add_succ,
      padicValNat_eq_zero_of_mem_Ioo ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
        (Nat.mul_add _ _ _▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
      zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : ∀ (h : n < p), padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
succ : padicValNat p (p * m + n).succ ! = padicValNat p (p * m)!
succ₁ : padicValNat p ((p * m + n + 1) * (p * m + n)!) = padicValNat p (p * m)!
succ₂ : padicValNat p (p * m + n).succ + padicValNat p (p * m + n)! = padicValNat p (p * m)!
succ₃ : padicValNat p (p * m + n).succ + padicValNat p (p * m)! = padicValNat p (p * m)!
succ₄ : padicValNat p (p * m + n.succ) + padicValNat p (p * m)! = padicValNat p (p * m)!
succ₅ : 0 + padicValNat p (p * m)! = padicValNat p (p * m)!
⊢ padicValNat p (p * m + (n + 1))! = padicValNat p (p * m)!
have succ₆ : padicValNat p (p * m)! = padicValNat p (p * m)!
Tactic: rw [add_succ, factorial_succ,
      padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
      hn <| lt_of_succ_lt h, ← add_succ,
      padicValNat_eq_zero_of_mem_Ioo ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
        (Nat.mul_add _ _ _▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
      zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n m : ℕ
hp : Fact (Nat.Prime p)
h : n < p
⊢ padicValNat p (p * m + n)! = padicValNat p (p * m)!
have zero : ∀ (h : 0 < p), padicValNat p (p * m + 0)! = padicValNat p (p * m)!
Tactic: induction n with
  | zero => rw [add_zero]
  | succ n hn =>
    rw [add_succ, factorial_succ,
      padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
      hn <| lt_of_succ_lt h, ← add_succ,
      padicValNat_eq_zero_of_mem_Ioo ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
        (Nat.mul_add _ _ _▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
      zero_add]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n m : ℕ
hp : Fact (Nat.Prime p)
h : n < p
zero : ∀ (h : 0 < p), padicValNat p (p * m + 0)! = padicValNat p (p * m)!
⊢ padicValNat p (p * m + n)! = padicValNat p (p * m)!
have succ : ∀ (n : ℕ) (hn : ∀ (h : n < p), padicValNat p (p * m + n)! = padicValNat p (p * m)!) (h : n + 1 < p),
  padicValNat p (p * m + (n + 1))! = padicValNat p (p * m)!
Tactic: induction n with
  | zero => rw [add_zero]
  | succ n hn =>
    rw [add_succ, factorial_succ,
      padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
      hn <| lt_of_succ_lt h, ← add_succ,
      padicValNat_eq_zero_of_mem_Ioo ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
        (Nat.mul_add _ _ _▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
      zero_add]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * (n / p))! = padicValNat p n !
have nth_rw : padicValNat p (p * (n / p))! = padicValNat p (p * (n / p) + n % p)!
Tactic: nth_rw 2 [← div_add_mod n p]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (p - 1) * padicValNat p n ! = n - (p.digits n).sum
have rw : (p - 1) * ∑ i ∈ Finset.Ico 1 (log p n + 1).succ, n / p ^ i = n - (p.digits n).sum
Tactic: rw [padicValNat_factorial <| lt_succ_of_lt <| lt_add_one (log p n)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : (p - 1) * ∑ i ∈ Finset.Ico (HAdd.hAdd (α := ℕ) 0 1) (log p n + 1 + 1), n / p ^ i = n - (p.digits n).sum
⊢ (p - 1) * ∑ i ∈ Finset.Ico (HAdd.hAdd (α := ℕ) 0 1) (log p n + 1).succ, n / p ^ i = n - (p.digits n).sum
have rw₁ : (p - 1) * ∑ x ∈ Finset.Ico 0 (log p n + 1), n / p ^ (x + 1) = n - (p.digits n).sum
Tactic: rw [Nat.succ_eq_add_one, ← Finset.sum_Ico_add' _ 0 _ 1,
    Ico_zero_eq_range, ← sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, Nat.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : (p - 1) * ∑ i ∈ Finset.Ico (HAdd.hAdd (α := ℕ) 0 1) (log p n + 1 + 1), n / p ^ i = n - (p.digits n).sum
rw₁ : (p - 1) * ∑ x ∈ Finset.Ico 0 (log p n + 1), n / p ^ (x + 1) = n - (p.digits n).sum
⊢ (p - 1) * ∑ i ∈ Finset.Ico (HAdd.hAdd (α := ℕ) 0 1) (log p n + 1).succ, n / p ^ i = n - (p.digits n).sum
have rw₂ : (p - 1) * ∑ x ∈ Finset.range (log p n + 1), n / p ^ (x + 1) = n - (p.digits n).sum
Tactic: rw [Nat.succ_eq_add_one, ← Finset.sum_Ico_add' _ 0 _ 1,
    Ico_zero_eq_range, ← sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, Nat.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : (p - 1) * ∑ i ∈ Finset.Ico (HAdd.hAdd (α := ℕ) 0 1) (log p n + 1 + 1), n / p ^ i = n - (p.digits n).sum
rw₁ : (p - 1) * ∑ x ∈ Finset.Ico 0 (log p n + 1), n / p ^ (x + 1) = n - (p.digits n).sum
rw₂ : (p - 1) * ∑ x ∈ Finset.range (log p n + 1), n / p ^ (x + 1) = n - (p.digits n).sum
⊢ (p - 1) * ∑ i ∈ Finset.Ico (HAdd.hAdd (α := ℕ) 0 1) (log p n + 1).succ, n / p ^ i = n - (p.digits n).sum
have rw₃ : (p - 1) * ∑ x ∈ Finset.range (log p n + 1), n / p ^ (x + 1) =
  (p - 1) * ∑ i ∈ Finset.range (log p n).succ, n / p ^ i.succ
Tactic: rw [Nat.succ_eq_add_one, ← Finset.sum_Ico_add' _ 0 _ 1,
    Ico_zero_eq_range, ← sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, Nat.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ (p - 1) * padicValNat p n ! < n
have rw : n - (p.digits n).sum < n
Tactic: rw [sub_one_mul_padicValNat_factorial n]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ n - (p.digits n).sum < n
have refine : 0 < (p.digits n).sum
Tactic: refine Nat.sub_lt_self ?_ (digit_sum_le p n)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ 0 < (p.digits n).sum
have hnil : p.digits n ≠ []
Tactic: have hnil : p.digits n ≠ [] := Nat.digits_ne_nil_iff_ne_zero.mpr hn
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ! < n
have apply : padicValNat p n ! ≤ (p - 1) * padicValNat p n !
Tactic: apply lt_of_le_of_lt _ (sub_one_mul_padicValNat_factorial_lt_of_ne_zero p hn)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
| padicValNat p n !
have rw : 1 * padicValNat p n !
Tactic: rw [← one_mul (padicValNat p n !)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ! ≤ (p - 1) * padicValNat p n !
have conv_lhs : 1 * padicValNat p n ! ≤ (p - 1) * padicValNat p n !
Tactic: conv_lhs => rw [← one_mul (padicValNat p n !)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ 1 * padicValNat p n ! ≤ (p - 1) * padicValNat p n !
have bc : 1 ≤ p - 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ padicValNat p n ! ≤ n
have pos : ∀ (hn : n = 0), padicValNat p n ! ≤ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
pos : ∀ (hn : n = 0), padicValNat p n ! ≤ n
⊢ padicValNat p n ! ≤ n
have neg : ∀ (hn : ¬n = 0), padicValNat p n ! ≤ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
⊢ (p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
have h : k ≤ n + k
Tactic: have h : k ≤ n + k := by exact Nat.le_add_left k n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
have simp : (p - 1) * padicValNat p ((n + k)! / (k ! * (n + k - k)!)) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Tactic: simp only [Nat.choose_eq_factorial_div_factorial h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p ((n + k)! / (k ! * (n + k - k)!)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
have rw : (p - 1) * padicValNat p (n + k)! - ((p - 1) * padicValNat p k ! + (p - 1) * padicValNat p (n + k - k)!) =
  (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Tactic: rw [padicValNat.div_of_dvd <| factorial_mul_factorial_dvd_factorial h, Nat.mul_sub_left_distrib,
      padicValNat.mul (factorial_ne_zero _) (factorial_ne_zero _), Nat.mul_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p (n + k)! - ((p - 1) * padicValNat p k ! + (p - 1) * padicValNat p (n + k - k)!) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
have simp : n + k - (p.digits (n + k)).sum - (k - (p.digits k).sum + (n + k - k - (p.digits (n + k - k)).sum)) =
  (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Tactic: simp only [sub_one_mul_padicValNat_factorial]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (p.digits (n + k)).sum - (k - (p.digits k).sum + (n + k - k - (p.digits (n + k - k)).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
have rw : n + k - (p.digits (n + k)).sum - (k + (n + k - k - (p.digits (n + k - k)).sum) - (p.digits k).sum) =
  (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Tactic: rw [← Nat.sub_add_comm <| digit_sum_le p k, Nat.add_sub_cancel n k, ← Nat.add_sub_assoc <|
      digit_sum_le p n, Nat.sub_sub (k + n), ← Nat.sub_right_comm, Nat.sub_sub, sub_add_eq,
      add_comm, tsub_tsub_assoc (Nat.le_refl (k + n)) <| (add_comm k n) ▸ (Nat.add_le_add
      (digit_sum_le p n) (digit_sum_le p k)), Nat.sub_self (k + n), zero_add, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
rw :
  n + k - (p.digits (n + k)).sum - (k + (n + k - k - (p.digits (n + k - k)).sum) - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
⊢ n + k - (p.digits (n + k)).sum - (k - (p.digits k).sum + (n + k - k - (p.digits (n + k - k)).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
have rw₁ : n + k - (p.digits (n + k)).sum - (k + (n - (p.digits n).sum) - (p.digits k).sum) =
  (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Tactic: rw [← Nat.sub_add_comm <| digit_sum_le p k, Nat.add_sub_cancel n k, ← Nat.add_sub_assoc <|
      digit_sum_le p n, Nat.sub_sub (k + n), ← Nat.sub_right_comm, Nat.sub_sub, sub_add_eq,
      add_comm, tsub_tsub_assoc (Nat.le_refl (k + n)) <| (add_comm k n) ▸ (Nat.add_le_add
      (digit_sum_le p n) (digit_sum_le p k)), Nat.sub_self (k + n), zero_add, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
rw :
  n + k - (p.digits (n + k)).sum - (k + (n + k - k - (p.digits (n + k - k)).sum) - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₁ :
  n + k - (p.digits (n + k)).sum - (k + (n - (p.digits n).sum) - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
⊢ n + k - (p.digits (n + k)).sum - (k - (p.digits k).sum + (n + k - k - (p.digits (n + k - k)).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
have rw₂ : n + k - (p.digits (n + k)).sum - (k + n - (p.digits n).sum - (p.digits k).sum) =
  (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Tactic: rw [← Nat.sub_add_comm <| digit_sum_le p k, Nat.add_sub_cancel n k, ← Nat.add_sub_assoc <|
      digit_sum_le p n, Nat.sub_sub (k + n), ← Nat.sub_right_comm, Nat.sub_sub, sub_add_eq,
      add_comm, tsub_tsub_assoc (Nat.le_refl (k + n)) <| (add_comm k n) ▸ (Nat.add_le_add
      (digit_sum_le p n) (digit_sum_le p k)), Nat.sub_self (k + n), zero_add, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
rw :
  n + k - (p.digits (n + k)).sum - (k + (n + k - k - (p.digits (n + k - k)).sum) - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₁ :
  n + k - (p.digits (n + k)).sum - (k + (n - (p.digits n).sum) - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₂ :
  n + k - (p.digits (n + k)).sum - (k + n - (p.digits n).sum - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
⊢ n + k - (p.digits (n + k)).sum - (k - (p.digits k).sum + (n + k - k - (p.digits (n + k - k)).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
have rw₃ : n + k - (p.digits (n + k)).sum - (k + n - ((p.digits n).sum + (p.digits k).sum)) =
  (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Tactic: rw [← Nat.sub_add_comm <| digit_sum_le p k, Nat.add_sub_cancel n k, ← Nat.add_sub_assoc <|
      digit_sum_le p n, Nat.sub_sub (k + n), ← Nat.sub_right_comm, Nat.sub_sub, sub_add_eq,
      add_comm, tsub_tsub_assoc (Nat.le_refl (k + n)) <| (add_comm k n) ▸ (Nat.add_le_add
      (digit_sum_le p n) (digit_sum_le p k)), Nat.sub_self (k + n), zero_add, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
rw :
  n + k - (p.digits (n + k)).sum - (k + (n + k - k - (p.digits (n + k - k)).sum) - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₁ :
  n + k - (p.digits (n + k)).sum - (k + (n - (p.digits n).sum) - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₂ :
  n + k - (p.digits (n + k)).sum - (k + n - (p.digits n).sum - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₃ :
  n + k - (p.digits (n + k)).sum - (k + n - ((p.digits n).sum + (p.digits k).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
⊢ n + k - (p.digits (n + k)).sum - (k - (p.digits k).sum + (n + k - k - (p.digits (n + k - k)).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
have rw₄ : n + k - (k + n - ((p.digits n).sum + (p.digits k).sum)) - (p.digits (n + k)).sum =
  (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Tactic: rw [← Nat.sub_add_comm <| digit_sum_le p k, Nat.add_sub_cancel n k, ← Nat.add_sub_assoc <|
      digit_sum_le p n, Nat.sub_sub (k + n), ← Nat.sub_right_comm, Nat.sub_sub, sub_add_eq,
      add_comm, tsub_tsub_assoc (Nat.le_refl (k + n)) <| (add_comm k n) ▸ (Nat.add_le_add
      (digit_sum_le p n) (digit_sum_le p k)), Nat.sub_self (k + n), zero_add, add_comm]