[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
s : ℕ → Set (NullMeasurableSpace α)
hs : ∀ (i : ℕ), (fun s => ∃ t, MeasurableSet t ∧ s =ᵐ[μ] t) (s i)
⊢ (fun s => ∃ t, MeasurableSet t ∧ s =ᵐ[μ] t) (⋃ (i : ℕ), s i)
[PROOFSTEP]
choose t htm hts using hs
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
s : ℕ → Set (NullMeasurableSpace α)
t : ℕ → Set α
htm : ∀ (i : ℕ), MeasurableSet (t i)
hts : ∀ (i : ℕ), s i =ᵐ[μ] t i
⊢ ∃ t, MeasurableSet t ∧ ⋃ (i : ℕ), s i =ᵐ[μ] t
[PROOFSTEP]
exact ⟨⋃ i, t i, MeasurableSet.iUnion htm, EventuallyEq.countable_iUnion hts⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → NullMeasurableSet t
⊢ NullMeasurableSet (⋃₀ s)
[PROOFSTEP]
rw [sUnion_eq_biUnion]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → NullMeasurableSet t
⊢ NullMeasurableSet (⋃ (i : Set α) (_ : i ∈ s), i)
[PROOFSTEP]
exact MeasurableSet.biUnion hs h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
[PROOFSTEP]
rcases h with ⟨t, htm, hst⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
[PROOFSTEP]
refine' ⟨t ∪ toMeasurable μ (s \ t), _, htm.union (measurableSet_toMeasurable _ _), _⟩
[GOAL]
case intro.intro.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ t ∪ toMeasurable μ (s \ t) ⊇ s
[PROOFSTEP]
exact diff_subset_iff.1 (subset_toMeasurable _ _)
[GOAL]
case intro.intro.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s
[PROOFSTEP]
have : toMeasurable μ (s \ t) =ᵐ[μ] (∅ : Set α) := by simp [ae_le_set.1 hst.le]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ toMeasurable μ (s \ t) =ᵐ[μ] ∅
[PROOFSTEP]
simp [ae_le_set.1 hst.le]
[GOAL]
case intro.intro.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
this : toMeasurable μ (s \ t) =ᵐ[μ] ∅
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s
[PROOFSTEP]
simpa only [union_empty] using hst.symm.union this
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ toMeasurable μ s =ᵐ[μ] s
[PROOFSTEP]
rw [toMeasurable_def, dif_pos]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ Exists.choose ?hc =ᵐ[μ] s
case hc
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
[PROOFSTEP]
exact (exists_measurable_superset_ae_eq h).choose_spec.snd.2
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i)
hd : Pairwise (AEDisjoint μ on s)
⊢ ∃ t, (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᵐ[μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
[PROOFSTEP]
choose t ht_sub htm ht_eq using fun i => exists_measurable_subset_ae_eq (h i)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i)
hd : Pairwise (AEDisjoint μ on s)
t : ι → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᵐ[μ] s i
⊢ ∃ t, (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᵐ[μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
[PROOFSTEP]
rcases exists_null_pairwise_disjoint_diff hd with ⟨u, hum, hu₀, hud⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i)
hd : Pairwise (AEDisjoint μ on s)
t : ι → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᵐ[μ] s i
u : ι → Set α
hum : ∀ (i : ι), MeasurableSet (u i)
hu₀ : ∀ (i : ι), ↑↑μ (u i) = 0
hud : Pairwise (Disjoint on fun i => s i \ u i)
⊢ ∃ t, (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᵐ[μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
[PROOFSTEP]
exact
  ⟨fun i => t i \ u i, fun i => (diff_subset _ _).trans (ht_sub _), fun i =>
    (ht_eq _).symm.trans (diff_null_ae_eq_self (hu₀ i)).symm, fun i => (htm i).diff (hum i),
    hud.mono fun i j h => h.mono (diff_subset_diff_left (ht_sub i)) (diff_subset_diff_left (ht_sub j))⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ↑↑μ (⋃ (i : ι), f i) = ∑' (i : ι), ↑↑μ (f i)
[PROOFSTEP]
rw [measure_eq_extend (MeasurableSet.iUnion h), extend_iUnion MeasurableSet.empty _ MeasurableSet.iUnion _ hn h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∑' (i : ι), extend (fun t _ht => ↑↑μ t) (f i) = ∑' (i : ι), ↑↑μ (f i)
[PROOFSTEP]
simp [measure_eq_extend, h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ↑↑μ ∅ = 0
[PROOFSTEP]
exact μ.empty
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → ↑↑μ (⋃ (i : ℕ), f i) = ∑' (i : ℕ), ↑↑μ (f i)
[PROOFSTEP]
exact μ.m_iUnion
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i)
⊢ ↑↑μ (⋃ (i : ι), f i) = ∑' (i : ι), ↑↑μ (f i)
[PROOFSTEP]
rcases exists_subordinate_pairwise_disjoint h hd with ⟨t, _ht_sub, ht_eq, htm, htd⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i)
t : ι → Set α
_ht_sub : ∀ (i : ι), t i ⊆ f i
ht_eq : ∀ (i : ι), f i =ᵐ[μ] t i
htm : ∀ (i : ι), MeasurableSet (t i)
htd : Pairwise (Disjoint on t)
⊢ ↑↑μ (⋃ (i : ι), f i) = ∑' (i : ι), ↑↑μ (f i)
[PROOFSTEP]
calc
  μ (⋃ i, f i) = μ (⋃ i, t i) := measure_congr (EventuallyEq.countable_iUnion ht_eq)
  _ = ∑' i, μ (t i) := (measure_iUnion htd htm)
  _ = ∑' i, μ (f i) := tsum_congr fun i => measure_congr (ht_eq _).symm
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ ↑↑μ (s ∪ t) = ↑↑μ s + ↑↑μ t
[PROOFSTEP]
rw [union_eq_iUnion, measure_iUnion₀, tsum_fintype, Fintype.sum_bool, cond, cond]
[GOAL]
case hd
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ Pairwise (AEDisjoint μ on fun b => bif b then s else t)
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ ∀ (i : Bool), NullMeasurableSet (bif i then s else t)
[PROOFSTEP]
exacts [(pairwise_on_bool AEDisjoint.symmetric).2 hd, fun b => Bool.casesOn b ht hs]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) = ↑↑μ s
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) ≤ ↑↑μ s
[PROOFSTEP]
rcases exists_measurable_superset μ s with ⟨s', hsub, hs'm, hs'⟩
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
s' : Set α
hsub : s ⊆ s'
hs'm : MeasurableSet s'
hs' : ↑↑μ s' = ↑↑μ s
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) ≤ ↑↑μ s
[PROOFSTEP]
replace hs'm : NullMeasurableSet s' μ := hs'm.nullMeasurableSet
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
s' : Set α
hsub : s ⊆ s'
hs' : ↑↑μ s' = ↑↑μ s
hs'm : NullMeasurableSet s'
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) ≤ ↑↑μ s
[PROOFSTEP]
calc
  μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t) :=
    add_le_add (measure_mono <| inter_subset_inter_left _ hsub) (measure_mono <| diff_subset_diff_left hsub)
  _ = μ (s' ∩ t ∪ s' \ t) :=
    (measure_union₀_aux (hs'm.inter ht) (hs'm.diff ht) <| (@disjoint_inf_sdiff _ s' t _).aedisjoint).symm
  _ = μ s' := (congr_arg μ (inter_union_diff _ _))
  _ = μ s := hs'
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ s ≤ ↑↑μ (s ∩ t) + ↑↑μ (s \ t)
[PROOFSTEP]
calc
  μ s = μ (s ∩ t ∪ s \ t) := by rw [inter_union_diff]
  _ ≤ μ (s ∩ t) + μ (s \ t) := measure_union_le _ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ s = ↑↑μ (s ∩ t ∪ s \ t)
[PROOFSTEP]
rw [inter_union_diff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ (s ∪ t) + ↑↑μ (s ∩ t) = ↑↑μ s + ↑↑μ t
[PROOFSTEP]
rw [← measure_inter_add_diff₀ (s ∪ t) ht, union_inter_cancel_right, union_diff_right, ← measure_inter_add_diff₀ s ht,
  add_comm, ← add_assoc, add_right_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
hs : NullMeasurableSet s
t : Set α
⊢ ↑↑μ (s ∪ t) + ↑↑μ (s ∩ t) = ↑↑μ s + ↑↑μ t
[PROOFSTEP]
rw [union_comm, inter_comm, measure_union_add_inter₀ t hs, add_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ ↑↑μ (s ∪ t) = ↑↑μ s + ↑↑μ t
[PROOFSTEP]
rw [← measure_union_add_inter₀ s ht, hd, add_zero]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
hd : AEDisjoint μ s t
⊢ ↑↑μ (s ∪ t) = ↑↑μ s + ↑↑μ t
[PROOFSTEP]
rw [union_comm, measure_union₀ hs (AEDisjoint.symm hd), add_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
hs : NullMeasurableSet s
⊢ ↑↑μ s + ↑↑μ sᶜ = ↑↑μ univ
[PROOFSTEP]
rw [← measure_union₀' hs aedisjoint_compl_right, union_compl_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝ : MeasurableSingletonClass (NullMeasurableSpace α)
s : Finset α
⊢ NullMeasurableSet ↑s
[PROOFSTEP]
apply Finset.measurableSet
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : α → β
hf : NullMeasurable f
hg : f =ᵐ[μ] g
s : Set β
hs : MeasurableSet s
x : α
hx : f x = g x
⊢ x ∈ f ⁻¹' s ↔ x ∈ g ⁻¹' s
[PROOFSTEP]
rw [mem_preimage, mem_preimage, hx]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s t : Set α
x✝ : MeasurableSpace α
μ : Measure α
⊢ OuterMeasure.trim ↑μ = ↑μ
[PROOFSTEP]
refine' le_antisymm (fun s => _) (@OuterMeasure.le_trim (NullMeasurableSpace α μ) _ _)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s✝ t : Set α
x✝ : MeasurableSpace α
μ : Measure α
s : Set (NullMeasurableSpace α)
⊢ ↑(OuterMeasure.trim ↑μ) s ≤ ↑↑μ s
[PROOFSTEP]
rw [@OuterMeasure.trim_eq_iInf (NullMeasurableSpace α μ) _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s✝ t : Set α
x✝ : MeasurableSpace α
μ : Measure α
s : Set (NullMeasurableSpace α)
⊢ ⨅ (t : Set (NullMeasurableSpace α)) (_ : s ⊆ t) (_ : MeasurableSet t), ↑↑μ t ≤ ↑↑μ s
[PROOFSTEP]
have : ∀ s, μ.toOuterMeasure s = μ s := by simp only [forall_const]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s✝ t : Set α
x✝ : MeasurableSpace α
μ : Measure α
s : Set (NullMeasurableSpace α)
⊢ ∀ (s : Set α), ↑↑μ s = ↑↑μ s
[PROOFSTEP]
simp only [forall_const]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s✝ t : Set α
x✝ : MeasurableSpace α
μ : Measure α
s : Set (NullMeasurableSpace α)
this : ∀ (s : Set α), ↑↑μ s = ↑↑μ s
⊢ ⨅ (t : Set (NullMeasurableSpace α)) (_ : s ⊆ t) (_ : MeasurableSet t), ↑↑μ t ≤ ↑↑μ s
[PROOFSTEP]
rw [this, measure_eq_iInf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s✝ t : Set α
x✝ : MeasurableSpace α
μ : Measure α
s : Set (NullMeasurableSpace α)
this : ∀ (s : Set α), ↑↑μ s = ↑↑μ s
⊢ ⨅ (t : Set (NullMeasurableSpace α)) (_ : s ⊆ t) (_ : MeasurableSet t), ↑↑μ t ≤
    ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑↑μ t
[PROOFSTEP]
apply iInf₂_mono
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s✝ t : Set α
x✝ : MeasurableSpace α
μ : Measure α
s : Set (NullMeasurableSpace α)
this : ∀ (s : Set α), ↑↑μ s = ↑↑μ s
⊢ ∀ (i : Set (NullMeasurableSpace α)), s ⊆ i → ⨅ (_ : MeasurableSet i), ↑↑μ i ≤ ⨅ (_ : MeasurableSet i), ↑↑μ i
[PROOFSTEP]
exact fun t _ht => iInf_mono' fun h => ⟨MeasurableSet.nullMeasurableSet h, le_rfl⟩
