[GOAL]
α : Type u_1
m0 : MeasurableSpace α
μ μ₁ μ₂ ν ν₁ ν₂ : Measure α
s t : Set α
hs : ↑↑μ s = 0
ht : ↑↑ν t = 0
hst : univ ⊆ s ∪ t
⊢ μ ⟂ₘ ν
[PROOFSTEP]
use toMeasurable μ s, measurableSet_toMeasurable _ _, (measure_toMeasurable _).trans hs
[GOAL]
case right
α : Type u_1
m0 : MeasurableSpace α
μ μ₁ μ₂ ν ν₁ ν₂ : Measure α
s t : Set α
hs : ↑↑μ s = 0
ht : ↑↑ν t = 0
hst : univ ⊆ s ∪ t
⊢ ↑↑ν (toMeasurable μ s)ᶜ = 0
[PROOFSTEP]
refine' measure_mono_null (fun x hx => (hst trivial).resolve_left fun hxs => hx _) ht
[GOAL]
case right
α : Type u_1
m0 : MeasurableSpace α
μ μ₁ μ₂ ν ν₁ ν₂ : Measure α
s t : Set α
hs : ↑↑μ s = 0
ht : ↑↑ν t = 0
hst : univ ⊆ s ∪ t
x : α
hx : x ∈ (toMeasurable μ s)ᶜ
hxs : x ∈ s
⊢ x ∈ toMeasurable μ s
[PROOFSTEP]
exact subset_toMeasurable _ _ hxs
[GOAL]
α : Type u_1
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
⊢ sum μ ⟂ₘ ν ↔ ∀ (i : ι), μ i ⟂ₘ ν
[PROOFSTEP]
refine' ⟨fun h i => h.mono (le_sum _ _) le_rfl, fun H => _⟩
[GOAL]
α : Type u_1
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
H : ∀ (i : ι), μ i ⟂ₘ ν
⊢ sum μ ⟂ₘ ν
[PROOFSTEP]
choose s hsm hsμ hsν using H
[GOAL]
α : Type u_1
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsν : ∀ (i : ι), ↑↑ν (s i)ᶜ = 0
⊢ sum μ ⟂ₘ ν
[PROOFSTEP]
refine' ⟨⋂ i, s i, MeasurableSet.iInter hsm, _, _⟩
[GOAL]
case refine'_1
α : Type u_1
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsν : ∀ (i : ι), ↑↑ν (s i)ᶜ = 0
⊢ ↑↑(sum μ) (⋂ (i : ι), s i) = 0
[PROOFSTEP]
rw [sum_apply _ (MeasurableSet.iInter hsm), ENNReal.tsum_eq_zero]
[GOAL]
case refine'_1
α : Type u_1
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsν : ∀ (i : ι), ↑↑ν (s i)ᶜ = 0
⊢ ∀ (i : ι), ↑↑(μ i) (⋂ (b : ι), s b) = 0
[PROOFSTEP]
exact fun i => measure_mono_null (iInter_subset _ _) (hsμ i)
[GOAL]
case refine'_2
α : Type u_1
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsν : ∀ (i : ι), ↑↑ν (s i)ᶜ = 0
⊢ ↑↑ν (⋂ (i : ι), s i)ᶜ = 0
[PROOFSTEP]
rwa [compl_iInter, measure_iUnion_null_iff]
[GOAL]
α : Type u_1
m0 : MeasurableSpace α
μ μ₁ μ₂ ν ν₁ ν₂ : Measure α
⊢ μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
[PROOFSTEP]
rw [← sum_cond, sum_left, Bool.forall_bool, cond, cond, and_comm]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
src✝ : OuterMeasure α := inducedOuterMeasure m (_ : MeasurableSet ∅) m0
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ ↑(inducedOuterMeasure m (_ : MeasurableSet ∅) m0) (iUnion f) =
    ∑' (i : ℕ), ↑(inducedOuterMeasure m (_ : MeasurableSet ∅) m0) (f i)
