# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Equal within s imply same limit within s

#### Anatole Dedecker (Jun 25 2020 at 22:08):

Do we have something like this ?

```
lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α → β) :
∀ x ∈ s, f x = g x → tendsto f (nhds_within a s) l → tendsto g (nhds_within a s) l :=
begin
sorry,
end
```

#### Patrick Massot (Jun 25 2020 at 22:12):

You need a lemma whose name contains "congr".

#### Patrick Massot (Jun 25 2020 at 22:12):

This is not a riddle, that's all I can say at first sight.

#### Patrick Massot (Jun 25 2020 at 22:12):

Now I'll look at mathlib.

#### Patrick Massot (Jun 25 2020 at 22:13):

Oh, you got parentheses wrong

#### Anatole Dedecker (Jun 25 2020 at 22:14):

Patrick Massot said:

Oh, you got parentheses wrong

Where ?

#### Patrick Massot (Jun 25 2020 at 22:15):

The forall is binding too much.

#### Anatole Dedecker (Jun 25 2020 at 22:15):

Oh yeah

#### Patrick Massot (Jun 25 2020 at 22:16):

There is no point in having all this right of the colon anyway.

#### Anatole Dedecker (Jun 25 2020 at 22:18):

Indeed

#### Patrick Massot (Jun 25 2020 at 22:23):

It seems this lemma doesn't exist yet, but docs#filter.tendsto.congr' does.

#### Patrick Massot (Jun 25 2020 at 22:27):

Do you want the answer or do you want to try to finish using this hint only?

#### Patrick Massot (Jun 25 2020 at 22:27):

The proof I have is 72 characters long.

#### Anatole Dedecker (Jun 25 2020 at 22:31):

My PC just crashed, but yeah I've seen this one and I'm trying to deduce mine

#### Anatole Dedecker (Jun 25 2020 at 22:38):

I have this :

```
lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α → β)
(h : ∀ x ∈ s, f x = g x) (hf : tendsto f (nhds_within a s) l) : tendsto g (nhds_within a s) l :=
begin
intros,
rw ← tendsto_congr',
exact hf,
use univ,
split,
apply filter.univ_sets,
use s,
use (by tauto),
rw univ_inter,
intros x hx,
exact h x hx,
end
```

#### Anatole Dedecker (Jun 25 2020 at 22:39):

I think I'm going too deep in the definition unfolding

#### Anatole Dedecker (Jun 25 2020 at 22:41):

And the first line is useless, I should have removed it

#### Patrick Massot (Jun 25 2020 at 22:42):

Your proof doesn't work here. Are you using an old mathlib?

#### Patrick Massot (Jun 25 2020 at 22:43):

For the purpose of this conversation, old probably means older than https://github.com/leanprover-community/mathlib/commit/d287d34590761dc6237c7b21d9427580b2d339c4.

#### Anatole Dedecker (Jun 25 2020 at 22:45):

I definitely underestimated update frequency then :sweat_smile:

#### Patrick Massot (Jun 25 2020 at 22:45):

https://leanprover-community.github.io/mathlib_stats.html

#### Anatole Dedecker (Jun 25 2020 at 22:46):

HUGE lockdown peak x)

#### Patrick Massot (Jun 25 2020 at 22:46):

Of course!

#### Anatole Dedecker (Jun 25 2020 at 22:49):

I was in another file with one more `open`

, but it works now :

```
import analysis.calculus.mean_value
open filter set
lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α → β) :
(∀ x ∈ s, f x = g x) → tendsto f (nhds_within a s) l → tendsto g (nhds_within a s) l :=
begin
intros h hf,
rw ← tendsto_congr',
exact hf,
use univ,
split,
apply filter.univ_sets,
use s,
use (by tauto),
rw univ_inter,
intros x hx,
exact h x hx,
end
```

#### Anatole Dedecker (Jun 25 2020 at 22:50):

Well, I think it should at least

#### Patrick Massot (Jun 25 2020 at 23:03):

No, it doesn't work here. Did you update mathlib?

#### Anatole Dedecker (Jun 25 2020 at 23:08):

