α : Type u_2
β : Type ?u.734278
γ : Type ?u.734281
δ : Type ?u.734284
ι✝ : Type ?u.734287
R : Type ?u.734290
R' : Type ?u.734293
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
ε : ℝ≥0∞
ε_pos : 0 < ε
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
Union_As_finite : ↑↑μ (⋃ (i : ι), As i) ≠ ⊤
con : ¬Set.Finite {i | ε ≤ ↑↑μ (As i)}
⊢ False
α : Type u_2
β : Type ?u.734278
γ : Type ?u.734281
δ : Type ?u.734284
ι✝ : Type ?u.734287
R : Type ?u.734290
R' : Type ?u.734293
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
ε : ℝ≥0∞
ε_pos : 0 < ε
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
Union_As_finite : ↑↑μ (⋃ (i : ι), As i) ≠ ⊤
⊢ Set.Finite {i | ε ≤ ↑↑μ (As i)}
by_contra con
α : Type u_2
β : Type ?u.734278
γ : Type ?u.734281
δ : Type ?u.734284
ι✝ : Type ?u.734287
R : Type ?u.734290
R' : Type ?u.734293
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
ε : ℝ≥0∞
ε_pos : 0 < ε
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
Union_As_finite : ↑↑μ (⋃ (i : ι), As i) ≠ ⊤
con : ¬Set.Finite {i | ε ≤ ↑↑μ (As i)}
aux : (∑' (i : ι), ↑↑μ (As i)) < ⊤
⊢ False
α : Type u_2
β : Type ?u.734278
γ : Type ?u.734281
δ : Type ?u.734284
ι✝ : Type ?u.734287
R : Type ?u.734290
R' : Type ?u.734293
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
ε : ℝ≥0∞
ε_pos : 0 < ε
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
Union_As_finite : ↑↑μ (⋃ (i : ι), As i) ≠ ⊤
con : ¬Set.Finite {i | ε ≤ ↑↑μ (As i)}
⊢ False
have aux :=
  lt_of_le_of_lt (tsum_meas_le_meas_iUnion_of_disjoint μ As_mble As_disj)
    (lt_top_iff_ne_top.mpr Union_As_finite)
no goals
α : Type u_2
β : Type ?u.734278
γ : Type ?u.734281
δ : Type ?u.734284
ι✝ : Type ?u.734287
R : Type ?u.734290
R' : Type ?u.734293
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ι : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
ε : ℝ≥0∞
ε_pos : 0 < ε
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
Union_As_finite : ↑↑μ (⋃ (i : ι), As i) ≠ ⊤
con : ¬Set.Finite {i | ε ≤ ↑↑μ (As i)}
aux : (∑' (i : ι), ↑↑μ (As i)) < ⊤
⊢ False
exact con (ENNReal.finite_const_le_of_tsum_ne_top aux.ne ε_pos.ne.symm)