α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78279
inst✝ : UniformSpace α
a b : α
⊢ (Filter.lift (𝓤 α) fun s => Filter.lift' (𝓤 α) fun t => {y | (y, a) ∈ s} ×ˢ ball b t) =
    Filter.lift (𝓤 α) fun s => Filter.lift' (𝓤 α) fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

case hg₁
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78279
inst✝ : UniformSpace α
a b : α
⊢ Monotone fun s => {y | (y, a) ∈ s}

case hg₂
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78279
inst✝ : UniformSpace α
a b : α
⊢ Monotone (ball b)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78279
inst✝ : UniformSpace α
a b : α
⊢ 𝓝 a ×ˢ 𝓝 b = Filter.lift (𝓤 α) fun s => Filter.lift' (𝓤 α) fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
rw [nhds_eq_uniformity', nhds_eq_uniformity, prod_lift'_lift']
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78279
inst✝ : UniformSpace α
a b : α
⊢ (Filter.lift (𝓤 α) fun s => Filter.lift' (𝓤 α) fun t => {y | (y, a) ∈ s} ×ˢ ball b t) =
    Filter.lift (𝓤 α) fun s => Filter.lift' (𝓤 α) fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

case hg₁
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78279
inst✝ : UniformSpace α
a b : α
⊢ Monotone fun s => {y | (y, a) ∈ s}

case hg₂
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78279
inst✝ : UniformSpace α
a b : α
⊢ Monotone (ball b)
exacts [rfl, monotone_preimage, monotone_preimage]