case inl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.178177
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
val✝ : α
xs : inl val✝ ∈ s
⊢ {p | p.fst = inl val✝ → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity

case inr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.178177
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
val✝ : β
xs : inr val✝ ∈ s
⊢ {p | p.fst = inr val✝ → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.178177
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
x : α ⊕ β
xs : x ∈ s
⊢ {p | p.fst = x → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
cases x
case inl.refine'_1.intro.mk.intro.refl.refl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.178177
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
fst✝ b : α
xs : inl (fst✝, b).fst ∈ s
h : (fst✝, b) ∈ {p | p.fst = (fst✝, b).fst → p.snd ∈ inl ⁻¹' s}
⊢ ((fun p => (inl p.fst, inl p.snd)) (fst✝, b)).snd ∈ s
case inl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.178177
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
val✝ : α
xs : inl val✝ ∈ s
⊢ {p | p.fst = inl val✝ → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
refine' mem_of_superset
  (union_mem_uniformity_sum (mem_nhds_uniformity_iff_right.1 (hs.1.mem_nhds xs)) univ_mem)
    (union_subset _ _) <;> rintro _ ⟨⟨_, b⟩, h, ⟨⟩⟩ ⟨⟩
no goals
case inl.refine'_1.intro.mk.intro.refl.refl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.178177
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
fst✝ b : α
xs : inl (fst✝, b).fst ∈ s
h : (fst✝, b) ∈ {p | p.fst = (fst✝, b).fst → p.snd ∈ inl ⁻¹' s}
⊢ ((fun p => (inl p.fst, inl p.snd)) (fst✝, b)).snd ∈ s
exact h rfl
case inr.refine'_2.intro.mk.intro.refl.refl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.178177
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
a snd✝ : β
xs : inr (a, snd✝).fst ∈ s
h : (a, snd✝) ∈ {p | p.fst = (a, snd✝).fst → p.snd ∈ inr ⁻¹' s}
⊢ ((fun p => (inr p.fst, inr p.snd)) (a, snd✝)).snd ∈ s
case inr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.178177
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
val✝ : β
xs : inr val✝ ∈ s
⊢ {p | p.fst = inr val✝ → p.snd ∈ s} ∈ UniformSpace.Core.sum.uniformity
refine' mem_of_superset
  (union_mem_uniformity_sum univ_mem (mem_nhds_uniformity_iff_right.1 (hs.2.mem_nhds xs)))
    (union_subset _ _) <;> rintro _ ⟨⟨a, _⟩, h, ⟨⟩⟩ ⟨⟩
no goals
case inr.refine'_2.intro.mk.intro.refl.refl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.178177
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α ⊕ β)
hs : IsOpen s
a snd✝ : β
xs : inr (a, snd✝).fst ∈ s
h : (a, snd✝) ∈ {p | p.fst = (a, snd✝).fst → p.snd ∈ inr ⁻¹' s}
⊢ ((fun p => (inr p.fst, inr p.snd)) (a, snd✝)).snd ∈ s
exact h rfl