-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem countable_meas_pos_of_disjoint_iUnion₀ {ι : Type*} {_ : MeasurableSpace α} {μ : Measure α}
    [SFinite μ] {As : ι → Set α} (As_mble : ∀ i : ι, NullMeasurableSet (As i) μ)
    (As_disj : Pairwise (AEDisjoint μ on As)) :
    Set.Countable { i : ι | 0 < μ (As i) }

Proof state:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
⊢ (⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}).Countable

Tactic:
refine countable_iUnion fun n ↦ ?_

Result:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
n : ℕ
⊢ {i | 0 < (sfiniteSeq μ n) (As i)}.Countable

Proof state:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
hi : 0 < ∑' (i : ℕ), 0
⊢ False

Tactic:
simp at hi

Result:
no goals

Proof state:
case As_mble
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
n : ℕ
⊢ ∀ (i : ι), NullMeasurableSet (As i) (sfiniteSeq μ n)

Tactic:
exact fun i ↦ (As_mble i).mono (le_sum _ _)

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : i ∈ {i | 0 < (sum (sfiniteSeq μ)) (As i)}
⊢ i ∈ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}

Tactic:
by_contra con

Result:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : i ∈ {i | 0 < (sum (sfiniteSeq μ)) (As i)}
con : i ∉ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
⊢ False

Proof state:
case Union_As_finite
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
n : ℕ
⊢ (sfiniteSeq μ n) (⋃ i, As i) ≠ ⊤

Tactic:
exact measure_ne_top _ (⋃ i, As i)

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
⊢ {i | 0 < (sum (sfiniteSeq μ)) (As i)}.Countable

Tactic:
apply Countable.mono obs

Result:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
⊢ (⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}).Countable

Proof state:
case hs
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : 0 < (sum (sfiniteSeq μ)) (As i)
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
⊢ NullMeasurableSet (As i) (sum (sfiniteSeq μ))

Tactic:
exact As_mble i

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
⊢ {i | 0 < μ (As i)}.Countable

Tactic:
rw [← sum_sfiniteSeq μ] at As_disj As_mble ⊢

Result:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
⊢ {i | 0 < (sum (sfiniteSeq μ)) (As i)}.Countable

Proof state:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
n : ℕ
⊢ {i | 0 < (sfiniteSeq μ n) (As i)}.Countable

Tactic:
apply countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀

Result:
case As_mble
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
n : ℕ
⊢ ∀ (i : ι), NullMeasurableSet (As i) (sfiniteSeq μ n)

case As_disj
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
n : ℕ
⊢ Pairwise (AEDisjoint (sfiniteSeq μ n) on As)

case Union_As_finite
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
n : ℕ
⊢ (sfiniteSeq μ n) (⋃ i, As i) ≠ ⊤

Proof state:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : 0 < ∑' (i_1 : ℕ), (sfiniteSeq μ i_1) (As i)
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
⊢ False

Tactic:
simp_rw [con] at hi

Result:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
hi : 0 < ∑' (i : ℕ), 0
⊢ False

Proof state:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
⊢ {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}

Tactic:
intro i hi

Result:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : i ∈ {i | 0 < (sum (sfiniteSeq μ)) (As i)}
⊢ i ∈ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}