suggestion to enhance error message (calc failed)

Stream: new members

[rzeta0]

Earlier I got the following error message:

'calc' tactic failed, has type
  3 ^ (k + 1) ≥ 2 ^ (k + 1) + 100
but it is expected to have type
  3 ^ (k + 1) ≥ 2 ^ (k + 1) + 100

This was puzzling until I later found the 3 needed to be `(3:ℤ).

Could the error message be enhanced?

---

The source was an MoP exercise which I'll include as a spoiler :

example : forall_sufficiently_large n : ℕ, (3:ℤ) ^ n ≥ 2 ^ n + 100 := by
dsimp
use 5
intro n hn
induction_from_starting_point n, hn with k hk IH
· -- base case
norm_num
· -- inductive step
calc
(3:ℤ) ^(k + 1) = 3 * (3^k) := by ring -- < -- needed to be (3:ℤ), was just 3 based on inforview goal
_ ≥ 3 * (2^k + 100) := by rel [IH]
_ = 2^(k+1) + 2^k + 100 + 200 := by ring
_ ≥ 2^(k+1) + 2^k + 100 := by extra
_ ≥ 2^(k+1) + 100 := by extra

[Eric Wieser]

set_option pp.numeralTypes true or similar would help here

[Jason Rute]

Yeah, maybe there needs to be a way to take two different types and pretty print them in a way where they are different, or to underline the differing terms. (Maybe with definitional equality this would be challenging to do reliably.)

[Eric Wieser]

There is already (underused) infrastructure for red/green diffs