α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
obs : {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
⊢ Set.Countable {i | 0 < ↑↑μ (As i)}
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
⊢ Set.Countable {i | 0 < ↑↑μ (As i)}
have obs : { i : ι | 0 < μ (As i) } ⊆ ⋃ n, { i : ι | 0 < μ (As i ∩ spanningSets μ n) } := by
  intro i i_in_nonzeroes
  by_contra con
  simp only [mem_iUnion, mem_setOf_eq, not_exists, not_lt, nonpos_iff_eq_zero] at *
  simp [(forall_measure_inter_spanningSets_eq_zero _).mp con] at i_in_nonzeroes
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
obs : {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
⊢ Set.Countable (⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)})
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
obs : {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
⊢ Set.Countable {i | 0 < ↑↑μ (As i)}
apply Countable.mono obs
case refine'_1
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
obs : {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
n : ℕ
⊢ ∀ (i : ι), MeasurableSet (As i ∩ spanningSets μ n)

case refine'_2
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
obs : {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
n : ℕ
⊢ Pairwise (Disjoint on fun i => As i ∩ spanningSets μ n)

case refine'_3
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
obs : {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
n : ℕ
⊢ ↑↑μ (⋃ (i : ι), As i ∩ spanningSets μ n) ≠ ⊤
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
obs : {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
⊢ Set.Countable (⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)})
refine' countable_iUnion fun n => countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top μ _ _ _
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
i : ι
i_in_nonzeroes : i ∈ {i | 0 < ↑↑μ (As i)}
⊢ i ∈ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
⊢ {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
intro i i_in_nonzeroes
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
i : ι
i_in_nonzeroes : i ∈ {i | 0 < ↑↑μ (As i)}
con : ¬i ∈ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
⊢ False
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
i : ι
i_in_nonzeroes : i ∈ {i | 0 < ↑↑μ (As i)}
⊢ i ∈ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
by_contra con
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
i : ι
i_in_nonzeroes : 0 < ↑↑μ (As i)
con : ∀ (x : ℕ), ↑↑μ (As i ∩ spanningSets μ x) = 0
⊢ False
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
i : ι
i_in_nonzeroes : i ∈ {i | 0 < ↑↑μ (As i)}
con : ¬i ∈ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
⊢ False
simp only [mem_iUnion, mem_setOf_eq, not_exists, not_lt, nonpos_iff_eq_zero] at *
no goals
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
i : ι
i_in_nonzeroes : 0 < ↑↑μ (As i)
con : ∀ (x : ℕ), ↑↑μ (As i ∩ spanningSets μ x) = 0
⊢ False
simp [(forall_measure_inter_spanningSets_eq_zero _).mp con] at i_in_nonzeroes
no goals
case refine'_1
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
obs : {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
n : ℕ
⊢ ∀ (i : ι), MeasurableSet (As i ∩ spanningSets μ n)
exact fun i => MeasurableSet.inter (As_mble i) (measurable_spanningSets μ n)
no goals
case refine'_2
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
obs : {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
n : ℕ
⊢ Pairwise (Disjoint on fun i => As i ∩ spanningSets μ n)
exact fun i j i_ne_j b hbi hbj =>
  As_disj i_ne_j (hbi.trans (inter_subset_left _ _)) (hbj.trans (inter_subset_left _ _))
case refine'_3
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
obs : {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
n : ℕ
⊢ (⋃ (i : ι), As i ∩ spanningSets μ n) ⊆ spanningSets μ n
case refine'_3
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
obs : {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
n : ℕ
⊢ ↑↑μ (⋃ (i : ι), As i ∩ spanningSets μ n) ≠ ⊤
refine' (lt_of_le_of_lt (measure_mono _) (measure_spanningSets_lt_top μ n)).ne
no goals
case refine'_3
α : Type u_2
β : Type ?u.742871
γ : Type ?u.742874
δ : Type ?u.742877
ι✝ : Type ?u.742880
R : Type ?u.742883
R' : Type ?u.742886
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
obs : {i | 0 < ↑↑μ (As i)} ⊆ ⋃ (n : ℕ), {i | 0 < ↑↑μ (As i ∩ spanningSets μ n)}
n : ℕ
⊢ (⋃ (i : ι), As i ∩ spanningSets μ n) ⊆ spanningSets μ n
exact iUnion_subset fun i => inter_subset_right _ _