Theorem: lemma0 (RMT4/uniform.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
inst✝ : UniformSpace α
⊢ Tendsto Prod.snd (𝓤 α ⊓ Filter.comap Prod.fst (𝓟 s)) (𝓝ᵘ s)
Tactic:
simp_rw [comap_principal, uniform_nhds_set, tendsto_lift', eventually_inf_principal]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
inst✝ : UniformSpace α
⊢ ∀ s_1 ∈ 𝓤 α, ∀ᶠ (x : α × α) in 𝓤 α, x ∈ Prod.fst ⁻¹' s → x.2 ∈ thickening s_1 s

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
inst✝ : UniformSpace α
⊢ ∀ s_1 ∈ 𝓤 α, ∀ᶠ (x : α × α) in 𝓤 α, x ∈ Prod.fst ⁻¹' s → x.2 ∈ thickening s_1 s
Tactic:
exact λ U hU => mem_of_superset hU (λ ⟨x, y⟩ hxy hx => mem_biUnion hx hxy)
State after:
no goals