refl for <= on ennreal

Stream: general

[Kevin Buzzard]

This surprised me:

import data.real.ennreal

open_locale ennreal

noncomputable instance : preorder ℝ≥0∞ := infer_instance -- works fine

example (a : ℝ≥0∞) : a ≤ a :=
begin
  exact le_refl a, -- works fine
end

example (a : ℝ≥0∞) : a ≤ a :=
begin
  refl, -- fails
  /-
  invalid apply tactic, failed to unify
    a ≤ a
  with
    ∀ [_inst_1 : preorder ?m_1] (a : ?m_1), a ≤ a
  -/
end

I don't think I've seen refl failing to prove x <= x on a preorder before.

[Kevin Buzzard]

Is it the apply bug?

example (a : ℝ≥0∞) : a ≤ a :=
begin
  apply le_refl _, -- works
end

example (a : ℝ≥0∞) : a ≤ a :=
begin
  apply le_refl, -- fails
end

[Alex J. Best]

I guess this is why we have refl' docs#tactic.interactive.reflexivity'

[Floris van Doorn]

Yes, this is the apply bug.

[Kevin Buzzard]

Thanks both. Indeed refl' works.

[Yury G. Kudryashov]

Should we redefine order on with_top?

[Yury G. Kudryashov]

With eqn compiler

[Yaël Dillies]

Yeah, I don't really understand the point of the current definition.

[Eric Wieser]

Are you describing docs#with_top.has_le?

[Eric Wieser]

I could believe the current definition is vaguely useful to at least have as a lemma statement somewhere, but the defeqs feel far more useful in the equation compiler version

[Yaël Dillies]

Yes, exactly.

[Yury G. Kudryashov]

Who is going to make a PR?

[Yury G. Kudryashov]

Nobody volunteered, so I'm going to do it.

[Yury G. Kudryashov]

BTW, why docs#with_bot.has_le has priority 10?

[Yaël Dillies]

Something to do with with_bot/with_top leakage?