`leanproject up`

?

#### Anatole Dedecker (Jun 26 2020 at 11:27):

Well I've just run `leanproject up`

and this definitely compile :

```
import analysis.calculus.mean_value
open filter set
lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α → β) :
(∀ x ∈ s, f x = g x) → tendsto f (nhds_within a s) l → tendsto g (nhds_within a s) l :=
begin
intros h hf,
rw ← tendsto_congr',
exact hf,
use univ,
split,
apply filter.univ_sets,
use s,
use (by tauto),
rw univ_inter,
intros x hx,
exact h x hx,
end
```

#### Patrick Massot (Jun 26 2020 at 11:32):

The main trick you're missing in docs#filter.mem_inf_sets_of_right . One could argue this is relying on internal details of `nhds_within`

, and the `nhds_within`

API is lacking.

#### Sebastien Gouezel (Jun 26 2020 at 11:38):

This works for me:

```
lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α]
{a : α} {l : filter β} {s : set α} {f g : α → β}
(h : ∀ x ∈ s, f x = g x) (hf : tendsto f (nhds_within a s) l) : tendsto g (nhds_within a s) l :=
(tendsto_congr' (eventually_eq_iff_exists_mem.2 ⟨s, self_mem_nhds_within, h⟩)).1 hf
```

I am cheating because this won't work for you, as I have somewhere in `filter/basic.lean`

the lemma

```
lemma eventually_eq_iff_exists_mem {l : filter α} {f g : α → β} :
(f =ᶠ[l] g) ↔ ∃ s ∈ l, ∀ x ∈ s, f x = g x :=
filter.eventually_iff_exists_mem
```

#### Patrick Massot (Jun 26 2020 at 11:42):

Spoilers!

#### Anatole Dedecker (Jun 26 2020 at 11:43):

Well even `filter.eventually_iff_exists_mem`

doesn't exist for me, should it ?

#### Sebastien Gouezel (Jun 26 2020 at 11:43):

Not so much because it doesn't work with current mathlib :)

#### Anatole Dedecker (Jun 26 2020 at 11:43):

AH

#### Patrick Massot (Jun 26 2020 at 11:44):

Anatole, do you want to see a short solution that actually work, or do you want to keep trying?

#### Sebastien Gouezel (Jun 26 2020 at 11:44):

No, it doesn't exist either. But it is not hard to prove. It's just to illustrate that having basic API (which is currently missing) helps a lot to prove further statements.

#### Anatole Dedecker (Jun 26 2020 at 11:45):

Patrick Massot said:

Anatole, do you want to see a short solution that actually work, or do you want to keep trying?

I'll take it, I like to learn by imitating x)

#### Patrick Massot (Jun 26 2020 at 11:45):

`λ h, tendsto.congr' $ mem_inf_sets_of_right (eventually_principal.mpr h)`

#### Anatole Dedecker (Jun 26 2020 at 11:45):

Guess I should train to use term-mode too

#### Patrick Massot (Jun 26 2020 at 11:46):

But again the correct solution is add lots of tiny lemmas that are easy to find.

#### Patrick Massot (Jun 26 2020 at 11:47):

After the third line of your solution, you need to stop and think: there should be a lemma here. Then type `extract_goal`

, do some cleanup, prove and use.

#### Patrick Massot (Jun 26 2020 at 11:49):

@Yury G. Kudryashov there is a serious issue with precedences for the eventually_eq notation.

#### Patrick Massot (Jun 26 2020 at 11:52):

Anatole, the issue is that `eventually_eq`

and `eventually_le`

are *very* recent and still lack of lot of lemmas. Even `eventually`

and `frequently`

are not so old and still lack lemmas. If you unfold all see to basic filter stuff, involving only membership and lattices operations on filters, then all the lemmas are there. But we need a lot of plumbing.

#### Anatole Dedecker (Jun 26 2020 at 11:56):

Wow tidy is powerful

```
lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α → β) :
(∀ x ∈ s, f x = g x) → tendsto f (nhds_within a s) l → tendsto g (nhds_within a s) l :=
begin
intros h hf,
rw ← tendsto_congr',
exact hf,
apply mem_inf_sets_of_right,
tidy,
end
```

