awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
_ : 1 + padicValNat p k + p ≤ p + k
⊢ 1 + padicValNat p k + p ≤ p * k

Tactic:
calc
      _ ≤ p + k := by lia
      _ ≤ _ := Nat.add_le_mul hp.out.two_le (by lia)

Premises used: Nat.add_le_mul, Nat.Prime.two_le, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : ¬p ∣ a
neg : 0 + p ≤ a
⊢ padicValNat p a + p ≤ a

Tactic:
rw [padicValNat.eq_zero_of_not_dvd dvd]

Premises used: padicValNat.eq_zero_of_not_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : ¬p ∣ a
⊢ 0 + p ≤ a

Tactic:
lia
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ n ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
rw : n < p ^ (padicValNat p n + 1) → p ^ padicValNat p n ≤ n
⊢ log p n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1)

Tactic:
rw [Nat.log_eq_iff (Or.inr ⟨(Nat.Prime.one_lt' p).out, by lia⟩), and_iff_right_iff_imp]

Premises used: Nat.log_eq_iff, and_iff_right_iff_imp, And.intro, Or.inr, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ n < p ^ (padicValNat p n + 1) → p ^ padicValNat p n ≤ n

Tactic:
fun _ => Nat.le_of_dvd (Nat.pos_iff_ne_zero.mpr hn) pow_padicValNat_dvd

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, pow_padicValNat_dvd, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ n < p ^ (padicValNat p n + 1) → p ^ padicValNat p n ≤ n

Tactic:
exact fun _ => Nat.le_of_dvd (Nat.pos_iff_ne_zero.mpr hn) pow_padicValNat_dvd

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, pow_padicValNat_dvd, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n : ℕ
hn : n ≠ 0
⊢ padicValNat 2 (n + 1) ≠ 0 ∨ LT.lt (α := ℕ) 1 2 ∧ n ≠ 0

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n : ℕ
hn : n ≠ 0
rw : ¬(HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) ≤ n ∧ n < HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1) + 1))
⊢ log 2 n ≠ padicValNat 2 (n + 1)

Tactic:
rw [Ne, log_eq_iff (by simp [hn])]

Premises used: Nat.log_eq_iff, Ne
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n : ℕ
hn : n ≠ 0
h1 : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) ≤ n
h2 : n < HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1) + 1)
⊢ HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 1 < n + 1

Tactic:
rw [← Nat.lt_add_one_iff, ← mul_one (2 ^ _)] at h1

Premises used: Nat.lt_add_one_iff, HPow.hPow, mul_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n : ℕ
hn : n ≠ 0
h1 : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) ≤ n
h2 : n < HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1) + 1)
h1₁ : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 1 < n + 1
⊢ n < HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1) + 1)

Tactic:
rw [← Nat.lt_add_one_iff, ← mul_one (2 ^ _)] at h1

Premises used: Nat.lt_add_one_iff, HPow.hPow, mul_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n : ℕ
hn : n ≠ 0
h1 : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 1 < n + 1
h2 : n < HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1) + 1)
⊢ n + 1 ≤ HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 2

Tactic:
rw [← add_one_le_iff, Nat.pow_succ] at h2

Premises used: Nat.pow_succ, Nat.add_one_le_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n : ℕ
hn : n ≠ 0
h1 : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 1 < n + 1
h2 : n + 1 ≤ HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 2
⊢ False

