case zero
p : ℕ
hp : Prime p
⊢ multiplicity p (p * zero)! = multiplicity p zero ! + ↑zero

case succ
p : ℕ
hp : Prime p
n : ℕ
ih : multiplicity p (p * n)! = multiplicity p n ! + ↑n
⊢ multiplicity p (p * succ n)! = multiplicity p (succ n)! + ↑(succ n)
n p : ℕ
hp : Prime p
⊢ multiplicity p (p * n)! = multiplicity p n ! + ↑n
induction' n with n ih
no goals
case zero
p : ℕ
hp : Prime p
⊢ multiplicity p (p * zero)! = multiplicity p zero ! + ↑zero
simp
case succ
p : ℕ
hp : Prime p
n : ℕ
ih : multiplicity p (p * n)! = multiplicity p n ! + ↑n
⊢ multiplicity p n ! + ↑n + multiplicity p (n + 1) + 1 = multiplicity p (n + 1) + multiplicity p n ! + ↑n + 1
case succ
p : ℕ
hp : Prime p
n : ℕ
ih : multiplicity p (p * n)! = multiplicity p n ! + ↑n
⊢ multiplicity p (p * succ n)! = multiplicity p (succ n)! + ↑(succ n)
simp only [succ_eq_add_one, multiplicity.mul, hp, hp.prime, ih, multiplicity_factorial_mul_succ,
  ← add_assoc, Nat.cast_one, Nat.cast_add, factorial_succ]
case succ.e_a
p : ℕ
hp : Prime p
n : ℕ
ih : multiplicity p (p * n)! = multiplicity p n ! + ↑n
⊢ multiplicity p n ! + ↑n + multiplicity p (n + 1) = multiplicity p (n + 1) + multiplicity p n ! + ↑n
case succ
p : ℕ
hp : Prime p
n : ℕ
ih : multiplicity p (p * n)! = multiplicity p n ! + ↑n
⊢ multiplicity p n ! + ↑n + multiplicity p (n + 1) + 1 = multiplicity p (n + 1) + multiplicity p n ! + ↑n + 1
congr 1
no goals
case succ.e_a
p : ℕ
hp : Prime p
n : ℕ
ih : multiplicity p (p * n)! = multiplicity p n ! + ↑n
⊢ multiplicity p n ! + ↑n + multiplicity p (n + 1) = multiplicity p (n + 1) + multiplicity p n ! + ↑n
rw [add_comm, add_assoc]