WithBot manipulation?

Stream: mathlib4

[Siddharth Bhat]

Not sure where I should ask this. Here's an MWE of something I'm trying to prove, I don't know how to get WitBot's arithmetic instances to play nice:

theorem withBotManipulation
  (H1 : (2 : WithBot ℕ) ^ 5 = some val)
  (H2 : val' < 2^5) : val' < val := by sorry

[Kevin Buzzard]

#mwe s contain all imports ;-)

[Kevin Buzzard]

import Mathlib.Tactic

theorem foo (H1 : (2 : WithBot ℕ) ^ 5 = some val) : val = 2 ^ 5 := by
  norm_cast at H1 -- this line not necessary but proof becomes unreadable without it
  cases H1
  simp

theorem withBotManipulation
    (H1 : (2 : WithBot ℕ) ^ 5 = some val)
    (H2 : val' < 2^5) : val' < val := by
  rw [foo H1]
  assumption

[Eric Wieser]

Which some is that?

[Siddharth Bhat]

Aha, super, norm_cast was indeed what I was looking for! Thanks @Kevin Buzzard !

[Eric Wieser]

It should be docs#WithBot.some, but I suspect it's actually Option.some

[Eric Wieser]

I just checked; it's the wrong some, and that's going to make proving things annoying