no goals
α : Type u_1
β : Type ?u.828734
γ : Type ?u.828737
δ : Type ?u.828740
ι : Type ?u.828743
R : Type ?u.828746
R' : Type ?u.828749
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
⊢ ∃ s, x ∈ s ∧ IsOpen s ∧ ↑↑μ s < ⊤
simpa only [exists_prop, and_assoc] using
  (μ.finiteAt_nhds x).exists_mem_basis (nhds_basis_opens x)