α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.154319
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf :
  Tendsto
    ((fun x => (f x.fst.fst x.fst.snd, f x.snd.fst x.snd.snd)) ∘ fun p =>
      ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd))
    (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
⊢ ∃ u, u ∈ 𝓤 α ∧ ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.154319
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf : UniformContinuous fun p => f p.fst p.snd
hs : s ∈ 𝓤 β
⊢ ∃ u, u ∈ 𝓤 α ∧ ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
rw [UniformContinuous, uniformity_prod_eq_prod, tendsto_map'_iff] at hf
case intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.154319
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf :
  Tendsto
    ((fun x => (f x.fst.fst x.fst.snd, f x.snd.fst x.snd.snd)) ∘ fun p =>
      ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd))
    (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
u : Set (α × α)
hu : u ∈ 𝓤 α
v : Set (α × α)
hv : v ∈ 𝓤 α
huvt :
  u ×ˢ v ⊆
    ((fun x => (f x.fst.fst x.fst.snd, f x.snd.fst x.snd.snd)) ∘ fun p =>
        ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      s
⊢ ∃ u, u ∈ 𝓤 α ∧ ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.154319
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf :
  Tendsto
    ((fun x => (f x.fst.fst x.fst.snd, f x.snd.fst x.snd.snd)) ∘ fun p =>
      ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd))
    (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
⊢ ∃ u, u ∈ 𝓤 α ∧ ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
rcases mem_prod_iff.1 (mem_map.1 <| hf hs) with ⟨u, hu, v, hv, huvt⟩
no goals
case intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.154319
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf :
  Tendsto
    ((fun x => (f x.fst.fst x.fst.snd, f x.snd.fst x.snd.snd)) ∘ fun p =>
      ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd))
    (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
u : Set (α × α)
hu : u ∈ 𝓤 α
v : Set (α × α)
hv : v ∈ 𝓤 α
huvt :
  u ×ˢ v ⊆
    ((fun x => (f x.fst.fst x.fst.snd, f x.snd.fst x.snd.snd)) ∘ fun p =>
        ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      s
⊢ ∃ u, u ∈ 𝓤 α ∧ ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
exact ⟨u, hu, fun a b c hab => @huvt ((_, _), (_, _)) ⟨hab, refl_mem_uniformity hv⟩⟩