α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
h : SigmaFinite μ
⊢ ↑↑μ univ < ⊤
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
⊢ SigmaFinite μ ↔ IsFiniteMeasure μ
refine'
  ⟨fun h => ⟨_⟩, fun h => by
    haveI := h
    infer_instance⟩
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
h this : SigmaFinite μ
⊢ ↑↑μ univ < ⊤
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
h : SigmaFinite μ
⊢ ↑↑μ univ < ⊤
haveI : SigmaFinite μ := h
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
⊢ ↑↑μ univ < ⊤
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
h this : SigmaFinite μ
⊢ ↑↑μ univ < ⊤
let s := spanningSets μ
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
⊢ ↑↑μ univ < ⊤
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
⊢ ↑↑μ univ < ⊤
have hs_univ : (⋃ i, s i) = Set.univ := iUnion_spanningSets μ
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), MeasurableSet (s i)
⊢ ↑↑μ univ < ⊤
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
⊢ ↑↑μ univ < ⊤
have hs_meas : ∀ i, MeasurableSet[⊥] (s i) := measurable_spanningSets μ
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
⊢ ↑↑μ univ < ⊤
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), MeasurableSet (s i)
⊢ ↑↑μ univ < ⊤
simp_rw [MeasurableSpace.measurableSet_bot_iff] at hs_meas
case inl
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : univ = ∅
⊢ ↑↑μ univ < ⊤

case inr
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
⊢ ↑↑μ univ < ⊤
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
⊢ ↑↑μ univ < ⊤
by_cases h_univ_empty : Set.univ = ∅
case inr.intro
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
i : ℕ
hsi : s i = univ
⊢ ↑↑μ univ < ⊤
case inr
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
⊢ ↑↑μ univ < ⊤
obtain ⟨i, hsi⟩ : ∃ i, s i = Set.univ := by
  by_contra h_not_univ
  push_neg  at h_not_univ
  have h_empty : ∀ i, s i = ∅ := by simpa [h_not_univ] using hs_meas
  simp [h_empty] at hs_univ
  exact h_univ_empty hs_univ.symm
case inr.intro
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
i : ℕ
hsi : s i = univ
⊢ ↑↑μ (s i) < ⊤
case inr.intro
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
i : ℕ
hsi : s i = univ
⊢ ↑↑μ univ < ⊤
rw [← hsi]
no goals
case inr.intro
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
i : ℕ
hsi : s i = univ
⊢ ↑↑μ (s i) < ⊤
exact measure_spanningSets_lt_top μ i
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
h this : IsFiniteMeasure μ
⊢ SigmaFinite μ
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
h : IsFiniteMeasure μ
⊢ SigmaFinite μ
haveI := h
no goals
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
h this : IsFiniteMeasure μ
⊢ SigmaFinite μ
infer_instance
case inl
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : univ = ∅
⊢ 0 < ⊤
case inl
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : univ = ∅
⊢ ↑↑μ univ < ⊤
rw [h_univ_empty, @measure_empty α ⊥]
no goals
case inl
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : univ = ∅
⊢ 0 < ⊤
exact ENNReal.zero_ne_top.lt_top
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ¬∃ i, s i = univ
⊢ False
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
⊢ ∃ i, s i = univ
by_contra h_not_univ
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), spanningSets μ i ≠ univ
⊢ False
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ¬∃ i, s i = univ
⊢ False
push_neg  at h_not_univ
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), spanningSets μ i ≠ univ
h_empty : ∀ (i : ℕ), s i = ∅
⊢ False
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), spanningSets μ i ≠ univ
⊢ False
have h_empty : ∀ i, s i = ∅ := by simpa [h_not_univ] using hs_meas
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), spanningSets μ i ≠ univ
h_empty : ∀ (i : ℕ), s i = ∅
hs_univ : ∅ = univ
⊢ False
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), spanningSets μ i ≠ univ
h_empty : ∀ (i : ℕ), s i = ∅
⊢ False
simp [h_empty] at hs_univ
no goals
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), spanningSets μ i ≠ univ
h_empty : ∀ (i : ℕ), s i = ∅
hs_univ : ∅ = univ
⊢ False
exact h_univ_empty hs_univ.symm
no goals
α : Type u_1
β : Type ?u.760205
γ : Type ?u.760208
δ : Type ?u.760211
ι : Type ?u.760214
R : Type ?u.760217
R' : Type ?u.760220
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : (⋃ (i : ℕ), s i) = univ
hs_meas : ∀ (i : ℕ), spanningSets μ i = ∅ ∨ spanningSets μ i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), spanningSets μ i ≠ univ
⊢ ∀ (i : ℕ), s i = ∅
simpa [h_not_univ] using hs_meas