#### Anatole Dedecker (Jun 26 2020 at 11:56):

But I don't think that's what you were hoping me to do

#### Johan Commelin (Jun 26 2020 at 11:57):

`tidy?`

will tell you how it proved it

#### Anatole Dedecker (Jun 26 2020 at 11:58):

```
lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α → β) :
(∀ x ∈ s, f x = g x) → tendsto f (nhds_within a s) l → tendsto g (nhds_within a s) l :=
begin
intros h hf,
rw ← tendsto_congr',
exact hf,
apply mem_inf_sets_of_right,
assumption,
end
```

#### Anatole Dedecker (Jun 26 2020 at 11:58):

x)

#### Patrick Massot (Jun 26 2020 at 12:11):

Here is your plumbing exercise:

```
import topology.continuous_on
open_locale filter topological_space
open filter set
variables {α β : Type*} [topological_space α] {a : α} {s : set α} {f g : α → β}
lemma eventually_eq_nhds_within_iff :
(f =ᶠ[nhds_within a s] g) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → f x = g x :=
sorry
lemma eventually_eq_nhds_within_of_eq_on (h : eq_on f g s) : f =ᶠ[nhds_within a s] g :=
sorry
lemma tendsto_nhds_within_congr {l : filter β} (hfg : ∀ x ∈ s, f x = g x)
(hf : tendsto f (nhds_within a s) l) : tendsto g (nhds_within a s) l :=
sorry
```

Make sure you understand the choices of binders. The second and third proofs should be one line long terms. The first one will probably be longer, which means it should probably be split further.

#### Anatole Dedecker (Jun 26 2020 at 12:16):

Hey, I got shorter than you :grinning_face_with_smiling_eyes:

```
lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α → β) :
(∀ x ∈ s, f x = g x) → tendsto f (nhds_within a s) l → tendsto g (nhds_within a s) l :=
λ h, (tendsto_congr' (mem_inf_sets_of_right (by exact h))).1
```

#### Anatole Dedecker (Jun 26 2020 at 12:16):

Now it is not entirely clear why `by exact h`

can't be replaced by `h`

here :thinking:

#### Sebastien Gouezel (Jun 26 2020 at 12:21):

For readability, you can use

```
λ h, (tendsto_congr' $ mem_inf_sets_of_right $ by exact h).1
```

#### Patrick Massot (Jun 26 2020 at 12:21):

The fact that `by exact`

is needed shows Lean elaboration has trouble. You're not being nice to Lean, it has to unfold many definition in the right order to get there. This is why you need plumbing.

#### Yury G. Kudryashov (Jun 26 2020 at 12:33):

Patrick Massot said:

Yury G. Kudryashov there is a serious issue with precedences for the eventually_eq notation.

What exactly do you mean? #mwe?

#### Patrick Massot (Jun 26 2020 at 12:34):

https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Equal.20within.20s.20imply.20same.20limit.20within.20s/near/202081600 is autonomous. The first statement needs unexpected parentheses.

#### Patrick Massot (Jun 26 2020 at 12:34):

And I know I saw other examples yesterday.

#### Yury G. Kudryashov (Jun 26 2020 at 13:05):

```
notation f ` =ᶠ[`:50 l:50 `] `:0 g:50 := filter.eventually_eq l f g
```

works in this case.

#### Kevin Buzzard (Jun 26 2020 at 13:46):

Anatole Dedecker said:

Guess I should train to use term-mode too

If you concentrate on proving and tactic mode then you will slowly realise which proofs have "content" (e.g. they use high-powered tactics) and which proofs are literally just "intro, apply, cases, exact" which are really just ways to make a function piece by piece. For these "basic" proofs it's a good exercise to turn it into term mode (because you learn some weird tricks sometimes). After a while you can write hybrid proofs, where the intro/apply stuff is in term mode, and the occasional high-powered tactic like `rw`

is just done by briefly dropping into tactic mode with `by rw ...`

#### Anatole Dedecker (Jun 27 2020 at 14:42):

