awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : Ne (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x) ⊤
rw : ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x = emultiplicity p (n + 1) + 1
rw₁ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + emultiplicity p (p * (n + 1)) = emultiplicity p (n + 1) + 1
rw₂ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (emultiplicity p p + emultiplicity p (n + 1)) =
    emultiplicity p (n + 1) + 1
⊢ HAdd.hAdd (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x)
      (∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x) =
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)
have rw₃ : ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
Tactic: rw [WithTop.add_left_inj h, sum_Ico_succ_top h2, hp.emultiplicity_mul, hp.emultiplicity_self,
    sum_congr rfl h4, sum_const_zero, zero_add, add_comm 1]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : Ne (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x) ⊤
rw : ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x = emultiplicity p (n + 1) + 1
rw₁ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + emultiplicity p (p * (n + 1)) = emultiplicity p (n + 1) + 1
rw₂ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (emultiplicity p p + emultiplicity p (n + 1)) =
    emultiplicity p (n + 1) + 1
rw₃ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
⊢ HAdd.hAdd (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x)
      (∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x) =
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)
have rw₄ : ∑ x ∈ Ico (p * n + 1) (p * (n + 1)), 0 + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
Tactic: rw [WithTop.add_left_inj h, sum_Ico_succ_top h2, hp.emultiplicity_mul, hp.emultiplicity_self,
    sum_congr rfl h4, sum_const_zero, zero_add, add_comm 1]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : Ne (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x) ⊤
rw : ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x = emultiplicity p (n + 1) + 1
rw₁ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + emultiplicity p (p * (n + 1)) = emultiplicity p (n + 1) + 1
rw₂ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (emultiplicity p p + emultiplicity p (n + 1)) =
    emultiplicity p (n + 1) + 1
rw₃ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
rw₄ : ∑ x ∈ Ico (p * n + 1) (p * (n + 1)), 0 + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
⊢ HAdd.hAdd (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x)
      (∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x) =
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)
have rw₅ : 0 + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
Tactic: rw [WithTop.add_left_inj h, sum_Ico_succ_top h2, hp.emultiplicity_mul, hp.emultiplicity_self,
    sum_congr rfl h4, sum_const_zero, zero_add, add_comm 1]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : Ne (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x) ⊤
rw : ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x = emultiplicity p (n + 1) + 1
rw₁ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + emultiplicity p (p * (n + 1)) = emultiplicity p (n + 1) + 1
rw₂ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (emultiplicity p p + emultiplicity p (n + 1)) =
    emultiplicity p (n + 1) + 1
rw₃ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
rw₄ : ∑ x ∈ Ico (p * n + 1) (p * (n + 1)), 0 + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
rw₅ : 0 + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
⊢ HAdd.hAdd (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x)
      (∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x) =
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)
have rw₆ : 1 + emultiplicity p (n + 1) = emultiplicity p (n + 1) + 1
Tactic: rw [WithTop.add_left_inj h, sum_Ico_succ_top h2, hp.emultiplicity_mul, hp.emultiplicity_self,
    sum_congr rfl h4, sum_const_zero, zero_add, add_comm 1]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : Ne (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x) ⊤
rw : ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x = emultiplicity p (n + 1) + 1
rw₁ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + emultiplicity p (p * (n + 1)) = emultiplicity p (n + 1) + 1
rw₂ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (emultiplicity p p + emultiplicity p (n + 1)) =
    emultiplicity p (n + 1) + 1
rw₃ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
rw₄ : ∑ x ∈ Ico (p * n + 1) (p * (n + 1)), 0 + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
rw₅ : 0 + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
rw₆ : 1 + emultiplicity p (n + 1) = emultiplicity p (n + 1) + 1
⊢ HAdd.hAdd (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x)
      (∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x) =
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)
have rw₇ : emultiplicity p (n + 1) + 1 = emultiplicity p (n + 1) + 1
Tactic: rw [WithTop.add_left_inj h, sum_Ico_succ_top h2, hp.emultiplicity_mul, hp.emultiplicity_self,
    sum_congr rfl h4, sum_const_zero, zero_add, add_comm 1]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (n + 1)! + (↑(n + 1) : ℕ∞)
have succ : emultiplicity p n ! + (↑n : ℕ∞) + emultiplicity p (n + 1) + 1 =
  emultiplicity p (n + 1) + emultiplicity p n ! + (↑n : ℕ∞) + 1
Tactic: simp only [hp, emultiplicity_factorial_mul_succ, ih, factorial_succ, emultiplicity_mul,
      cast_add, cast_one, ← add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)
⊢ emultiplicity p n ! + (↑n : ℕ∞) + emultiplicity p (n + 1) + 1 =
    emultiplicity p (n + 1) + emultiplicity p n ! + (↑n : ℕ∞) + 1
