import mathlib breaks existing proofs

Stream: lean4

[Jonathan Protzenko]

I have the following definition (simplified):

def USize.checked_rem (n: USize) (m: USize): Option USize :=
  if h: m > 0 then
    .some ⟨ n.val % m.val, by
      have h1: m.val < USize.size := m.val.isLt
      have h2: n.val.val % m.val.val < m.val.val := @Nat.mod_lt n.val m.val h
      apply Nat.lt_trans h2 h1
    ⟩
  else
    .none

works fine, except if I add import Mathlib at the top of my file, my proof no longer works, and I get:

type mismatch
  m.val.isLt
has type
  ↑m.val < size : Prop
but is expected to have type
  m.val < ↑size : Prop

is there any advice on how to debug this? the reason for importing mathlib was to get the benefits of linarith

[Mario Carneiro]

you should mouseover the up arrows to see what the types are

[Eric Wieser]

I think the problem is that m.val < USize.size is not well-typed, so Lean tried inserting a coercion first on the right, and if that failed, on the left

[Jonathan Protzenko]

ok, there was an implicit .val that Lean was adding

[Jonathan Protzenko]

and somehow, import Mathlib made it fail... the fix was to write instead have h1: m.val.val

[Jonathan Protzenko]

(and leave the rest unchanged)

[Eric Wieser]

If you have mathlib imported, there is a coercion from Nat to Fin n that lean picks before it tries the coercion from Fin n to Nat

[Jonathan Protzenko]

ah! that explains a lot... thanks so much

[Eric Wieser]

have h1: ↑m.val < USize.size := m.val.isLt or even have h1 := m.val.isLt would be nicer than .val.val

[Jonathan Protzenko]

I'm not familiar with the \uparrow notation... need to read about it!

[Jonathan Protzenko]

ok that's a nice notation for coercions... and indeed it makes things more pleasant. thanks!