ennreal not \le itself?

Stream: new members

[Rémy Degenne]

Hello everyone. I am new to lean and a small problem is currently puzzling me: I cannot find how to complete the following goal,

example (a : ennreal) : a ≤ a :=
begin
  sorry,
end

Replacing sorry by refl or by simp fails, and I don't understand why.
Thanks!

[Johan Commelin]

Hmm, both should work

[Johan Commelin]

import data.real.ennreal

example (x : ennreal) : x ≤ x :=
begin
  exact le_refl x
end

this works...

[Johan Commelin]

But I can't replace the exact le_refl x by apply le_refl

[Johan Commelin]

very strange

[Rémy Degenne]

Thank you. At least I can get the other parts of my code to work. But it is indeed very strange.

[Reid Barton]

Presumably the apply bug. Does refl use apply perhaps?

[Johan Commelin]

example (x : ennreal) : x ≤ x :=
begin
  refl' -- works
end

[Kevin Buzzard]

Nice work Rémy, you (re)discovered an annoying bug which is surprisingly hard to fix :-) Fortunately we have workarounds