Theorem: null_set_from_countable_cover (Sard/LocallyLipschitzMeasureZero.lean)

State before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
⊢ ↑μ t = 0
Tactic:
have h : μ t ≤ 0 := by
  have : ∀ n, μ (s n ∩ t) = 0 := fun n => measure_inter_null_of_null_left t (hnull n)
  calc μ t
    _ = μ ((⋃ (n : ℕ), s n) ∩ t) := by simp only [inter_eq_right.mpr hcov]
    _ = μ (⋃ (n : ℕ), (s n ∩ t)) := by rw [iUnion_inter]
    _ ≤ ∑' (n : ℕ), μ (s n ∩ t) := by apply OuterMeasure.iUnion_nat
    _ = ∑' (n : ℕ), 0 := by simp_rw [this]
    _ = 0 := by rw [tsum_zero]
State after:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
h : ↑μ t ≤ 0
⊢ ↑μ t = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
h : ↑μ t ≤ 0
⊢ ↑μ t = 0
Tactic:
simp only [nonpos_iff_eq_zero, zero_le] at h ⊢
State after:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
h : ↑μ t = 0
⊢ ↑μ t = 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
h : ↑μ t = 0
⊢ ↑μ t = 0
Tactic:
exact h
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
⊢ ↑μ t ≤ 0
Tactic:
have : ∀ n, μ (s n ∩ t) = 0 := fun n => measure_inter_null_of_null_left t (hnull n)
State after:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ↑μ t ≤ 0

State before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ↑μ t ≤ 0
Tactic:
calc μ t
  _ = μ ((⋃ (n : ℕ), s n) ∩ t) := by simp only [inter_eq_right.mpr hcov]
  _ = μ (⋃ (n : ℕ), (s n ∩ t)) := by rw [iUnion_inter]
  _ ≤ ∑' (n : ℕ), μ (s n ∩ t) := by apply OuterMeasure.iUnion_nat
  _ = ∑' (n : ℕ), 0 := by simp_rw [this]
  _ = 0 := by rw [tsum_zero]
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ↑μ t = ↑μ ((⋃ n, s n) ∩ t)
Tactic:
simp only [inter_eq_right.mpr hcov]
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ↑μ ((⋃ n, s n) ∩ t) = ↑μ (⋃ n, s n ∩ t)
Tactic:
rw [iUnion_inter]
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ↑μ (⋃ n, s n ∩ t) ≤ ∑' (n : ℕ), ↑μ (s n ∩ t)
Tactic:
apply OuterMeasure.iUnion_nat
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ∑' (n : ℕ), ↑μ (s n ∩ t) = ∑' (n : ℕ), 0
Tactic:
simp_rw [this]
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
inst✝⁵ : MetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : MetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
t : Set X
μ : Measure X
s : ℕ → Set X
hnull : ∀ (n : ℕ), ↑μ (s n) = 0
hcov : t ⊆ ⋃ n, s n
this : ∀ (n : ℕ), ↑μ (s n ∩ t) = 0
⊢ ∑' (n : ℕ), 0 = 0
Tactic:
rw [tsum_zero]
State after:
no goals