Can't infer nontrivial ℝ

Stream: Is there code for X?

[Winston Yin]

Just started exploring the analysis part of mathlib. Why can't Lean infer the instance nontrivial ℝ? How would you prove this?

example (r : ℝ) (hr : 0 < r) : 0 < r / 2 :=
begin
  rw lt_div_iff zero_lt_two,
  rw zero_mul,
  exact hr,
  apply_instance -- why can't Lean infer nontrivial ℝ?
end

[Yaël Dillies]

Can you include imports?

[Winston Yin]

(sorry, I meant to post this on #general)

[Winston Yin]

import geometry.manifold.mfderiv
import analysis.ODE.picard_lindelof

[Winston Yin]

Same behaviour with just:

import analysis.ODE.picard_lindelof

[Kyle Miller]

I'm finding that

import analysis.ODE.picard_lindelof

example (r : ℝ) (hr : 0 < r) : 0 < r / 2 :=
begin
  rw lt_div_iff zero_lt_two,
  rw zero_mul,
  exact hr,
  apply_instance
end

works just fine on a recent mathlib

[Yaël Dillies]

When you mean "why can't Lean infer nontrivial ℝ?", do you mean "why am I presented this goal?"?

[Kyle Miller]

I've never really understood what causes rw to need to introduce instance goals (especially since there are a number of others here that it seems to find just fine), but giving it a hint that the lemma is about the reals helps it out:

example (r : ℝ) (hr : 0 < r) : 0 < r / 2 :=
begin
  rw lt_div_iff (zero_lt_two : (0 : ℝ) < _),
  rw zero_mul,
  exact hr,
end

[Yaël Dillies]

This is a recurring problem with the zero_lt_... lemmas, so I'm adding a version with the type explicit in #16172.

[Adam Topaz]

linarith also works :)

[Yaël Dillies]

Or just docs#half_pos

[Adam Topaz]

but who can remember that?!

[Yaël Dillies]

Me, in fact :stuck_out_tongue_wink:

[Winston Yin]

Yaël Dillies said:

When you mean "why can't Lean infer nontrivial ℝ?", do you mean "why am I presented this goal?"?

Yeah. Why would Lean present me with this goal when apply_instance ends up finding it with no extra steps anyway?

[Winston Yin]

In the past when I've seen this behaviour it was because my own lemma included an unnecessary / unused typeclass variable

[Adam Topaz]

I think the reason has to do with the internals of how rw fills in metavariables.