-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformContinuousOn.tendstoUniformlyOn [UniformSpace α] [UniformSpace γ] {x : α} {U : Set α}
    {V : Set β} {F : α → β → γ} (hF : UniformContinuousOn (↿F) (U ×ˢ V)) (hU : x ∈ U) :
    TendstoUniformlyOn F (F x) (𝓝[U] x) V

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
⊢ TendstoUniformlyOn F (F x) (𝓝[U] x) V

Tactic:
set φ := fun q : α × β => ((x, q.2), q)

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)
⊢ TendstoUniformlyOn F (F x) (𝓝[U] x) V

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)
⊢ Tendsto ((fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ φ) (comap (Prod.mk x ∘ Prod.fst) (𝓤 α)) (𝓤 α ×ˢ 𝓤 β)

Tactic:
exact tendsto_comap.prod_mk (tendsto_diag_uniformity _ _)

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)
⊢ Tendsto (fun q => (F x q.2, F q.1 q.2)) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)

Tactic:
change Tendsto (Prod.map (↿F) ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)
⊢ Tendsto (Prod.map (↿F) ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)
⊢ Tendsto (Prod.map (↿F) ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)

Tactic:
simp only [nhdsWithin, Filter.prod_eq_inf, comap_inf, inf_assoc, comap_principal, inf_principal]

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)
⊢ Tendsto (Prod.map (↿F) ↿F ∘ φ) (comap Prod.fst (𝓝 x) ⊓ 𝓟 (Prod.fst ⁻¹' U ∩ Prod.snd ⁻¹' V)) (𝓤 γ)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)
⊢ Tendsto (Prod.map (↿F) ↿F ∘ φ) (comap Prod.fst (𝓝 x) ⊓ 𝓟 (Prod.fst ⁻¹' U ∩ Prod.snd ⁻¹' V)) (𝓤 γ)

Tactic:
refine hF.comp (Tendsto.inf ?_ <| tendsto_principal_principal.2 fun x hx => ⟨⟨hU, hx.2⟩, hx⟩)

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)
⊢ Tendsto φ (comap Prod.fst (𝓝 x)) (𝓤 (α × β))

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)
⊢ TendstoUniformlyOn F (F x) (𝓝[U] x) V

Tactic:
rw [tendstoUniformlyOn_iff_tendsto]

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)
⊢ Tendsto (fun q => (F x q.2, F q.1 q.2)) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)