Lean 3 bug: infer type failed, unknown variable

Stream: general

[Matt Diamond]

I'm not sure if there's any interest in a Lean 3 bug report or if the community has moved on and no longer maintains it, but here's a minimal example to reproduce an issue I encountered:

Lean 3 playground link

import order.filter.at_top_bot

open filter

example (s : set (ℕ → ℕ)) (hs : s.countable)
  : 0 ≤ᶠ[at_top] nat.succ :=
begin
  rw set.countable_iff_exists_injective at hs,
  rw [eventually_le, eventually_at_top], -- fails
end

example (s : set (ℕ → ℕ)) (hs : s.countable)
  : 0 ≤ᶠ[at_top] nat.succ :=
begin
  rw [eventually_le, eventually_at_top], -- does not fail
end

[Ruben Van de Velde]

I'm afraid lean 3 is very much unmaintained at this point

[Matt Diamond]

Ah okay, I thought that might be the case.

[Matt Diamond]

I did try to see if I could reproduce it in Lean 4, but oddly the rewrite doesn't even work at all due to failing to find an instance of the pattern. Not exactly a bug, but kind of weird that it fails to rewrite when Lean 3 is able to rewrite:

import Mathlib.Order.Filter.AtTopBot

open Filter

example (s : Set (ℕ → ℕ)) (hs : s.Countable)
  : 0 ≤ᶠ[at_top] Nat.succ :=
by
  rw [EventuallyLE, eventually_atTop]

[Eric Rodriguez]

the filter is called atTop in mathlib4 and that's your issue

[Matt Diamond]

ah, thanks! weird that it wasn't showing an error with that term

[Ruben Van de Velde]

And your other issue is that autoImplicit is on by default, or you'd have gotten an error

[Matt Diamond]

oh I see

[Matt Diamond]

thanks for the help!

[Kyle Miller]

That's fascinating that this rw bug never popped up before, given just how well tested that tactic is. There aren't too many references to "infer type failed, unknown variable" on the zulip, and none in the issue tracker for Lean 3.

[Matt Diamond]

Yeah, I think it has something to do with classes... if I add resetI prior to the rw then the issue goes away. But it's nbd if this never gets fixed, it's not a blocker for me (and I should probably stop using Lean 3 anyway).