## Stream: general

### Topic: rewrite fails

#### Kevin Buzzard (Mar 14 2019 at 23:17):

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 (Mar 14 2019 at 23:17):

Type class inference can find all the relevant instances.

#### Chris Hughes (Mar 14 2019 at 23:30):

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

Last updated: May 11 2021 at 21:10 UTC