manual fix

Author: kim-em

Mathlib/Data/Nat/Multiplicity.lean

@@ -117,7 +117,7 @@ theorem sub_one_mul_multiplicity_factorial {n p : ℕ} (hp : p.Prime) :
     (p - 1) * multiplicity p n ! =
     n - (p.digits n).sum := by
   simp only [multiplicity_eq_of_emultiplicity_eq_some <|
-      emultiplicity_factorial hp <| lt_succ_of_lt <| lt_add_one (log p n),
+      emultiplicity_factorial hp <| lt_succ_of_lt <| Nat.lt_add_one (log p n),
     ← Finset.sum_Ico_add' _ 0 _ 1, Ico_zero_eq_range, ←
     sub_one_mul_sum_log_div_pow_eq_sub_sum_digits]