n p : ℕ
hp : Prime p
hp' : _root_.Prime p
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
n p : ℕ
hp : Prime p
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
have hp' := hp.prime
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
have h0 : 2 ≤ p := hp.two_le
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
have h1 : 1 ≤ p * n + 1 := Nat.le_add_left _ _
case h2
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ p * n + 1 ≤ p * (n + 1)

n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
have h2 : p * n + 1 ≤ p * (n + 1)
case h3
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ p * n + 1 ≤ p * (n + 1) + 1

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
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
have h3 : p * n + 1 ≤ p * (n + 1) + 1
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
hm : multiplicity p (p * n)! ≠ ⊤
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
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
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
have hm : multiplicity p (p * n)! ≠ ⊤ := by
  rw [Ne.def, eq_top_iff_not_finite, Classical.not_not, finite_nat_iff]
  exact ⟨hp.ne_one, factorial_pos _⟩
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
⊢ multiplicity p (p * n)! ≠ ⊤ → multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
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
hm : multiplicity p (p * n)! ≠ ⊤
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
revert hm
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 : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
⊢ multiplicity p (p * n)! ≠ ⊤ → multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
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
⊢ multiplicity p (p * n)! ≠ ⊤ → multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
have h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), multiplicity p m = 0 := by
  intro m hm
  rw [multiplicity_eq_zero, ← not_dvd_iff_between_consec_multiples _ hp.pos]
  rw [mem_Ico] at hm
  exact ⟨n, lt_of_succ_le hm.1, hm.2⟩
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 : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
⊢ ∑ x in Ico 1 (p * n + 1), multiplicity p x ≠ ⊤ →
    ∑ x in Ico 1 (p * n + 1), multiplicity p x + ∑ x in Ico (p * n + 1) (p * (n + 1) + 1), multiplicity p x =
      ∑ x in Ico 1 (p * n + 1), multiplicity p x + (multiplicity p (n + 1) + 1)
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 : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
⊢ multiplicity p (p * n)! ≠ ⊤ → multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
simp_rw [← prod_Ico_id_eq_factorial, multiplicity.Finset.prod hp', ← sum_Ico_consecutive _ h1 h3,
  add_assoc]
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 : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
h : ∑ x in Ico 1 (p * n + 1), multiplicity p x ≠ ⊤
⊢ ∑ x in Ico 1 (p * n + 1), multiplicity p x + ∑ x in Ico (p * n + 1) (p * (n + 1) + 1), multiplicity p x =
    ∑ x in Ico 1 (p * n + 1), multiplicity p x + (multiplicity p (n + 1) + 1)
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 : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
⊢ ∑ x in Ico 1 (p * n + 1), multiplicity p x ≠ ⊤ →
    ∑ x in Ico 1 (p * n + 1), multiplicity p x + ∑ x in Ico (p * n + 1) (p * (n + 1) + 1), multiplicity p x =
      ∑ x in Ico 1 (p * n + 1), multiplicity p x + (multiplicity p (n + 1) + 1)
intro h
no goals
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 : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
h : ∑ x in Ico 1 (p * n + 1), multiplicity p x ≠ ⊤
⊢ ∑ x in Ico 1 (p * n + 1), multiplicity p x + ∑ x in Ico (p * n + 1) (p * (n + 1) + 1), multiplicity p x =
    ∑ x in Ico 1 (p * n + 1), multiplicity p x + (multiplicity p (n + 1) + 1)
rw [PartENat.add_left_cancel_iff h, sum_Ico_succ_top h2, multiplicity.mul hp',
  hp.multiplicity_self, sum_congr rfl h4, sum_const_zero, zero_add, add_comm (1 : PartENat)]
no goals
case h2
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ p * n + 1 ≤ p * (n + 1)
linarith
no goals
case h3
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ p * n + 1 ≤ p * (n + 1) + 1
linarith
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
⊢ p ≠ 1 ∧ 0 < (p * n)!
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
⊢ multiplicity p (p * n)! ≠ ⊤
rw [Ne.def, eq_top_iff_not_finite, Classical.not_not, finite_nat_iff]
no goals
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
⊢ p ≠ 1 ∧ 0 < (p * n)!
exact ⟨hp.ne_one, factorial_pos _⟩
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
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ multiplicity p m = 0
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
⊢ ∀ (m : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
intro m hm
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
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ ∃ k, p * k < m ∧ m < p * (k + 1)
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
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ multiplicity p m = 0
rw [multiplicity_eq_zero, ← not_dvd_iff_between_consec_multiples _ hp.pos]
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
m : ℕ
hm : p * n + 1 ≤ m ∧ m < p * (n + 1)
⊢ ∃ k, p * k < m ∧ m < p * (k + 1)
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
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ ∃ k, p * k < m ∧ m < p * (k + 1)
rw [mem_Ico] at hm
no goals
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
m : ℕ
hm : p * n + 1 ≤ m ∧ m < p * (n + 1)
⊢ ∃ k, p * k < m ∧ m < p * (k + 1)
exact ⟨n, lt_of_succ_le hm.1, hm.2⟩