have succ : emultiplicity p n ! + (↑n : ℕ∞) + emultiplicity p (n + 1) = emultiplicity p (n + 1) + emultiplicity p n ! + (↑n : ℕ∞)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)
⊢ emultiplicity p n ! + (↑n : ℕ∞) + emultiplicity p (n + 1) = emultiplicity p (n + 1) + emultiplicity p n ! + (↑n : ℕ∞)
have succ : emultiplicity p (n + 1) + (emultiplicity p n ! + (↑n : ℕ∞)) = emultiplicity p (n + 1) + emultiplicity p n ! + (↑n : ℕ∞)
Tactic: rw [add_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)
succ :
  emultiplicity p (n + 1) + (emultiplicity p n ! + (↑n : ℕ∞)) =
    emultiplicity p (n + 1) + emultiplicity p n ! + (↑n : ℕ∞)
⊢ emultiplicity p n ! + (↑n : ℕ∞) + emultiplicity p (n + 1) = emultiplicity p (n + 1) + emultiplicity p n ! + (↑n : ℕ∞)
have succ₁ : emultiplicity p (n + 1) + (emultiplicity p n ! + (↑n : ℕ∞)) =
  emultiplicity p (n + 1) + (emultiplicity p n ! + (↑n : ℕ∞))
Tactic: rw [add_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
n p : ℕ
hp : Prime p
⊢ emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)
have zero : emultiplicity p (p * 0)! = emultiplicity p 0! + (↑0 : ℕ∞)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    simp only [hp, emultiplicity_factorial_mul_succ, ih, factorial_succ, emultiplicity_mul,
      cast_add, cast_one, ← add_assoc]
    congr 1
    rw [add_comm, add_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
n p : ℕ
hp : Prime p
zero : emultiplicity p (p * 0)! = emultiplicity p 0! + (↑0 : ℕ∞)
⊢ emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)
have succ : ∀ (n : ℕ) (ih : emultiplicity p (p * n)! = emultiplicity p n ! + (↑n : ℕ∞)),
  emultiplicity p (p * (n + 1))! = emultiplicity p (n + 1)! + (↑(n + 1) : ℕ∞)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    simp only [hp, emultiplicity_factorial_mul_succ, ih, factorial_succ, emultiplicity_mul,
      cast_add, cast_one, ← add_assoc]
    congr 1
    rw [add_comm, add_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
n p : ℕ
hp : Prime p
⊢ multiplicity p (p ^ n)! = ∑ i ∈ range n, p ^ i
have rw : emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)
Tactic: rw [← ENat.coe_inj, ← (Nat.finiteMultiplicity_iff.2
      ⟨hp.ne_one, (p ^ n).factorial_pos⟩).emultiplicity_eq_multiplicity]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
h : emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)
⊢ emultiplicity p (p ^ (n + 1))! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
have succ : emultiplicity p (p * p ^ n)! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
Tactic: rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.coe_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
h : emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)
succ : emultiplicity p (p * p ^ n)! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
⊢ emultiplicity p (p ^ (n + 1))! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
have succ₁ : emultiplicity p (p ^ n)! + (↑(p ^ n) : ℕ∞) = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
Tactic: rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.coe_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
h : emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)
succ : emultiplicity p (p * p ^ n)! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
succ₁ : emultiplicity p (p ^ n)! + (↑(p ^ n) : ℕ∞) = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
⊢ emultiplicity p (p ^ (n + 1))! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
have succ₂ : HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ range n, p ^ i) : ℕ∞) (↑(p ^ n) : ℕ∞) = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
Tactic: rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.coe_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
h : emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)
succ : emultiplicity p (p * p ^ n)! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
succ₁ : emultiplicity p (p ^ n)! + (↑(p ^ n) : ℕ∞) = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
succ₂ : HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ range n, p ^ i) : ℕ∞) (↑(p ^ n) : ℕ∞) = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
⊢ emultiplicity p (p ^ (n + 1))! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
have succ₃ : HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ range n, p ^ i) : ℕ∞) (↑(p ^ n) : ℕ∞) = (↑(∑ x ∈ range n, p ^ x + p ^ n) : ℕ∞)
Tactic: rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.coe_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
h : emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)
succ : emultiplicity p (p * p ^ n)! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
succ₁ : emultiplicity p (p ^ n)! + (↑(p ^ n) : ℕ∞) = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
succ₂ : HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ range n, p ^ i) : ℕ∞) (↑(p ^ n) : ℕ∞) = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
succ₃ : HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ range n, p ^ i) : ℕ∞) (↑(p ^ n) : ℕ∞) = (↑(∑ x ∈ range n, p ^ x + p ^ n) : ℕ∞)
⊢ emultiplicity p (p ^ (n + 1))! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
have succ₄ : HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ range n, p ^ i) : ℕ∞) (↑(p ^ n) : ℕ∞) =
  HAdd.hAdd (α := ℕ∞) (↑(∑ x ∈ range n, p ^ x) : ℕ∞) (↑(p ^ n) : ℕ∞)
