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

case hg₂
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78723
inst✝ : UniformSpace α
a b : α
⊢ ∀ (t : Set (α × α)), Monotone fun s => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78723
inst✝ : UniformSpace α
a b : α
⊢ 𝓝 (a, b) = Filter.lift' (𝓤 α) fun s => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ s}
rw [nhds_prod_eq, nhds_nhds_eq_uniformity_uniformity_prod, lift_lift'_same_eq_lift']
no goals
case hg₁
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78723
inst✝ : UniformSpace α
a b : α
⊢ ∀ (s : Set (α × α)), Monotone fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
exact fun s => monotone_const.set_prod monotone_preimage
case hg₂
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78723
inst✝ : UniformSpace α
a b : α
t : Set (α × α)
⊢ Monotone fun s => {y | (y, a) ∈ s}
case hg₂
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78723
inst✝ : UniformSpace α
a b : α
⊢ ∀ (t : Set (α × α)), Monotone fun s => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
refine fun t => Monotone.set_prod ?_ monotone_const
no goals
case hg₂
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.78723
inst✝ : UniformSpace α
a b : α
t : Set (α × α)
⊢ Monotone fun s => {y | (y, a) ∈ s}
exact monotone_preimage (f := fun y => (y, a))