Tactic:
not_dvd_of_lt_of_lt_mul_succ h1 (lt_of_le_of_ne' h2 ?_) pow_padicValNat_dvd

Premises used: Nat.not_dvd_of_lt_of_lt_mul_succ, pow_padicValNat_dvd, lt_of_le_of_ne'
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n : ℕ
hn : n ≠ 0
h1 : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 1 < n + 1
h2 : n + 1 ≤ HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 2
refine : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * HAdd.hAdd (α := ℕ) 1 1 ≠ n + 1
⊢ False

Tactic:
refine not_dvd_of_lt_of_lt_mul_succ h1 (lt_of_le_of_ne' h2 ?_) pow_padicValNat_dvd

Premises used: Nat.not_dvd_of_lt_of_lt_mul_succ, pow_padicValNat_dvd, lt_of_le_of_ne'
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n : ℕ
hn : n ≠ 0
h1 : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 1 < n + 1
h2 : n + 1 ≤ HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 2
⊢ HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * HAdd.hAdd (α := ℕ) 1 1 ≠ n + 1

Tactic:
pow_succ_padicValNat_not_dvd (p := 2) n.succ_ne_zero ∘ dvd_of_eq

Premises used: pow_succ_padicValNat_not_dvd, Function.comp, Nat.succ_ne_zero, dvd_of_eq, Not
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n : ℕ
hn : n ≠ 0
h1 : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 1 < n + 1
h2 : n + 1 ≤ HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 2
⊢ HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * HAdd.hAdd (α := ℕ) 1 1 ≠ n + 1

Tactic:
exact pow_succ_padicValNat_not_dvd (p := 2) n.succ_ne_zero ∘ dvd_of_eq

Premises used: pow_succ_padicValNat_not_dvd, Nat.succ_ne_zero, dvd_of_eq
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Prime p)
apply : log p (n + 1) ≤ max (log p n) (padicValNat p (n + 1))
⊢ max (log p n) (padicValNat p (n + 1)) = log p (n + 1)

Tactic:
apply le_antisymm (max_le (le_log_of_pow_le hp.out.one_lt (pow_log_le_add_one p n))
    (padicValNat_le_nat_log (n + 1)))

Premises used: Nat.Prime.one_lt, Nat.le_log_of_pow_le, le_antisymm, HAdd.hAdd, max_le, OfNat.ofNat, Fact.out, Nat.pow_log_le_add_one, padicValNat_le_nat_log
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Prime p)
rw : log p n < log p (n + 1) → log p (n + 1) ≤ padicValNat p (n + 1)
⊢ log p (n + 1) ≤ max (log p n) (padicValNat p (n + 1))

Tactic:
rw [le_max_iff, or_iff_not_imp_left, not_le]

Premises used: not_le, Classical.or_iff_not_imp_left, le_max_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Prime p)
h : log p n < log p (n + 1)
⊢ n + 1 = p ^ log p (n + 1)

Tactic:
replace h := le_antisymm (add_one_le_iff.mpr (lt_pow_of_log_lt hp.out.one_lt h))
    (pow_log_le_self p n.succ_ne_zero)
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Prime p)
h : n + 1 = p ^ log p (n + 1)
rw : log p (p ^ log p (n + 1)) ≤ padicValNat p (p ^ log p (n + 1))
rw₁ : log p (p ^ log p (n + 1)) ≤ log p (n + 1)
rw₂ rw₃ : log p (n + 1) ≤ log p (n + 1)
⊢ log p (n + 1) ≤ padicValNat p (n + 1)

Tactic:
rw [h, padicValNat.prime_pow, ← h]

Premises used: padicValNat.prime_pow
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : Membership.mem (γ := Finset ℕ) (Finset.image (fun (x : ℕ) ↦ p ^ x) (Finset.range (padicValNat p n + 1))) t
⊢ ∃ a < padicValNat p n + 1, p ^ a = t

Tactic:
simp only [Finset.mem_image, Finset.mem_range] at ht

Premises used: Finset.mem_image, Finset.mem_range
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : ∃ a < padicValNat p n + 1, p ^ a = t
obtain : ∀ (k : ℕ) (hk : k < padicValNat p n + 1), p ^ k ∈ n.divisors
⊢ t ∈ n.divisors

Tactic:
obtain ⟨k, hk, rfl⟩ := ht

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
rw : p ^ k ∣ n ∧ n ≠ 0
⊢ p ^ k ∈ n.divisors

Tactic:
rw [Nat.mem_divisors]

Premises used: Nat.mem_divisors
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ k ≤ padicValNat p n

Tactic:
lia
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∣ n ∧ n ≠ 0

Tactic:
exact ⟨(pow_dvd_pow p <| by lia).trans pow_padicValNat_dvd, hn⟩
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
inr : ∀ (hn : n ≠ 0), Finset.image (fun (t : ℕ) ↦ p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1
⊢ 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)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun (t : ℕ) ↦ p ^ (t + 1)) (Finset.range (padicValNat p 0)) ⊆ (divisors 0).erase 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
⊢ ∃ a < padicValNat p n, p ^ (a + 1) = t

