linarith fails on ofDigits

Stream: mathlib4

[Bolton Bailey]

In this example, linarith fails:

import Mathlib

theorem extracted_1 :
    (Nat.ofDigits 2 []) ≤ 2 * (Nat.ofDigits 2 []) := by
  -- set s := ofDigits 2 [] -- works with this line
  linarith -- fails

I would expect both sides to process Nat.ofDigits 2 [] into an atom and solve the goal that way. Why does this not happen?

[Kyle Miller]

Looking at the output with set_option trace.linarith true, there's some process where the Nat.ofDigits are transformed into returning Int. Maybe something is going wrong after that?

In any case, omega can solve this.

[Bolton Bailey]

Interestingly, omega does not solve the issue this was minimized from.

[Bolton Bailey]

import Mathlib

open Nat

theorem extracted_1 :
    ofDigits 2 ([0]).reverse ≤ 2 * (ofDigits 2 ([0]).reverse + 2 ^ ([0]).length) := by
  omega --fails