rewrite fails

Stream: general

[Kevin Buzzard]

import algebra.archimedean
import topology.algebra.ordered

variables {β : Type*} [discrete_linear_ordered_field β] [floor_ring β] [topological_space β]
  [orderable_topology β]

open filter

def digit (b : ℕ) (r : β) (i : ℕ) : ℤ := 37

theorem expansion_tendsto {b : ℕ} (hb : 1 < b) (r : β) (N : ℕ) :
  tendsto (λ n : ℕ, finset.sum (finset.range n)
    (λ i, (digit b r i : β) * b ^ (n - 1 - i) / b ^ n))
    at_top (nhds (fract r)) :=
begin
  -- rw tendsto_orderable, -- why does this fail?
  /-
  invalid rewrite tactic, failed to synthesize type class instance
  -/
  apply tendsto_orderable.2, -- works fine, now 3 goals
    swap, apply_instance, swap, apply_instance, -- type class inference deals with two
  sorry
end

Why does the rewrite fail?

[Kevin Buzzard]

Type class inference can find all the relevant instances.

[Chris Hughes]

I don't know why, but sometimes rw @tendsto_orderable \b _ _ _ _ works