I've been busy IRL since yesterday afternoon, but here is the plumbing @Patrick Massot . I could shorten the first, especially if I finally start to learn `rcases`

:sweat_smile: but I'll work on this later, cause my parents are exploiting me right now x)

```
import topology.continuous_on
import tactic.tidy
open_locale filter topological_space
open filter set
variables {α β : Type*} [topological_space α] {a : α} {s : set α} {f g : α → β}
lemma eventually_eq_nhds_within_iff :
(f =ᶠ[nhds_within a s] g) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → f x = g x :=
begin
unfold eventually_eq,
rw eventually_iff,
rw eventually_iff,
rw mem_nhds_within,
rw mem_nhds_sets_iff,
split,
{ intros h,
cases h with u hu,
cases hu with hu hau,
cases hau with hau hus,
use u,
split,
intros x hx hxs,
apply hus,
exact and.intro hx hxs,
exact and.intro hu hau, },
{ intros h,
cases h with t ht,
cases ht with htsub ht,
cases ht with ht hta,
use t,
split,
exact ht,
split,
exact hta,
intros x hx,
cases hx with hxt hxs,
exact htsub hxt hxs }
end
lemma eventually_eq_nhds_within_of_eq_on (h : eq_on f g s) : f =ᶠ[nhds_within a s] g :=
mem_inf_sets_of_right h
lemma tendsto_nhds_within_congr {l : filter β} (hfg : ∀ x ∈ s, f x = g x)
(hf : tendsto f (nhds_within a s) l) : tendsto g (nhds_within a s) l :=
(tendsto_congr' $ eventually_eq_nhds_within_of_eq_on hfg).1 hf
```

#### Patrick Massot (Jun 27 2020 at 20:03):

Indeed you need to learn about `rintros`

/`rcases`

. But actually you are not using any tactic here. After the rewrite, everything you wrote has completely straightforward translation to term mode. You can also group your `rw`

in one tactic invocation.

#### Patrick Massot (Jun 27 2020 at 20:04):

```
lemma eventually_eq_nhds_within_iff :
(f =ᶠ[nhds_within a s] g) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → f x = g x :=
begin
rw [eventually_eq, eventually_iff, eventually_iff, mem_nhds_within, mem_nhds_sets_iff],
exact ⟨λ ⟨u, hu, hau, hus⟩, ⟨u, λ x hx hxs, hus ⟨hx, hxs⟩, ⟨hu, hau⟩⟩,
λ ⟨t, htsub, ht, hta⟩, ⟨t, ht, hta, λ x ⟨hxt, hxs⟩, htsub hxt hxs⟩⟩
end
```

#### Patrick Massot (Jun 27 2020 at 20:04):

This is exactly your proof, but without wasting too much space.

#### Patrick Massot (Jun 27 2020 at 20:07):

Note also:

- nobody is interested in seeing this proof since the statement is obvious. mathlib style in this case is to compress the proof.
- actually you don't loose any information. You can still move your cursor and see the tactic state. Note that the tactic state is update when you move your cursor from left to right in the
`rw`

line but also in the exact line. - you still miss intermediate lemmas that could be useful.

#### Patrick Massot (Jun 27 2020 at 20:13):

Elaborating on the third point: don't you find it weird that you had to use the definition of neighborhoods in this proof? Don't you feel the lemma should be more general than that?

#### Patrick Massot (Jun 27 2020 at 20:14):

```
import topology.continuous_on
open_locale filter topological_space
open filter
variables {α β : Type*} {a : α} {s : set α} {f g : α → β}
lemma eventually_eq_inf_principal_iff {F : filter α} :
(f =ᶠ[F ⊓ 𝓟 s] g) ↔ ∀ᶠ x in F, x ∈ s → f x = g x :=
by simp [eventually_eq, eventually_iff, mem_inf_principal]
lemma eventually_eq_nhds_within_iff [topological_space α] :
(f =ᶠ[nhds_within a s] g) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → f x = g x :=
eventually_eq_inf_principal_iff
```

Last updated: May 16 2021 at 05:21 UTC