Nat.cast to WithBot

Stream: mathlib4

[Johan Commelin]

From !4#2631:

-- Porting note: In Lean3, these are same `coe`, but not in Lean4.
private theorem _root_.WithBot.some_eq_nat_cast : WithBot.some n = Nat.cast n := rfl

Is there a std way to fix this?

[Johan Commelin]

Apparently this already exists as

theorem Nat.cast_withBot (n : ℕ) : Nat.cast n = WithBot.some n := rfl

but that doesn't solve the coe issue

[Eric Wieser]

I think the comment is slightly misleading. In lean 3 it was @coe _ _ inst1 n = @coe _ _ inst2 n which had the same head symbol and explicit arguments (which is enough for simp and rw to not know the difference), but in lean4 the head symbols are no longer the same

[Eric Wieser]

I think this behavior is by design, as part of the "coe instances are inlined" behavior

[Eric Wieser]

If we want all casts to have the same head symbol as they did in lean3, that amounts to either reverting that design decision in lean4, or hacking around it in mathlib4/std4 to pretend the decision was never made (i.e by adding a global Std.coe function and using it in all instances).

[Gabriel Ebner]

IIUI the issue here is that we've got two coercions ℕ → WithBot ℕ, right? There's Nat.cast if you coerce to WithBot ℕ directly, and WithBot.coe if you coerce to WithBot α and then substitute α by ℕ later.

[Gabriel Ebner]

My suggestion for !4#2631 would be to just use the Nat.cast API here.

rw [← Nat.cast_le, ← degree_eq_natDegree]