Tactic: rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.coe_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
n p : ℕ
hp : Prime p
⊢ emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)
have zero : emultiplicity p (HPow.hPow (β := ℕ) p 0)! = (↑(∑ i ∈ range 0, p ^ i) : ℕ∞)
Tactic: induction n with
  | zero => simp [hp.emultiplicity_one]
  | succ n h =>
    rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.coe_add]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
n p : ℕ
hp : Prime p
zero : emultiplicity p (HPow.hPow (β := ℕ) p 0)! = (↑(∑ i ∈ range 0, p ^ i) : ℕ∞)
⊢ emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)
have succ : ∀ (n : ℕ) (h : emultiplicity p (p ^ n)! = (↑(∑ i ∈ range n, p ^ i) : ℕ∞)),
  emultiplicity p (p ^ (n + 1))! = (↑(∑ i ∈ range (n + 1), p ^ i) : ℕ∞)
Tactic: induction n with
  | zero => simp [hp.emultiplicity_one]
  | succ n h =>
    rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.coe_add]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p n r b : ℕ
hp : Prime p
hbn : log p n < b
⊢ p ^ r ∣ n ! ↔ r ≤ ∑ i ∈ Ico 1 b, n / p ^ i
have rw : p ^ r ∣ n ! ↔ (↑r : WithTop ℕ) ≤ (↑(∑ i ∈ Ico 1 b, n / p ^ i) : WithTop ℕ)
Tactic: rw [← WithTop.coe_le_coe, ENat.some_eq_coe, ← hp.emultiplicity_factorial hbn,
    pow_dvd_iff_le_emultiplicity]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p n r b : ℕ
hp : Prime p
hbn : log p n < b
rw : p ^ r ∣ n ! ↔ (↑r : WithTop ℕ) ≤ (↑(∑ i ∈ Ico 1 b, n / p ^ i) : WithTop ℕ)
⊢ p ^ r ∣ n ! ↔ r ≤ ∑ i ∈ Ico 1 b, n / p ^ i
have rw₁ : p ^ r ∣ n ! ↔ LE.le (α := WithTop ℕ) (↑r : WithTop ℕ) (↑(∑ i ∈ Ico 1 b, n / p ^ i) : WithTop ℕ)
Tactic: rw [← WithTop.coe_le_coe, ENat.some_eq_coe, ← hp.emultiplicity_factorial hbn,
    pow_dvd_iff_le_emultiplicity]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p n r b : ℕ
hp : Prime p
hbn : log p n < b
rw : p ^ r ∣ n ! ↔ (↑r : WithTop ℕ) ≤ (↑(∑ i ∈ Ico 1 b, n / p ^ i) : WithTop ℕ)
rw₁ : p ^ r ∣ n ! ↔ LE.le (α := WithTop ℕ) (↑r : WithTop ℕ) (↑(∑ i ∈ Ico 1 b, n / p ^ i) : WithTop ℕ)
⊢ p ^ r ∣ n ! ↔ r ≤ ∑ i ∈ Ico 1 b, n / p ^ i
have rw₂ : p ^ r ∣ n ! ↔ (↑r : WithTop ℕ) ≤ emultiplicity p n !
Tactic: rw [← WithTop.coe_le_coe, ENat.some_eq_coe, ← hp.emultiplicity_factorial hbn,
    pow_dvd_iff_le_emultiplicity]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p n r b : ℕ
hp : Prime p
hbn : log p n < b
rw : p ^ r ∣ n ! ↔ (↑r : WithTop ℕ) ≤ (↑(∑ i ∈ Ico 1 b, n / p ^ i) : WithTop ℕ)
rw₁ : p ^ r ∣ n ! ↔ LE.le (α := WithTop ℕ) (↑r : WithTop ℕ) (↑(∑ i ∈ Ico 1 b, n / p ^ i) : WithTop ℕ)
rw₂ : p ^ r ∣ n ! ↔ (↑r : WithTop ℕ) ≤ emultiplicity p n !
⊢ p ^ r ∣ n ! ↔ r ≤ ∑ i ∈ Ico 1 b, n / p ^ i
have rw₃ : (↑r : ℕ∞) ≤ emultiplicity p n ! ↔ (↑r : WithTop ℕ) ≤ emultiplicity p n !
Tactic: rw [← WithTop.coe_le_coe, ENat.some_eq_coe, ← hp.emultiplicity_factorial hbn,
    pow_dvd_iff_le_emultiplicity]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ emultiplicity p n ! ≤ (↑(n / (p - 1)) : ℕ∞)