[PROOFSTEP]
rw [inducedOuterMeasure_eq m0 mU, mU hf hd]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
src✝ : OuterMeasure α := inducedOuterMeasure m (_ : MeasurableSet ∅) m0
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i)) = ∑' (i : ℕ), ↑(inducedOuterMeasure m (_ : MeasurableSet ∅) m0) (f i)
[PROOFSTEP]
congr
[GOAL]
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
src✝ : OuterMeasure α := inducedOuterMeasure m (_ : MeasurableSet ∅) m0
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ (fun i => m (f i) (_ : MeasurableSet (f i))) = fun i => ↑(inducedOuterMeasure m (_ : MeasurableSet ∅) m0) (f i)
[PROOFSTEP]
funext n
[GOAL]
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
src✝ : OuterMeasure α := inducedOuterMeasure m (_ : MeasurableSet ∅) m0
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
n : ℕ
⊢ m (f n) (_ : MeasurableSet (f n)) = ↑(inducedOuterMeasure m (_ : MeasurableSet ∅) m0) (f n)
[PROOFSTEP]
rw [inducedOuterMeasure_eq m0 mU]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
src✝ : OuterMeasure α := inducedOuterMeasure m (_ : MeasurableSet ∅) m0
⊢ OuterMeasure.trim (inducedOuterMeasure m (_ : MeasurableSet ∅) m0) = inducedOuterMeasure m (_ : MeasurableSet ∅) m0
[PROOFSTEP]
unfold OuterMeasure.trim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
src✝ : OuterMeasure α := inducedOuterMeasure m (_ : MeasurableSet ∅) m0
⊢ inducedOuterMeasure (fun s x => ↑(inducedOuterMeasure m (_ : MeasurableSet ∅) m0) s) (_ : MeasurableSet ∅)
      (_ : ↑(inducedOuterMeasure m (_ : MeasurableSet ∅) m0) ∅ = 0) =
    inducedOuterMeasure m (_ : MeasurableSet ∅) m0
[PROOFSTEP]
congr
[GOAL]
case e_m
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
src✝ : OuterMeasure α := inducedOuterMeasure m (_ : MeasurableSet ∅) m0
⊢ (fun s x => ↑(inducedOuterMeasure m (_ : MeasurableSet ∅) m0) s) = m
[PROOFSTEP]
funext s hs
[GOAL]
case e_m.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
src✝ : OuterMeasure α := inducedOuterMeasure m (_ : MeasurableSet ∅) m0
s : Set α
hs : MeasurableSet s
⊢ ↑(inducedOuterMeasure m (_ : MeasurableSet ∅) m0) s = m s hs
[PROOFSTEP]
exact inducedOuterMeasure_eq m0 mU hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
x✝¹ x✝ : Measure α
m₁ : OuterMeasure α
u₁ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → ↑m₁ (⋃ (i : ℕ), f i) = ∑' (i : ℕ), ↑m₁ (f i)
h₁ : OuterMeasure.trim m₁ = m₁
m₂ : OuterMeasure α
_u₂ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → ↑m₂ (⋃ (i : ℕ), f i) = ∑' (i : ℕ), ↑m₂ (f i)
_h₂ : OuterMeasure.trim m₂ = m₂
_h :
  ↑{ toOuterMeasure := m₁, m_iUnion := u₁, trimmed := h₁ } = ↑{ toOuterMeasure := m₂, m_iUnion := _u₂, trimmed := _h₂ }
