-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem sigmaFinite_bot_iff (μ : @Measure α ⊥) : SigmaFinite μ ↔ IsFiniteMeasure μ

Proof state:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
⊢ μ univ < ⊤

Tactic:
by_cases h_univ_empty : (Set.univ : Set α) = ∅

Result:
case pos
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : univ = ∅
⊢ μ univ < ⊤

case neg
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
⊢ μ univ < ⊤

Proof state:
α : Type u_1
μ : Measure α
h : IsFiniteMeasure μ
⊢ SigmaFinite μ

Tactic:
haveI := h

Result:
α : Type u_1
μ : Measure α
h this : IsFiniteMeasure μ
⊢ SigmaFinite μ

Proof state:
α : Type u_1
μ : Measure α
⊢ SigmaFinite μ ↔ IsFiniteMeasure μ

Tactic:
refine
  ⟨fun h => ⟨?_⟩, fun h => by
    haveI := h
    infer_instance⟩

Result:
α : Type u_1
μ : Measure α
h : SigmaFinite μ
⊢ μ univ < ⊤

Proof state:
case pos
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : univ = ∅
⊢ 0 < ⊤

Tactic:
exact ENNReal.zero_ne_top.lt_top

Result:
no goals

Proof state:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
⊢ μ univ < ⊤

Tactic:
have hs_meas : ∀ i, MeasurableSet[⊥] (s i) := measurableSet_spanningSets μ

Result:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), MeasurableSet (s i)
⊢ μ univ < ⊤

Proof state:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
⊢ μ univ < ⊤

Tactic:
let s := spanningSets μ

Result:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
⊢ μ univ < ⊤

Proof state:
α : Type u_1
μ : Measure α
h : SigmaFinite μ
⊢ μ univ < ⊤

Tactic:
haveI : SigmaFinite μ := h

Result:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
⊢ μ univ < ⊤

Proof state:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
h_empty : ∀ (i : ℕ), s i = ∅
hs_univ : ∅ = univ
⊢ False

Tactic:
exact h_univ_empty hs_univ.symm

Result:
no goals

Proof state:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
⊢ ∃ i, s i = univ

Tactic:
by_contra! h_not_univ

Result:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
⊢ False

Proof state:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
⊢ μ univ < ⊤

Tactic:
have hs_univ : ⋃ i, s i = Set.univ := iUnion_spanningSets μ

Result:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
⊢ μ univ < ⊤

Proof state:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
⊢ False

Tactic:
have h_empty : ∀ i, s i = ∅ := by simpa [h_not_univ] using hs_meas

Result:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
h_empty : ∀ (i : ℕ), s i = ∅
⊢ False

Proof state:
case pos
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : univ = ∅
⊢ μ univ < ⊤

Tactic:
rw [h_univ_empty, measure_empty]

Result:
case pos
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : univ = ∅
⊢ 0 < ⊤

Proof state:
case neg.intro
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
i : ℕ
hsi : s i = univ
⊢ μ (s i) < ⊤

Tactic:
exact measure_spanningSets_lt_top μ i

Result:
no goals

Proof state:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
h_empty : ∀ (i : ℕ), s i = ∅
⊢ False

Tactic:
simp only [h_empty, iUnion_empty] at hs_univ

Result:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
h_empty : ∀ (i : ℕ), s i = ∅
hs_univ : ∅ = univ
⊢ False

Proof state:
case neg.intro
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
i : ℕ
hsi : s i = univ
⊢ μ univ < ⊤

Tactic:
rw [← hsi]

Result:
case neg.intro
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
i : ℕ
hsi : s i = univ
⊢ μ (s i) < ⊤

Proof state:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), MeasurableSet (s i)
⊢ μ univ < ⊤

Tactic:
simp_rw [MeasurableSpace.measurableSet_bot_iff] at hs_meas

Result:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
⊢ μ univ < ⊤

Proof state:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
⊢ ∀ (i : ℕ), s i = ∅

Tactic:
simpa [h_not_univ] using hs_meas

Result:
no goals

Proof state:
α : Type u_1
μ : Measure α
h this : IsFiniteMeasure μ
⊢ SigmaFinite μ

Tactic:
infer_instance

Result:
no goals

Proof state:
case neg
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
⊢ μ univ < ⊤

Tactic:
obtain ⟨i, hsi⟩ : ∃ i, s i = Set.univ := by
  by_contra! h_not_univ
  have h_empty : ∀ i, s i = ∅ := by simpa [h_not_univ] using hs_meas
  simp only [h_empty, iUnion_empty] at hs_univ
  exact h_univ_empty hs_univ.symm

Result:
case neg.intro
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
i : ℕ
hsi : s i = univ
⊢ μ univ < ⊤