α : Type u_1
β : Type ?u.3499652
γ : Type ?u.3499655
δ : Type ?u.3499658
ι : Type ?u.3499661
R : Type ?u.3499664
R' : Type ?u.3499667
m✝ m0✝ : MeasurableSpace α
μ✝ : Measure α
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (trim μ (_ : m₂ ≤ m0))
x✝ : Type u_1
⊢ SigmaFinite (trim μ hm)
α : Type u_1
β : Type ?u.3499652
γ : Type ?u.3499655
δ : Type ?u.3499658
ι : Type ?u.3499661
R : Type ?u.3499664
R' : Type ?u.3499667
m✝ m0✝ : MeasurableSpace α
μ✝ : Measure α
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (trim μ (_ : m₂ ≤ m0))
⊢ SigmaFinite (trim μ hm)
have _ := Measure.FiniteSpanningSetsIn (μ.trim (hm₂.trans hm)) Set.univ
case refine'_1
α : Type u_1
β : Type ?u.3499652
γ : Type ?u.3499655
δ : Type ?u.3499658
ι : Type ?u.3499661
R : Type ?u.3499664
R' : Type ?u.3499667
m✝ m0✝ : MeasurableSpace α
μ✝ : Measure α
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (trim μ (_ : m₂ ≤ m0))
x✝ : Type u_1
⊢ Set (Set α)

case refine'_2
α : Type u_1
β : Type ?u.3499652
γ : Type ?u.3499655
δ : Type ?u.3499658
ι : Type ?u.3499661
R : Type ?u.3499664
R' : Type ?u.3499667
m✝ m0✝ : MeasurableSpace α
μ✝ : Measure α
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (trim μ (_ : m₂ ≤ m0))
x✝ : Type u_1
⊢ FiniteSpanningSetsIn (trim μ hm) ?refine'_1
α : Type u_1
β : Type ?u.3499652
γ : Type ?u.3499655
δ : Type ?u.3499658
ι : Type ?u.3499661
R : Type ?u.3499664
R' : Type ?u.3499667
m✝ m0✝ : MeasurableSpace α
μ✝ : Measure α
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (trim μ (_ : m₂ ≤ m0))
x✝ : Type u_1
⊢ SigmaFinite (trim μ hm)
refine' Measure.FiniteSpanningSetsIn.sigmaFinite _
no goals
case refine'_1
α : Type u_1
β : Type ?u.3499652
γ : Type ?u.3499655
δ : Type ?u.3499658
ι : Type ?u.3499661
R : Type ?u.3499664
R' : Type ?u.3499667
m✝ m0✝ : MeasurableSpace α
μ✝ : Measure α
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (trim μ (_ : m₂ ≤ m0))
x✝ : Type u_1
⊢ Set (Set α)
exact Set.univ
case refine'_2
α : Type u_1
β : Type ?u.3499652
γ : Type ?u.3499655
δ : Type ?u.3499658
ι : Type ?u.3499661
R : Type ?u.3499664
R' : Type ?u.3499667
m✝ m0✝ : MeasurableSpace α
μ✝ : Measure α
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (trim μ (_ : m₂ ≤ m0))
x✝ : Type u_1
i : ℕ
⊢ ↑↑(trim μ hm) (spanningSets (trim μ (_ : m₂ ≤ m0)) i) < ⊤
case refine'_2
α : Type u_1
β : Type ?u.3499652
γ : Type ?u.3499655
δ : Type ?u.3499658
ι : Type ?u.3499661
R : Type ?u.3499664
R' : Type ?u.3499667
m✝ m0✝ : MeasurableSpace α
μ✝ : Measure α
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (trim μ (_ : m₂ ≤ m0))
x✝ : Type u_1
⊢ FiniteSpanningSetsIn (trim μ hm) univ
refine'
  { set := spanningSets (μ.trim (hm₂.trans hm))
    set_mem := fun _ => Set.mem_univ _
    finite := fun i => _ spanning := iUnion_spanningSets _ }
no goals
case refine'_2
α : Type u_1
β : Type ?u.3499652
γ : Type ?u.3499655
δ : Type ?u.3499658
ι : Type ?u.3499661
R : Type ?u.3499664
R' : Type ?u.3499667
m✝ m0✝ : MeasurableSpace α
μ✝ : Measure α
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (trim μ (_ : m₂ ≤ m0))
x✝ : Type u_1
i : ℕ
⊢ ↑↑(trim μ hm) (spanningSets (trim μ (_ : m₂ ≤ m0)) i) < ⊤
calc
  (μ.trim hm) (spanningSets (μ.trim (hm₂.trans hm)) i) =
      ((μ.trim hm).trim hm₂) (spanningSets (μ.trim (hm₂.trans hm)) i) :=
    by rw [@trim_measurableSet_eq α m₂ m (μ.trim hm) _ hm₂ (measurable_spanningSets _ _)]
  _ = (μ.trim (hm₂.trans hm)) (spanningSets (μ.trim (hm₂.trans hm)) i) := by
    rw [@trim_trim _ _ μ _ _ hm₂ hm]
  _ < ∞ := measure_spanningSets_lt_top _ _
no goals
α : Type u_1
β : Type ?u.3499652
γ : Type ?u.3499655
δ : Type ?u.3499658
ι : Type ?u.3499661
R : Type ?u.3499664
R' : Type ?u.3499667
m✝ m0✝ : MeasurableSpace α
μ✝ : Measure α
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (trim μ (_ : m₂ ≤ m0))
x✝ : Type u_1
i : ℕ
⊢ ↑↑(trim μ hm) (spanningSets (trim μ (_ : m₂ ≤ m0)) i) =
    ↑↑(trim (trim μ hm) hm₂) (spanningSets (trim μ (_ : m₂ ≤ m0)) i)
rw [@trim_measurableSet_eq α m₂ m (μ.trim hm) _ hm₂ (measurable_spanningSets _ _)]
no goals
α : Type u_1
β : Type ?u.3499652
γ : Type ?u.3499655
δ : Type ?u.3499658
ι : Type ?u.3499661
R : Type ?u.3499664
R' : Type ?u.3499667
m✝ m0✝ : MeasurableSpace α
μ✝ : Measure α
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (trim μ (_ : m₂ ≤ m0))
x✝ : Type u_1
i : ℕ
⊢ ↑↑(trim (trim μ hm) hm₂) (spanningSets (trim μ (_ : m₂ ≤ m0)) i) =
    ↑↑(trim μ (_ : m₂ ≤ m0)) (spanningSets (trim μ (_ : m₂ ≤ m0)) i)
rw [@trim_trim _ _ μ _ _ hm₂ hm]