have rw : LE.le (α := ℕ∞) (↑(∑ i ∈ Ico 1 (log p n).succ, n / p ^ i) : ℕ∞) (↑(n / (p - 1)) : ℕ∞)
Tactic: rw [hp.emultiplicity_factorial (lt_succ_self _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ LE.le (α := ℕ∞) (↑(∑ i ∈ Ico 1 (log p n).succ, n / p ^ i) : ℕ∞) (↑(n / (p - 1)) : ℕ∞)
have a : ∑ i ∈ Ico 1 (log p n).succ, n / p ^ i ≤ n / (p - 1)
Tactic: apply WithTop.coe_mono
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
have rw : emultiplicity p ((n + k).choose k * k ! * n !) =
  (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
Tactic: rw [← hp.emultiplicity_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k * k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
have this : (n + k).choose k * k ! * n ! = (n + k)!
Tactic: have := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ emultiplicity p ((n + k).choose k * k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
have rw : (↑(HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 1 b, k / p ^ i) (∑ i ∈ Ico 1 b, (n + k - k) / p ^ i) +
        #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n + k - k) % p ^ i})) :
    ℕ∞) =
  (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) +
    HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ Ico 1 b, k / p ^ i) : ℕ∞) (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞)
Tactic: rw [this, hp.emultiplicity_factorial hnb, hp.emultiplicity_mul,
      hp.emultiplicity_factorial ((log_mono_right (le_add_left k n)).trans_lt hnb),
      hp.emultiplicity_factorial ((log_mono_right (le_add_left n k)).trans_lt
      (add_comm n k ▸ hnb)), multiplicity_choose_aux hp (le_add_left k n)]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k) = (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞)
have h₁ : emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
  (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
Tactic: have h₁ :
      emultiplicity p (choose (n + k) k) + emultiplicity p (k ! * n !) =
        #{i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i} + emultiplicity p (k ! * n !) := by
    rw [← hp.emultiplicity_mul, ← mul_assoc]
    have := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)
    rw [this, hp.emultiplicity_factorial hnb, hp.emultiplicity_mul,
      hp.emultiplicity_factorial ((log_mono_right (le_add_left k n)).trans_lt hnb),
      hp.emultiplicity_factorial ((log_mono_right (le_add_left n k)).trans_lt
      (add_comm n k ▸ hnb)), multiplicity_choose_aux hp (le_add_left k n)]
    simp [add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
⊢ emultiplicity p ((n + k).choose k) = (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞)
have refine : emultiplicity p (k ! * n !) ≠ ⊤
Tactic: refine WithTop.add_right_cancel ?_ h₁
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) : ℕ∞) + emultiplicity p (k ! * n !)
⊢ emultiplicity p (k ! * n !) ≠ ⊤
have apply : FiniteMultiplicity p (k ! * n !)
Tactic: apply finiteMultiplicity_iff_emultiplicity_ne_top.1
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
Goal:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ emultiplicity p (n.choose k) = (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})) : ℕ∞)
have this : n - k + k = n
Tactic: have := Nat.sub_add_cancel hkn
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ emultiplicity p (n.choose k) = (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})) : ℕ∞)
have h : n = n - k + k
Tactic: convert! @emultiplicity_choose' p (n - k) k b hp _
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
h : n = n - k + k
⊢ emultiplicity p (n.choose k) = (↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})) : ℕ∞)
have convert! : log p (n - k + k) < b
Tactic: convert! @emultiplicity_choose' p (n - k) k b hp _
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ n = n - k + k
have h : n = n
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n k : ℕ
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1)) + emultiplicity p (k + 1)
have rw : emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1) * (k + 1))
Tactic: rw [← hp.emultiplicity_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n k : ℕ
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1) * (k + 1))
have refine : n + 1 ∣ (n + 1).choose (k + 1) * (k + 1)
Tactic: refine emultiplicity_le_emultiplicity_of_dvd_right ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ (n + 1).choose (k + 1) * (k + 1)
have rw : n + 1 ∣ (n + 1) * n.choose k
Tactic: rw [← add_one_mul_choose_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) + emultiplicity p k ≤ (↑n : ℕ∞)
have hdisj : Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
Tactic: have hdisj :
        Disjoint {i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}
          {i ∈ Ico 1 n.succ | p ^ i ∣ k} := by
        simp +contextual [disjoint_right, *, dvd_iff_mod_eq_zero,
          Nat.mod_lt _ (pow_pos hp.pos _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ emultiplicity p ((p ^ n).choose k) + emultiplicity p k ≤ (↑n : ℕ∞)
have rw : LE.le (α := ℕ∞)
  (↑(#({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) +
        #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ∣ k})) :
    ℕ∞)
  (↑n : ℕ∞)
Tactic: rw [emultiplicity_choose hp hkn (lt_succ_self _),
        emultiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0.bot_lt
          (lt_succ_of_le (log_mono_right hkn)),
        ← Nat.cast_add]