Tactic:
simp only [Finset.mem_image, Finset.mem_range] at ht

Premises used: Finset.mem_image, Finset.mem_range
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : ∃ a < padicValNat p n, p ^ (a + 1) = t
inr : ∀ (k : ℕ) (hk : k < padicValNat p n), p ^ (k + 1) ∈ n.divisors.erase 1
⊢ t ∈ n.divisors.erase 1

Tactic:
obtain ⟨k, hk, rfl⟩ := ht

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
inr : p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∣ n ∧ n ≠ 0
⊢ p ^ (k + 1) ∈ n.divisors.erase 1

Tactic:
rw [Finset.mem_erase, Nat.mem_divisors]

Premises used: Nat.mem_divisors, Finset.mem_erase
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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

Tactic:
⟨?_, (pow_dvd_pow p <| succ_le_iff.2 hk).trans pow_padicValNat_dvd, hn⟩

Premises used: Iff.mpr, pow_dvd_pow, pow_padicValNat_dvd, And.intro, Nat.succ_le_iff, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
inr : p ^ (k + 1) ≠ 1
⊢ p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∣ n ∧ n ≠ 0

Tactic:
refine ⟨?_, (pow_dvd_pow p <| succ_le_iff.2 hk).trans pow_padicValNat_dvd, hn⟩
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1

Tactic:
(Nat.one_lt_pow k.succ_ne_zero hp.out.one_lt).ne'

Premises used: Nat.one_lt_pow, Nat.Prime.one_lt, LT.lt.ne', Nat.succ_ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1

Tactic:
exact (Nat.one_lt_pow k.succ_ne_zero hp.out.one_lt).ne'

Premises used: Nat.one_lt_pow, Nat.Prime.one_lt, LT.lt.ne', Nat.succ_ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
a : Eq (α := ℕ∞) (↑(padicValNat p (p * n)!) : ℕ∞) (↑(padicValNat p n ! + n) : ℕ∞)
⊢ padicValNat p (p * n)! = padicValNat p n ! + n

Tactic:
apply Nat.cast_injective (R := ℕ∞)

Premises used: Nat.cast_injective
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
a : emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)
⊢ Eq (α := ℕ∞) (↑(padicValNat p (p * n)!) : ℕ∞) (↑(padicValNat p n ! + n) : ℕ∞)

Tactic:
rw [padicValNat_eq_emultiplicity <| factorial_ne_zero (p * n), Nat.cast_add,
      padicValNat_eq_emultiplicity <| factorial_ne_zero n]

Premises used: HMul.hMul, Nat.cast_add, Nat.factorial_ne_zero, padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)

Tactic:
Prime.emultiplicity_factorial_mul hp.out

Premises used: Nat.Prime.emultiplicity_factorial_mul, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)

Tactic:
exact Prime.emultiplicity_factorial_mul hp.out

Premises used: Nat.Prime.emultiplicity_factorial_mul, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p m k : ℕ
hm : m ∈ Set.Ioo (p * k) (p * (k + 1))
⊢ padicValNat p m = 0

Tactic:
padicValNat.eq_zero_of_not_dvd <| not_dvd_of_lt_of_lt_mul_succ hm.1 hm.2

Premises used: Nat.not_dvd_of_lt_of_lt_mul_succ, And.right, And.left, padicValNat.eq_zero_of_not_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p m : ℕ
hp : Fact (Nat.Prime p)
h : 0 < p
zero zero₁ : padicValNat p (p * m)! = padicValNat p (p * m)!
⊢ padicValNat p (p * m + 0)! = padicValNat p (p * m)!

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)!
succ₆ succ₇ : padicValNat p (p * m)! = padicValNat p (p * m)!
⊢ padicValNat p (p * m + (n + 1))! = 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]

Premises used: HMul.hMul, Nat.factorial_succ, zero_add, Nat.lt_add_of_pos_right, Nat.factorial_ne_zero, Nat.succ_ne_zero, HAdd.hAdd, Nat.add_succ, Nat.succ_pos, padicValNat.mul, And.intro, Nat.lt_of_succ_lt, padicValNat_eq_zero_of_mem_Ioo
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)!
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)!
⊢ padicValNat p (p * m + n)! = 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]

