chore: remove no-longer-needed Nat.digits workarounds (#10429)

`norm_num` now successfully reduces `Nat.digits` calls that have concrete arguments, so we can clean up some old workarounds.

This all works because Lean 4.6.0 introduced "simprocs", including the default-enabled `reduceLE`, `reduceMod`, `reduceDiv`, etc. which `norm_num` can invoke to discharge the side-goals required by applications of `digits_of_two_le_of_pos`.

Another crucial aspect is that `{ decide := false }` is the default for `simp` (and `norm_num`) after #8366.  Otherwise,
the `Acc`-based recursion in `digitsAux` would bog down kernel reduction.

Archive/Imo/Imo1960Q1.lean

@@ -95,20 +95,15 @@ theorem right_direction {n : ℕ} : ProblemPredicate n → SolutionPredicate n :
   iterate 82
     replace :=
       searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num1; rfl)
-        (by -- This used to be just `norm_num`, but after leanprover/lean4#2790,
-            -- that triggers a max recursion depth exception. As a workaround, we
-            -- manually rewrite with `Nat.digits_of_two_le_of_pos` first.
-            rw [Nat.digits_of_two_le_of_pos (by norm_num) (by norm_num)]
-            norm_num <;> decide)
+        (by norm_num <;> decide)
   exact searchUpTo_end this
 #align imo1960_q1.right_direction Imo1960Q1.right_direction
 
 /-
 Now we just need to prove the equivalence, for the precise problem statement.
 -/
 theorem left_direction (n : ℕ) (spn : SolutionPredicate n) : ProblemPredicate n := by
-  -- Porting note: This is very slow
-  rcases spn with (rfl | rfl) <;> refine' ⟨_, by decide, _⟩ <;> rfl
+  rcases spn with (rfl | rfl) <;> refine' ⟨_, by decide, _⟩ <;> norm_num <;> rfl
 #align imo1960_q1.left_direction Imo1960Q1.left_direction
 
 end Imo1960Q1

Archive/Imo/Imo1962Q1.lean

@@ -130,17 +130,7 @@ Now we combine these cases to show that 153846 is the smallest solution.
 
 
 theorem satisfied_by_153846 : ProblemPredicate 153846 := by
-  -- This proof used to be the single line `norm_num [ProblemPredicate]`.
-  -- After leanprover/lean4#2790, that triggers a max recursion depth exception.
-  -- As a workaround, we manually apply `Nat.digits_of_two_le_of_pos` a few times
-  -- before invoking `norm_num`.
-  unfold ProblemPredicate
-  have two_le_ten : 2 ≤ 10 := by norm_num
-  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
-  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
-  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
-  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
-  norm_num
+  norm_num [ProblemPredicate]
   decide
 #align imo1962_q1.satisfied_by_153846 Imo1962Q1.satisfied_by_153846