⊢ { toOuterMeasure := m₁, m_iUnion := u₁, trimmed := h₁ } = { toOuterMeasure := m₂, m_iUnion := _u₂, trimmed := _h₂ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ₁ s = ↑↑μ₂ s
⊢ ↑μ₁ = ↑μ₂
[PROOFSTEP]
rw [← trimmed, OuterMeasure.trim_congr (h _), trimmed]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ μ₁ = μ₂ → ∀ (s : Set α), MeasurableSet s → ↑↑μ₁ s = ↑↑μ₂ s
[PROOFSTEP]
rintro rfl s _hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ : Measure α
s✝ s₁ s₂ t s : Set α
_hs : MeasurableSet s
⊢ ↑↑μ₁ s = ↑↑μ₁ s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
⊢ ↑↑μ s = ↑(OuterMeasure.trim ↑μ) s
[PROOFSTEP]
rw [μ.trimmed]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
⊢ ↑↑μ s = ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑↑μ t
[PROOFSTEP]
rw [measure_eq_trim, OuterMeasure.trim_eq_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
⊢ ↑↑μ s = ⨅ (t : { t // s ⊆ t ∧ MeasurableSet t }), ↑↑μ ↑t
[PROOFSTEP]
simp_rw [iInf_subtype, iInf_and, ← measure_eq_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
⊢ ↑↑μ s = extend (fun t _ht => ↑↑μ t) s
[PROOFSTEP]
rw [extend_eq]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
[PROOFSTEP]
exact hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s
[PROOFSTEP]
simpa only [← measure_eq_trim] using μ.toOuterMeasure.exists_measurable_superset_eq_trim s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Type u_5
inst✝¹ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
ι : Sort u_6
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), ↑↑(μ i) t = ↑↑(μ i) s
[PROOFSTEP]
simpa only [← measure_eq_trim] using
  OuterMeasure.exists_measurable_superset_forall_eq_trim (fun i => (μ i).toOuterMeasure) s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ ν : Measure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s ∧ ↑↑ν t = ↑↑ν s
[PROOFSTEP]
simpa only [Bool.forall_bool.trans and_comm] using exists_measurable_superset_forall_eq (fun b => cond b μ ν) s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
hs : Set.Countable s
f : β → Set α
⊢ ↑↑μ (⋃ (b : β) (_ : b ∈ s), f b) ≤ ∑' (p : ↑s), ↑↑μ (f ↑p)
[PROOFSTEP]
haveI := hs.to_subtype
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
hs : Set.Countable s
f : β → Set α
this : Countable ↑s
⊢ ↑↑μ (⋃ (b : β) (_ : b ∈ s), f b) ≤ ∑' (p : ↑s), ↑↑μ (f ↑p)
[PROOFSTEP]
rw [biUnion_eq_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
hs : Set.Countable s
f : β → Set α
this : Countable ↑s
⊢ ↑↑μ (⋃ (x : ↑s), f ↑x) ≤ ∑' (p : ↑s), ↑↑μ (f ↑p)
[PROOFSTEP]
apply measure_iUnion_le
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Finset β
f : β → Set α
⊢ ↑↑μ (⋃ (b : β) (_ : b ∈ s), f b) ≤ ∑ p in s, ↑↑μ (f p)
[PROOFSTEP]
rw [← Finset.sum_attach, Finset.attach_eq_univ, ← tsum_fintype]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Finset β
f : β → Set α
⊢ ↑↑μ (⋃ (b : β) (_ : b ∈ s), f b) ≤ ∑' (b : { x // x ∈ s }), ↑↑μ (f ↑b)
[PROOFSTEP]
exact measure_biUnion_le s.countable_toSet f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝¹ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
⊢ ↑↑μ (⋃ (b : β), f b) ≤ ∑ p : β, ↑↑μ (f p)
[PROOFSTEP]
convert measure_biUnion_finset_le Finset.univ f
[GOAL]
case h.e'_3.h.e'_3.h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝¹ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
x✝ : β
⊢ f x✝ = ⋃ (_ : x✝ ∈ Finset.univ), f x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
⊢ ↑↑μ (⋃ (i : β) (_ : i ∈ s), f i) < ⊤
[PROOFSTEP]
convert (measure_biUnion_finset_le hs.toFinset f).trans_lt _ using 3
[GOAL]
case h.e'_3.h.e'_3.h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
⊢ (fun i => ⋃ (_ : i ∈ s), f i) = fun b => ⋃ (_ : b ∈ Finite.toFinset hs), f b
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h.e'_3.h.e'_3.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
x✝¹ : β
x✝ : α
⊢ x✝ ∈ ⋃ (_ : x✝¹ ∈ s), f x✝¹ ↔ x✝ ∈ ⋃ (_ : x✝¹ ∈ Finite.toFinset hs), f x✝¹
[PROOFSTEP]
rw [Finite.mem_toFinset]
[GOAL]
case convert_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
⊢ ∑ p in Finite.toFinset hs, ↑↑μ (f p) < ⊤
[PROOFSTEP]
apply ENNReal.sum_lt_top
[GOAL]
case convert_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
⊢ ∀ (a : β), a ∈ Finite.toFinset hs → ↑↑μ (f a) ≠ ⊤
[PROOFSTEP]
simpa only [Finite.mem_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ ↑↑μ (s ∪ t) < ⊤ ↔ ↑↑μ s < ⊤ ∧ ↑↑μ t < ⊤
[PROOFSTEP]
refine' ⟨fun h => ⟨_, _⟩, fun h => measure_union_lt_top h.1 h.2⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : ↑↑μ (s ∪ t) < ⊤
⊢ ↑↑μ s < ⊤
[PROOFSTEP]
exact (measure_mono (Set.subset_union_left s t)).trans_lt h
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : ↑↑μ (s ∪ t) < ⊤
⊢ ↑↑μ t < ⊤
[PROOFSTEP]
exact (measure_mono (Set.subset_union_right s t)).trans_lt h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ ¬↑↑μ (s ∪ t) = ⊤ ↔ ¬(↑↑μ s = ⊤ ∨ ↑↑μ t = ⊤)
[PROOFSTEP]
simp only [← lt_top_iff_ne_top, ← Ne.def, not_or, measure_union_lt_top_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝¹ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable β
s : β → Set α
hs : ↑↑μ (⋃ (n : β), s n) ≠ 0
⊢ ∃ n, 0 < ↑↑μ (s n)
[PROOFSTEP]
contrapose! hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝¹ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable β
s : β → Set α
hs : ∀ (n : β), ↑↑μ (s n) ≤ 0
⊢ ↑↑μ (⋃ (n : β), s n) = 0
[PROOFSTEP]
exact measure_iUnion_null fun n => nonpos_iff_eq_zero.1 (hs n)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α✝
μ✝ μ₁ μ₂ : Measure α✝
s s₁ s₂ t : Set α✝
α : Type ?u.37668
m : MeasurableSpace α
μ : Measure α
⊢ univ ∈ {s | ↑↑μ sᶜ = 0}
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α✝
μ✝ μ₁ μ₂ : Measure α✝
s s₁ s₂ t : Set α✝
α : Type ?u.37668
m : MeasurableSpace α
μ : Measure α
x✝ y✝ : Set α
hs : x✝ ∈ {s | ↑↑μ sᶜ = 0}
ht : y✝ ∈ {s | ↑↑μ sᶜ = 0}
⊢ x✝ ∩ y✝ ∈ {s | ↑↑μ sᶜ = 0}
[PROOFSTEP]
simp only [compl_inter, mem_setOf_eq]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α✝
μ✝ μ₁ μ₂ : Measure α✝
s s₁ s₂ t : Set α✝
α : Type ?u.37668
m : MeasurableSpace α
μ : Measure α
x✝ y✝ : Set α
hs : x✝ ∈ {s | ↑↑μ sᶜ = 0}
ht : y✝ ∈ {s | ↑↑μ sᶜ = 0}
⊢ ↑↑μ (x✝ᶜ ∪ y✝ᶜ) = 0
[PROOFSTEP]
exact measure_union_null hs ht
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
⊢ sᶜ ∈ Measure.ae μ ↔ ↑↑μ s = 0
[PROOFSTEP]
simp only [mem_ae_iff, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ ∀ (S : Set (Set α)), Set.Countable S → (∀ (s : Set α), s ∈ S → s ∈ Measure.ae μ) → ⋂₀ S ∈ Measure.ae μ
[PROOFSTEP]
intro S hSc hS
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
S : Set (Set α)
hSc : Set.Countable S
hS : ∀ (s : Set α), s ∈ S → s ∈ Measure.ae μ
⊢ ⋂₀ S ∈ Measure.ae μ
[PROOFSTEP]
rw [mem_ae_iff, compl_sInter, sUnion_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
S : Set (Set α)
hSc : Set.Countable S
hS : ∀ (s : Set α), s ∈ S → s ∈ Measure.ae μ
⊢ ↑↑μ (⋃ (x : Set α) (_ : x ∈ S), xᶜ) = 0
[PROOFSTEP]
exact (measure_biUnion_null_iff hSc).2 hS
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
f g : α → ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ f ≤ᵐ[μ] g
[PROOFSTEP]
rw [Filter.EventuallyLE, ae_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
f g : α → ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ↑↑μ {a | ¬f a ≤ g a} = 0
[PROOFSTEP]
rw [ae_iff] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
f g : α → ℝ≥0∞
h : ↑↑μ {a | ¬f a < g a} = 0
⊢ ↑↑μ {a | ¬f a ≤ g a} = 0
[PROOFSTEP]
refine' measure_mono_null (fun x hx => _) h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
f g : α → ℝ≥0∞
h : ↑↑μ {a | ¬f a < g a} = 0
x : α
hx : x ∈ {a | ¬f a ≤ g a}
⊢ x ∈ {a | ¬f a < g a}
[PROOFSTEP]
exact not_lt.2 (le_of_lt (not_le.1 hx))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ (∀ᵐ (x : α) ∂μ, ¬x ∈ s) ↔ ↑↑μ s = 0
[PROOFSTEP]
simp only [ae_iff, Classical.not_not, setOf_mem_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → x ∈ t) ↔ ↑↑μ (s \ t) = 0
[PROOFSTEP]
simp [ae_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ ↑↑μ {a | a ∈ s ∧ ¬a ∈ t} = 0 ↔ ↑↑μ (s \ t) = 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ s ∪ t =ᵐ[μ] t ↔ ↑↑μ (s \ t) = 0
[PROOFSTEP]
simp [eventuallyLE_antisymm_iff, ae_le_set, union_diff_right, diff_eq_empty.2 (Set.subset_union_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ s \ t =ᵐ[μ] s ↔ ↑↑μ (s ∩ t) = 0
[PROOFSTEP]
simp [eventuallyLE_antisymm_iff, ae_le_set, diff_diff_right, diff_diff, diff_eq_empty.2 (Set.subset_union_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ s t : Set α
⊢ s =ᵐ[μ] t ↔ ↑↑μ (s \ t) = 0 ∧ ↑↑μ (t \ s) = 0
[PROOFSTEP]
simp [eventuallyLE_antisymm_iff, ae_le_set]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ s t : Set α
⊢ ↑↑μ (s ∆ t) = 0 ↔ s =ᵐ[μ] t
[PROOFSTEP]
simp [ae_eq_set, symmDiff_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ s t : Set α
⊢ sᶜ =ᵐ[μ] tᶜ ↔ s =ᵐ[μ] t
[PROOFSTEP]
simp only [← measure_symmDiff_eq_zero_iff, compl_symmDiff_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ s t : Set α
⊢ sᶜ =ᵐ[μ] t ↔ s =ᵐ[μ] tᶜ
[PROOFSTEP]
rw [← ae_eq_set_compl_compl, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s =ᵐ[μ] univ
⊢ s ∪ t =ᵐ[μ] univ
[PROOFSTEP]
convert ae_eq_set_union h (ae_eq_refl t)
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s =ᵐ[μ] univ
⊢ univ = univ ∪ t
[PROOFSTEP]
rw [univ_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] univ
⊢ s ∪ t =ᵐ[μ] univ
[PROOFSTEP]
convert ae_eq_set_union (ae_eq_refl s) h
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] univ
⊢ univ = s ∪ univ
[PROOFSTEP]
rw [union_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s =ᵐ[μ] ∅
⊢ s ∪ t =ᵐ[μ] t
[PROOFSTEP]
convert ae_eq_set_union h (ae_eq_refl t)
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s =ᵐ[μ] ∅
⊢ t = ∅ ∪ t
[PROOFSTEP]
rw [empty_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] ∅
⊢ s ∪ t =ᵐ[μ] s
[PROOFSTEP]
convert ae_eq_set_union (ae_eq_refl s) h
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] ∅
⊢ s = s ∪ ∅
[PROOFSTEP]
rw [union_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s =ᵐ[μ] univ
⊢ s ∩ t =ᵐ[μ] t
[PROOFSTEP]
convert ae_eq_set_inter h (ae_eq_refl t)
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s =ᵐ[μ] univ
⊢ t = univ ∩ t
[PROOFSTEP]
rw [univ_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] univ
⊢ s ∩ t =ᵐ[μ] s
[PROOFSTEP]
convert ae_eq_set_inter (ae_eq_refl s) h
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] univ
⊢ s = s ∩ univ
[PROOFSTEP]
rw [inter_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s =ᵐ[μ] ∅
⊢ s ∩ t =ᵐ[μ] ∅
[PROOFSTEP]
convert ae_eq_set_inter h (ae_eq_refl t)
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s =ᵐ[μ] ∅
⊢ ∅ = ∅ ∩ t
[PROOFSTEP]
rw [empty_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] ∅
⊢ s ∩ t =ᵐ[μ] ∅
[PROOFSTEP]
convert ae_eq_set_inter (ae_eq_refl s) h
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] ∅
⊢ ∅ = s ∩ ∅
[PROOFSTEP]
rw [inter_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝¹ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
M : Type u_6
inst✝ : One M
f : α → M
s : Set α
⊢ mulIndicator s f =ᵐ[μ] 1 ↔ ↑↑μ (s ∩ mulSupport f) = 0
[PROOFSTEP]
simp [EventuallyEq, eventually_iff, Measure.ae, compl_setOf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝¹ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
M : Type u_6
inst✝ : One M
f : α → M
s : Set α
⊢ ↑↑μ {a | a ∈ s ∧ ¬f a = 1} = 0 ↔ ↑↑μ (s ∩ mulSupport f) = 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
H : s ≤ᵐ[μ] t
⊢ ↑↑μ (s ∪ t) = ↑↑μ (t ∪ s \ t)
[PROOFSTEP]
rw [union_diff_self, Set.union_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
H : s ≤ᵐ[μ] t
⊢ ↑↑μ t + ↑↑μ (s \ t) = ↑↑μ t
[PROOFSTEP]
rw [ae_le_set.1 H, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
⊢ s ⊆ toMeasurable μ s
[PROOFSTEP]
rw [toMeasurable_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
⊢ s ⊆
    if h : ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s then Exists.choose h
    else
      if h' : ∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u) then Exists.choose h'
      else Exists.choose (_ : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s)
[PROOFSTEP]
split_ifs with hs h's
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
hs : ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
⊢ s ⊆ Exists.choose hs
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
hs : ¬∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u)
⊢ s ⊆ Exists.choose h's
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
hs : ¬∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ¬∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u)
⊢ s ⊆ Exists.choose (_ : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s)
[PROOFSTEP]
exacts [hs.choose_spec.fst, h's.choose_spec.fst, (exists_measurable_superset μ s).choose_spec.1]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
⊢ MeasurableSet (toMeasurable μ s)
[PROOFSTEP]
rw [toMeasurable_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
⊢ MeasurableSet
    (if h : ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s then Exists.choose h
    else
      if h' : ∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u) then Exists.choose h'
      else Exists.choose (_ : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s))
[PROOFSTEP]
split_ifs with hs h's
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
hs : ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
⊢ MeasurableSet (Exists.choose hs)
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
hs : ¬∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u)
⊢ MeasurableSet (Exists.choose h's)
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
hs : ¬∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ¬∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u)
⊢ MeasurableSet (Exists.choose (_ : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s))
[PROOFSTEP]
exacts [hs.choose_spec.snd.1, h's.choose_spec.snd.1, (exists_measurable_superset μ s).choose_spec.2.1]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
⊢ ↑↑μ (toMeasurable μ s) = ↑↑μ s
[PROOFSTEP]
rw [toMeasurable_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
⊢ ↑↑μ
      (if h : ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s then Exists.choose h
      else
        if h' : ∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u) then
          Exists.choose h'
        else Exists.choose (_ : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s)) =
    ↑↑μ s
[PROOFSTEP]
split_ifs with hs h's
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
hs : ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
⊢ ↑↑μ (Exists.choose hs) = ↑↑μ s
[PROOFSTEP]
exact measure_congr hs.choose_spec.snd.2
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
hs : ¬∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u)
⊢ ↑↑μ (Exists.choose h's) = ↑↑μ s
[PROOFSTEP]
simpa only [inter_univ] using h's.choose_spec.snd.2 univ MeasurableSet.univ
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
hs : ¬∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ¬∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u)
⊢ ↑↑μ (Exists.choose (_ : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s)) = ↑↑μ s
[PROOFSTEP]
exact (exists_measurable_superset μ s).choose_spec.2.2