Real.lt

Stream: mathlib4

[Michael Stoll]

Consider the following.

import Mathlib.Data.Real.Basic

lemma xyz {f g : ℝ → ℝ} {s : Set ℝ} (h : s.EqOn f g) {x : ℝ} (hx : x ∈ s) : f x = g x :=
  h hx

lemma xxx (f : ℝ → ℝ) : f 2 = f 2 := by
  have H (s) (hs : 1 < s) : f s = f s := rfl
  have H' : ∀ s ∈ {s | 1 < s}, f s = f s := fun _ _ ↦ rfl
  have : H = H' := rfl
  refine xyz H ?_
  -- ⊢ 2 ∈ Real.lt 1
  -- with `H'` in place of `H`, the goal is, as expected,
  -- ⊢ 2 ∈ {s | 1 < s}
  sorry

#check Real.lt -- unknown constant 'Real.lt'

Using H (which is defeq to what is expected at this point) results in a strange goal involving Real.lt, which is a private definition (in Data.Real.Basic) without API (it is just used to define < on reals), which means that one gets stuck.

Is this expected or perhaps a bug?

[Matthew Ballard]

This is probably relatively recent and due to lean#5020 which allows Lean to more eagerly reduce docs#Membership.mem