Best practices for eventually equal sets

Stream: mathlib4

[Geoffrey Irving]

Here's an example of a lemma about sets being eventually equal. It's true and I have a proof, but the proof is super messy because eventual equality and filter_upwards on Set X turns x \in s into s x. Is there a better way to either state or prove this kind of lemma?

lemma Set.eventuallyEq_inter {X : Type} [TopologicalSpace X] {s t u : Set X} {x : X} :
    (t ∩ s : Set X) =ᶠ[𝓝 x] (u ∩ s : Set X) ↔ t =ᶠ[𝓝[s] x] u := by
  rw [Filter.EventuallyEq, eventuallyEq_nhdsWithin_iff]
  constructor
  · intro h
    filter_upwards [h]
    -- `filter_upwards` on sets drops ∈ notation, so we recover it manually
    suffices h : ∀ x, (x ∈ (t ∩ s) ↔ x ∈ (u ∩ s)) → x ∈ s → (x ∈ t ↔ x ∈ u) by
      simp only [← eq_iff_iff] at h; exact h
    intro x e m
    simpa only [mem_inter_iff, m, and_true] using e
  · intro h
    filter_upwards [h]
    -- `filter_upwards` on sets drops ∈ notation, so we recover it manually
    suffices h : ∀ x, (x ∈ s → (x ∈ t ↔ u x)) → (x ∈ t ∩ s ↔ x ∈ u ∩ s) by
      simp only [← eq_iff_iff] at h; exact h
    intro x h
    simpa only [mem_inter_iff, and_congr_left_iff

[Yaël Dillies]

filter_upwards is only doing what you told it to, namely to consider t as a function. You committed the sin when writing t =ᶠ[𝓝[s] x] u instead of (· ∈ t) =ᶠ[𝓝[s] x] (· ∈ u)

[Geoffrey Irving]

Thanks, that's much better!

lemma Set.eventuallyEq_inter {X : Type} [TopologicalSpace X] {s t u : Set X} {x : X} :
    (· ∈ t ∩ s) =ᶠ[𝓝 x] (· ∈ u ∩ s) ↔ (· ∈ t) =ᶠ[𝓝[s] x] (· ∈ u) := by
  rw [Filter.EventuallyEq, eventuallyEq_nhdsWithin_iff]
  simp only [mem_inter_iff, eq_iff_iff, and_congr_left_iff]

[Geoffrey Irving]

Looks like the sin is elsewhere in Mathlib, though: docs#nhdsWithin_eq_iff_eventuallyEq.

[Yaël Dillies]

... yes :sad:

[Yaël Dillies]

I have in the past argued against but someone was for keeping it (I think?). IIRC here are a few people who were previously involved: @Sébastien Gouëzel, @Oliver Nash

[Geoffrey Irving]

I imagine there's been extensive discussion about making x \in s an abbrev too. :)

[Geoffrey Irving]

Interesting, docs#nhdsWithin_eq_iff_eventuallyEq is annoying to use because of this, but if I make an alternate version without the sin it doesn't infer as I'd expect to it. So dragons everywhere... :)

[Yaël Dillies]

Oh, do you mind explaining?

[Sébastien Gouëzel]

Indeed, I had started (maybe even completed) a refactor, for the same thing in measure theory, replacing everywhere t =ᶠ[mu] u with (· ∈ t) =ᶠ[mu] (· ∈ u). It worked, and avoided a few elaboration issues, but it was so ugly and so much more verbose that we collectively decided not to merge it.
The next suggestion was to have a new notation for almost everywhere equality of sets, but nobody implemented it yet.

[Geoffrey Irving]

Hmm, actually the version without the sin does work better. Not sure what I did differently when I reconstructed the problem:

/-- Version that doesn't commit the sin -/
lemma nhdsWithin_eq_iff_eventuallyEq' {X : Type} [TopologicalSpace X] {s t : Set X} {x : X} :
    𝓝[s] x = 𝓝[t] x ↔ (· ∈ s) =ᶠ[𝓝 x] (· ∈ t) :=
  nhdsWithin_eq_iff_eventuallyEq

/-- This proof works, but requires two manually rewriting the result type of
`nhdsWithin_eq_iff_eventuallyEq` -/
lemma ContinuousWithinAt.congr_set {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} {s t : Set X} {x : X} (fc : ContinuousWithinAt f s x)
    (hst : (· ∈ s) =ᶠ[𝓝 x] (· ∈ t)) : ContinuousWithinAt f t x := by
  have e : 𝓝[s] x = 𝓝[t] x := nhdsWithin_eq_iff_eventuallyEq.mpr hst
  simpa only [ContinuousWithinAt, e] using fc

/-- This one line proof does not work. -/
lemma ContinuousWithinAt.congr_set' {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} {s t : Set X} {x : X} (fc : ContinuousWithinAt f s x)
    (hst : (· ∈ s) =ᶠ[𝓝 x] (· ∈ t)) : ContinuousWithinAt f t x := by
  -- Fails, since I didn't rewrite the type of `nhdsWithin_eq_iff_eventuallyEq.mpr hst`
  simpa only [ContinuousWithinAt, nhdsWithin_eq_iff_eventuallyEq.mpr hst] using fc

/-- Using `nhdsWithin_eq_iff_of_eventuallyEq'` helps, oops, I thought it didn't on the first try -/
lemma ContinuousWithinAt.congr_set'' {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} {s t : Set X} {x : X} (fc : ContinuousWithinAt f s x)
    (hst : (· ∈ s) =ᶠ[𝓝 x] (· ∈ t)) : ContinuousWithinAt f t x := by
  -- Ah, this does work.
  simpa only [ContinuousWithinAt, nhdsWithin_eq_iff_eventuallyEq'.mpr hst] using fc