Premises used: HMul.hMul, Nat.factorial_succ, zero_add, Nat.lt_add_of_pos_right, Nat.factorial_ne_zero, Nat.succ_ne_zero, HAdd.hAdd, Nat.add_succ, Nat.succ_pos, padicValNat.mul, And.intro, Nat.zero, Nat.lt_of_succ_lt, add_zero, padicValNat_eq_zero_of_mem_Ioo, Nat.succ
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
nth_rw : padicValNat p (p * (n / p))! = padicValNat p (p * (n / p) + n % p)!
⊢ padicValNat p (p * (n / p))! = padicValNat p n !

Tactic:
nth_rw 2 [← div_add_mod n p]

Premises used: Nat.div_add_mod
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * (n / p))! = padicValNat p (p * (n / p) + n % p)!

Tactic:
(padicValNat_factorial_mul_add (n / p) <| mod_lt n hp.out.pos).symm

Premises used: HDiv.hDiv, Nat.Prime.pos, Nat.mod_lt, padicValNat_factorial_mul_add, Eq.symm, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * (n / p))! = padicValNat p (p * (n / p) + n % p)!

Tactic:
exact (padicValNat_factorial_mul_add (n / p) <| mod_lt n hp.out.pos).symm

Premises used: HDiv.hDiv, Nat.Prime.pos, Nat.mod_lt, padicValNat_factorial_mul_add, Eq.symm, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n b : ℕ
hp : Fact (Nat.Prime p)
hnb : log p n < b
⊢ padicValNat p n ! = ∑ i ∈ Finset.Ico 1 b, n / p ^ i

Tactic:
exact_mod_cast ((padicValNat_eq_emultiplicity (p := p) <| factorial_ne_zero _) ▸
      Prime.emultiplicity_factorial hp.out hnb)
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : (p - 1) * ∑ i ∈ Finset.Ico 1 (log p n + 1).succ, n / p ^ i = n - (p.digits n).sum
⊢ (p - 1) * padicValNat p n ! = n - (p.digits n).sum

Tactic:
rw [padicValNat_factorial <| lt_succ_of_lt <| lt_add_one (log p n)]

Premises used: lt_add_one, padicValNat_factorial, Nat.lt_succ_of_lt, Nat.log
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
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
rw₄ rw₅ :
  (p - 1) * ∑ x ∈ Finset.range (log p n + 1), n / p ^ (x + 1) =
    (p - 1) * ∑ i ∈ Finset.range (log p n + 1), n / p ^ i.succ
⊢ (p - 1) * ∑ i ∈ Finset.Ico (HAdd.hAdd (α := ℕ) 0 1) (log p n + 1).succ, n / p ^ i = 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]

Premises used: Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, Nat.succ_eq_add_one, Finset.sum_Ico_add', Nat.Ico_zero_eq_range, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
rw : n - (p.digits n).sum < n
⊢ (p - 1) * padicValNat p n ! < n

Tactic:
rw [sub_one_mul_padicValNat_factorial n]

Premises used: sub_one_mul_padicValNat_factorial
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ n - (p.digits n).sum < n

Tactic:
Nat.sub_lt_self ?_ (digit_sum_le p n)

Premises used: Nat.sub_lt_self, Nat.digit_sum_le
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
refine : 0 < (p.digits n).sum
⊢ n - (p.digits n).sum < n

Tactic:
refine Nat.sub_lt_self ?_ (digit_sum_le p n)

Premises used: Nat.sub_lt_self, Nat.digit_sum_le
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ p.digits n ≠ []

Tactic:
have hnil : p.digits n ≠ [] := Nat.digits_ne_nil_iff_ne_zero.mpr hn
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
hnil : p.digits n ≠ []
⊢ 0 < (p.digits n).sum

Tactic:
List.sum_pos_iff_exists_pos_nat.mpr
    ⟨_, List.getLast_mem hnil, Nat.pos_of_ne_zero (Nat.getLast_digit_ne_zero p hn)⟩

Premises used: Iff.mpr, Nat.getLast_digit_ne_zero, Nat.pos_of_ne_zero, List.sum_pos_iff_exists_pos_nat, And.intro, List.getLast_mem, Exists.intro
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
hnil : p.digits n ≠ []
⊢ 0 < (p.digits n).sum

