equating numbers from maps and co maps

Stream: Is there code for X?

[Max Bobbin]

I was working on this idea a while ago when I made a post about the congruence of filter.tendsto. I'm trying to show that if we know a the limit of a function evaluates to x at a and assume that it evaluates to x at b as a comap, then a = b. I wanted to make sure what I am trying to prove is actually true. The tricky part is using the nhds_within

edit: added 0 < a

import data.real.basic


example
(a b : ℝ)
(f : ℝ → ℝ)
(ha : 0 < a)
(h : filter.tendsto f (nhds_within a (set.Ioo 0 a)) filter.at_top)
(h1 : filter.tendsto f (nhds_within a (set.Ioi a)) filter.at_bot)
(h2 : filter.at_top.comap f ≤ (nhds_within b (set.Ioo 0 b)))
(h3 : filter.at_bot.comap f ≤ (nhds_within b (set.Ioi b)))
: a = b :=

[Max Bobbin]

using (filter.map_le_iff_le_comap.1 h).trans h2 I can get nhds_within a (set.Ioo 0 a) ≤ nhds_within b (set.Ioo 0 b)

[Max Bobbin]

same with using h1 and h3

[Kevin Buzzard]

This code doesn't compile for me. Are you on an old mathlib? Adding something like import topology.instances.real gets it working again. My mental model for filter.tendsto says that if a<0 then h is vacuously true and this doesn't bode well somehow.

[Max Bobbin]

I am on an old version of mathlib for Lean 3. We are cleaning up our github before we update. I also forgot 0 < a let me edit the post