α : Type u_1
β : Type ?u.731841
γ : Type ?u.731844
δ : Type ?u.731847
ι : Type ?u.731850
R : Type ?u.731853
R' : Type ?u.731856
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's✝ : r < ↑↑μ s
h's : ∃ i, r < ↑↑(restrict μ (spanningSets μ i)) s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < ↑↑μ t ∧ ↑↑μ t < ⊤
α : Type u_1
β : Type ?u.731841
γ : Type ?u.731844
δ : Type ?u.731847
ι : Type ?u.731850
R : Type ?u.731853
R' : Type ?u.731856
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < ↑↑μ s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < ↑↑μ t ∧ ↑↑μ t < ⊤
rw [← iSup_restrict_spanningSets hs,
  @lt_iSup_iff _ _ _ r fun i : ℕ => μ.restrict (spanningSets μ i) s] at h's
case intro
α : Type u_1
β : Type ?u.731841
γ : Type ?u.731844
δ : Type ?u.731847
ι : Type ?u.731850
R : Type ?u.731853
R' : Type ?u.731856
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < ↑↑μ s
n : ℕ
hn : r < ↑↑(restrict μ (spanningSets μ n)) s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < ↑↑μ t ∧ ↑↑μ t < ⊤
α : Type u_1
β : Type ?u.731841
γ : Type ?u.731844
δ : Type ?u.731847
ι : Type ?u.731850
R : Type ?u.731853
R' : Type ?u.731856
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's✝ : r < ↑↑μ s
h's : ∃ i, r < ↑↑(restrict μ (spanningSets μ i)) s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < ↑↑μ t ∧ ↑↑μ t < ⊤
rcases h's with ⟨n, hn⟩
case intro
α : Type u_1
β : Type ?u.731841
γ : Type ?u.731844
δ : Type ?u.731847
ι : Type ?u.731850
R : Type ?u.731853
R' : Type ?u.731856
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < ↑↑μ s
n : ℕ
hn : r < ↑↑μ (s ∩ spanningSets μ n)
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < ↑↑μ t ∧ ↑↑μ t < ⊤
case intro
α : Type u_1
β : Type ?u.731841
γ : Type ?u.731844
δ : Type ?u.731847
ι : Type ?u.731850
R : Type ?u.731853
R' : Type ?u.731856
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < ↑↑μ s
n : ℕ
hn : r < ↑↑(restrict μ (spanningSets μ n)) s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < ↑↑μ t ∧ ↑↑μ t < ⊤
simp only [restrict_apply hs] at hn
case intro
α : Type u_1
β : Type ?u.731841
γ : Type ?u.731844
δ : Type ?u.731847
ι : Type ?u.731850
R : Type ?u.731853
R' : Type ?u.731856
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < ↑↑μ s
n : ℕ
hn : r < ↑↑μ (s ∩ spanningSets μ n)
⊢ ↑↑μ (s ∩ spanningSets μ n) < ⊤
case intro
α : Type u_1
β : Type ?u.731841
γ : Type ?u.731844
δ : Type ?u.731847
ι : Type ?u.731850
R : Type ?u.731853
R' : Type ?u.731856
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < ↑↑μ s
n : ℕ
hn : r < ↑↑μ (s ∩ spanningSets μ n)
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < ↑↑μ t ∧ ↑↑μ t < ⊤
refine'
  ⟨s ∩ spanningSets μ n, hs.inter (measurable_spanningSets _ _), inter_subset_left _ _, hn, _⟩
no goals
case intro
α : Type u_1
β : Type ?u.731841
γ : Type ?u.731844
δ : Type ?u.731847
ι : Type ?u.731850
R : Type ?u.731853
R' : Type ?u.731856
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < ↑↑μ s
n : ℕ
hn : r < ↑↑μ (s ∩ spanningSets μ n)
⊢ ↑↑μ (s ∩ spanningSets μ n) < ⊤
exact (measure_mono (inter_subset_right _ _)).trans_lt (measure_spanningSets_lt_top _ _)