Tactic:
exact List.sum_pos_iff_exists_pos_nat.mpr
    ⟨_, List.getLast_mem hnil, Nat.pos_of_ne_zero (Nat.getLast_digit_ne_zero p hn)⟩

Premises used: Iff.mpr, Nat.getLast_digit_ne_zero, Nat.pos_of_ne_zero, List.sum_pos_iff_exists_pos_nat, And.intro, List.getLast_mem, Exists.intro
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
apply : padicValNat p n ! ≤ (p - 1) * padicValNat p n !
⊢ padicValNat p n ! < n

Tactic:
apply lt_of_le_of_lt _ (sub_one_mul_padicValNat_factorial_lt_of_ne_zero p hn)

Premises used: lt_of_le_of_lt, sub_one_mul_padicValNat_factorial_lt_of_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
rw : 1 * padicValNat p n !
| padicValNat p n !

Tactic:
rw [← one_mul (padicValNat p n !)]

Premises used: padicValNat, Nat.factorial, one_mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
conv_lhs : 1 * padicValNat p n ! ≤ (p - 1) * padicValNat p n !
⊢ padicValNat p n ! ≤ (p - 1) * padicValNat p n !

Tactic:
conv_lhs => rw [← one_mul (padicValNat p n !)]

Premises used: padicValNat, Nat.factorial, one_mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
bc : 1 ≤ p - 1
⊢ 1 * padicValNat p n ! ≤ (p - 1) * padicValNat p n !

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ p - 1

Tactic:
le_sub_one_of_lt (Nat.Prime.one_lt hp.elim)

Premises used: Nat.Prime.one_lt, Nat.le_sub_one_of_lt, Fact.elim
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ p - 1

Tactic:
exact le_sub_one_of_lt (Nat.Prime.one_lt hp.elim)

Premises used: Nat.Prime.one_lt, Nat.le_sub_one_of_lt, Fact.elim
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
pos : ∀ (hn : n = 0), padicValNat p n ! ≤ n
neg : ∀ (hn : ¬n = 0), padicValNat p n ! ≤ n
⊢ padicValNat p n ! ≤ n

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n = 0
⊢ padicValNat p n ! ≤ n

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : ¬n = 0
⊢ padicValNat p n ! ≤ n

Tactic:
le_of_lt (padicValNat_factorial_lt_of_ne_zero p hn)

Premises used: le_of_lt, padicValNat_factorial_lt_of_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : ¬n = 0
⊢ padicValNat p n ! ≤ n

Tactic:
exact le_of_lt (padicValNat_factorial_lt_of_ne_zero p hn)

Premises used: le_of_lt, padicValNat_factorial_lt_of_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n k b : ℕ
hp : Fact (Nat.Prime p)
hkn : k ≤ n
hnb : log p n < b
⊢ padicValNat p (n.choose k) = #({i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})

Tactic:
exact_mod_cast (padicValNat_eq_emultiplicity (p := p) <| (choose_ne_zero hkn)) ▸
    Prime.emultiplicity_choose hp.out hkn hnb
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n k b : ℕ
hp : Fact (Nat.Prime p)
hnb : log p (n + k) < b
⊢ padicValNat p ((n + k).choose k) = #({i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})

Tactic:
exact_mod_cast (padicValNat_eq_emultiplicity (p := p) <| choose_ne_zero <|
    Nat.le_add_left k n) ▸ Prime.emultiplicity_choose' hp.out hnb
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
⊢ k ≤ n + k

Tactic:
Nat.le_add_left k n

Premises used: Nat.le_add_left
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
⊢ k ≤ n + k

Tactic:
exact Nat.le_add_left k n

Premises used: Nat.le_add_left
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
⊢ k ≤ n + k

Tactic:
have h : k ≤ n + k := by exact Nat.le_add_left k n
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
simp :
  (p - 1) * padicValNat p ((n + k)! / (k ! * (n + k - k)!)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
⊢ (p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
simp only [Nat.choose_eq_factorial_div_factorial h]

Premises used: Nat.choose_eq_factorial_div_factorial