Theorem: lemma1 (RMT4/uniform.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
F : ι → α → β
f : α → β
inst✝ : UniformSpace β
hF : TendstoUniformlyOn F f p s
⊢ Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
Tactic:
rw [tendstoUniformlyOn_iff_tendsto] at hF
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
F : ι → α → β
f : α → β
inst✝ : UniformSpace β
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
F : ι → α → β
f : α → β
inst✝ : UniformSpace β
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
Tactic:
refine tendsto_prod_iff'.mpr ⟨lemma2, ?h⟩
State after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
F : ι → α → β
f : α → β
inst✝ : UniformSpace β
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto (fun n => (f n.2, F n.1 n.2).2) (p ×ˢ 𝓟 s) (𝓝ᵘ (f '' s))

State before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
F : ι → α → β
f : α → β
inst✝ : UniformSpace β
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto (fun n => (f n.2, F n.1 n.2).2) (p ×ˢ 𝓟 s) (𝓝ᵘ (f '' s))
Tactic:
exact lemma0.comp (tendsto_inf.mpr ⟨hF, tendsto_comap_iff.mpr lemma2⟩)
State after:
no goals