-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem measure_null_of_locally_null [TopologicalSpace α] [SecondCountableTopology α]
    (s : Set α) (hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, μ u = 0) : μ s = 0

Proof state:
case intro.intro
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
t : Set α
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ ⋃ x ∈ t, u x
⊢ μ (⋃ x ∈ t, u x) = 0

Tactic:
exact (measure_biUnion_null_iff t_count).2 fun x hx => hu₀ x (ts hx)

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
⊢ μ s = 0

Tactic:
choose t ht using TopologicalSpace.countable_cover_nhdsWithin hxu

Result:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
t : Set α
ht : t ⊆ s ∧ t.Countable ∧ s ⊆ ⋃ x ∈ t, u x
⊢ μ s = 0

Proof state:
case intro.intro
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
t : Set α
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ ⋃ x ∈ t, u x
⊢ μ s = 0

Tactic:
apply measure_mono_null ht

Result:
case intro.intro
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
t : Set α
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ ⋃ x ∈ t, u x
⊢ μ (⋃ x ∈ t, u x) = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, μ u = 0
⊢ μ s = 0

Tactic:
choose! u hxu hu₀ using hs

Result:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
⊢ μ s = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
t : Set α
ht : t ⊆ s ∧ t.Countable ∧ s ⊆ ⋃ x ∈ t, u x
⊢ μ s = 0

Tactic:
rcases ht with ⟨ts, t_count, ht⟩

Result:
case intro.intro
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
u : α → Set α
hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x
hu₀ : ∀ x ∈ s, μ (u x) = 0
t : Set α
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ ⋃ x ∈ t, u x
⊢ μ s = 0