[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
⊢ ∃ t, (∀ (i : ι), MeasurableSet (t i)) ∧ (∀ (i : ι), ↑↑μ (t i) = 0) ∧ Pairwise (Disjoint on fun i => s i \ t i)
[PROOFSTEP]
refine'
  ⟨fun i => toMeasurable μ (s i ∩ ⋃ j ∈ ({ i }ᶜ : Set ι), s j), fun i => measurableSet_toMeasurable _ _, fun i => _, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i : ι
⊢ ↑↑μ ((fun i => toMeasurable μ (s i ∩ ⋃ (j : ι) (_ : j ∈ {i}ᶜ), s j)) i) = 0
[PROOFSTEP]
simp only [measure_toMeasurable, inter_iUnion]
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i : ι
⊢ ↑↑μ (⋃ (i_1 : ι) (_ : i_1 ∈ {i}ᶜ), s i ∩ s i_1) = 0
[PROOFSTEP]
exact (measure_biUnion_null_iff <| to_countable _).2 fun j hj => hd (Ne.symm hj)
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
⊢ Pairwise (Disjoint on fun i => s i \ (fun i => toMeasurable μ (s i ∩ ⋃ (j : ι) (_ : j ∈ {i}ᶜ), s j)) i)
[PROOFSTEP]
simp only [Pairwise, disjoint_left, onFun, mem_diff, not_and, and_imp, Classical.not_not]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
⊢ ∀ ⦃i j : ι⦄,
    i ≠ j →
      ∀ ⦃a : α⦄,
        a ∈ s i →
          ¬a ∈ toMeasurable μ (s i ∩ ⋃ (j : ι) (_ : j ∈ {i}ᶜ), s j) →
            a ∈ s j → a ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι) (_ : j_1 ∈ {j}ᶜ), s j_1)
[PROOFSTEP]
intro i j hne x hi hU hj
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
hU : ¬x ∈ toMeasurable μ (s i ∩ ⋃ (j : ι) (_ : j ∈ {i}ᶜ), s j)
hj : x ∈ s j
⊢ x ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι) (_ : j_1 ∈ {j}ᶜ), s j_1)
[PROOFSTEP]
replace hU : x ∉ s i ∩ iUnion λ j => iUnion λ _ => s j := λ h => hU (subset_toMeasurable _ _ h)
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
hj : x ∈ s j
hU : ¬x ∈ s i ∩ ⋃ (j : ι) (_ : j ∈ {i}ᶜ), s j
⊢ x ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι) (_ : j_1 ∈ {j}ᶜ), s j_1)
[PROOFSTEP]
simp only [mem_inter_iff, mem_iUnion, not_and, not_exists] at hU 
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
hj : x ∈ s j
hU : x ∈ s i → ∀ (x_1 : ι), x_1 ∈ {i}ᶜ → ¬x ∈ s x_1
⊢ x ∈ toMeasurable μ (s j ∩ ⋃ (j_1 : ι) (_ : j_1 ∈ {j}ᶜ), s j_1)
[PROOFSTEP]
exact (hU hi j hne.symm hj).elim
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : AEDisjoint μ s t
⊢ AEDisjoint μ t s
[PROOFSTEP]
rwa [AEDisjoint, inter_comm]
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : Disjoint s t
⊢ AEDisjoint μ s t
[PROOFSTEP]
rw [AEDisjoint, disjoint_iff_inter_eq_empty.1 h, measure_empty]
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
⊢ AEDisjoint μ (⋃ (i : ι), s i) t ↔ ∀ (i : ι), AEDisjoint μ (s i) t
[PROOFSTEP]
simp only [AEDisjoint, iUnion_inter, measure_iUnion_null_iff]
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t✝ u v : Set α
inst✝ : Countable ι
t : ι → Set α
⊢ AEDisjoint μ s (⋃ (i : ι), t i) ↔ ∀ (i : ι), AEDisjoint μ s (t i)
[PROOFSTEP]
simp only [AEDisjoint, inter_iUnion, measure_iUnion_null_iff]
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
⊢ AEDisjoint μ (s ∪ t) u ↔ AEDisjoint μ s u ∧ AEDisjoint μ t u
[PROOFSTEP]
simp [union_eq_iUnion, and_comm]
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
⊢ AEDisjoint μ s (t ∪ u) ↔ AEDisjoint μ s t ∧ AEDisjoint μ s u
[PROOFSTEP]
simp [union_eq_iUnion, and_comm]
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : AEDisjoint μ s t
x : α
hx : x ∈ s \ toMeasurable μ (s ∩ t)
⊢ x ∈ ?m.9910 h \ t
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : AEDisjoint μ s t
x : α
hx : x ∈ s \ toMeasurable μ (s ∩ t)
⊢ x ∈ ?m.9910 h ∧ ¬x ∈ t
[PROOFSTEP]
exact ⟨hx.1, fun hxt => hx.2 <| subset_toMeasurable _ _ ⟨hx.1, hxt⟩⟩
