-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem _root_.MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt
    [InnerRegularCompactLTTop μ] [IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α]
    {s : Set α} (hs : NullMeasurableSet s μ) (hμs : μ s ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ U, IsOpen U ∧ μ U < ∞ ∧ μ (U ∆ s) < ε

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
U : Set α
hUo : IsOpen U
hμU : μ U < ⊤
hUs : μ (U ∆ t) < ε
⊢ ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε

Tactic:
refine ⟨U, hUo, hμU, ?_⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
U : Set α
hUo : IsOpen U
hμU : μ U < ⊤
hUs : μ (U ∆ t) < ε
⊢ μ (U ∆ s) < ε

Proof state:
case intro.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε

Tactic:
rcases htm.exists_isOpen_symmDiff_lt (by rwa [← measure_congr hst]) hε with ⟨U, hUo, hμU, hUs⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
U : Set α
hUo : IsOpen U
hμU : μ U < ⊤
hUs : μ (U ∆ t) < ε
⊢ ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ ?m.151190 t ≠ ⊤

Tactic:
rwa [← measure_congr hst]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
U : Set α
hUo : IsOpen U
hμU : μ U < ⊤
hUs : μ (U ∆ t) < ε
⊢ μ (U ∆ s) < ε

Tactic:
rwa [measure_congr <| (ae_eq_refl _).symmDiff hst]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : NullMeasurableSet s μ
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε

Tactic:
rcases hs with ⟨t, htm, hst⟩

Result:
case intro.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε