struggling to use one_div_pos with casting

Stream: new members

[Saif Ghobash]

Here is a MWE

example (n : ℕ) (h : 0 < 1/(↑n)): 0 < ↑n :=
begin
  rw one_div_pos at h,
end

Im getting the following error

rewrite tactic failed, did not find instance of the pattern in the target expression
  0 < _

[Bryan Gin-ge Chen]

Your example doesn't work for me, I get

failed to synthesize type class instance for
n : ℕ
⊢ has_lift_t ℕ ℕ

I suspect that what's going on in your actual example is that whatever type you're coercing to isn't one that satisfies the assumptions for one_div_pos. You can check this by using some pretty printing options, e.g. set_option pp.all true.

[Bryan Gin-ge Chen]

I think your MWE is missing some imports at the least.

[Saif Ghobash]

I just have data.real.basic imported, I retired the example with n as a real number explicitly (i.e 0 < 1/(n:\R)) and it worked, anyways. thank you.

[Kevin Buzzard]

Right -- Lean doesn't know where you're coercing to if you just use the arrow.