α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.snd, F n.fst n.snd) ∈ u
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
⊢ TendstoUniformlyOnFilter F f p p'
intro u hu
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.snd, F n.fst n.snd) ∈ u
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.snd, F n.fst n.snd) ∈ u
rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.snd, F n.fst n.snd) ∈ u
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.snd, F n.fst n.snd) ∈ u
have hmc : ∀ᶠ x in (p ×ˢ p) ×ˢ p', Tendsto (fun n : ι => F n x.snd) p (𝓝 (f x.snd)) := by
  rw [eventually_prod_iff]
  refine' ⟨fun _ => True, by simp, _, hF', by simp⟩
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f (Prod.swap y).snd, F (Prod.swap y).fst (Prod.swap y).snd) ∈ u
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.snd, F n.fst n.snd) ∈ u
rw [Filter.eventually_swap_iff]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f (Prod.swap y).snd, F (Prod.swap y).fst (Prod.swap y).snd) ∈ u
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f (Prod.swap y).snd, F (Prod.swap y).fst (Prod.swap y).snd) ∈ u
have := tendsto_prodAssoc.eventually (tendsto_prod_swap.eventually ((hF t ht).and hmc))
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
⊢ ∀ (x : α × ι),
    (∀ᶠ (y : ι) in p,
        (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).snd,
              F (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).fst.snd
                (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).snd) ∈
            t ∧
          Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).snd) p
            (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).snd))) →
      (f (Prod.swap x).snd, F (Prod.swap x).fst (Prod.swap x).snd) ∈ u
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f (Prod.swap y).snd, F (Prod.swap y).fst (Prod.swap y).snd) ∈ u
apply this.curry.mono
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
⊢ ∀ (a : α) (b : ι), (∀ᶠ (x : ι) in p, (F b a, F x a) ∈ t) → Tendsto (fun n => F n a) p (𝓝 (f a)) → (f a, F b a) ∈ u
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
⊢ ∀ (x : α × ι),
    (∀ᶠ (y : ι) in p,
        (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).snd,
              F (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).fst.snd
                (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).snd) ∈
            t ∧
          Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).snd) p
            (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).snd))) →
      (f (Prod.swap x).snd, F (Prod.swap x).fst (Prod.swap x).snd) ∈ u
simp only [Equiv.prodAssoc_apply, eventually_and, eventually_const, Prod.snd_swap, Prod.fst_swap,
  and_imp, Prod.forall]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun n => F n x) p (𝓝 (f x))
⊢ (f x, F n x) ∈ u
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
⊢ ∀ (a : α) (b : ι), (∀ᶠ (x : ι) in p, (F b a, F x a) ∈ t) → Tendsto (fun n => F n a) p (𝓝 (f a)) → (f a, F b a) ∈ u
intro x n hx hm'
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun n => F n x) p (𝓝 (f x))
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun n => F n x) p (𝓝 (f x))
⊢ (f x, F n x) ∈ u
refine' Set.mem_of_mem_of_subset (mem_compRel.mpr _) htmem
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun n => F n x) p (𝓝 (f x))
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
rw [Uniform.tendsto_nhds_right] at hm'
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this✝ :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)
this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun x_2 => (f x, F x_2 x)) x_1 ∈ t
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
have := hx.and (hm' ht)
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this✝ :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)
this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun x_2 => (f x, F x_2 x)) x_1 ∈ t
m : ι
hm : (F n x, F m x) ∈ t ∧ (fun x_1 => (f x, F x_1 x)) m ∈ t
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this✝ :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)
this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun x_2 => (f x, F x_2 x)) x_1 ∈ t
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
obtain ⟨m, hm⟩ := this.exists
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this✝ :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)
this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun x_2 => (f x, F x_2 x)) x_1 ∈ t
m : ι
hm : (F n x, F m x) ∈ t ∧ (fun x_1 => (f x, F x_1 x)) m ∈ t
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
exact ⟨F m x, ⟨hm.2, htsymm hm.1⟩⟩
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∃ pa,
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ pb,
        (∀ᶠ (y : α) in p', pb y) ∧
          ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → Tendsto (fun n => F n (x, y).snd) p (𝓝 (f (x, y).snd))
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
rw [eventually_prod_iff]
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∃ pa,
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ pb,
        (∀ᶠ (y : α) in p', pb y) ∧
          ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → Tendsto (fun n => F n (x, y).snd) p (𝓝 (f (x, y).snd))
refine' ⟨fun _ => True, by simp, _, hF', by simp⟩
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∀ᶠ (x : ι × ι) in p ×ˢ p, (fun x => True) x
simp
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∀ {x : ι × ι},
    (fun x => True) x →
      ∀ {y : α}, Tendsto (fun n => F n y) p (𝓝 (f y)) → Tendsto (fun n => F n (x, y).snd) p (𝓝 (f (x, y).snd))
simp