α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U✝ : Set α
ε : ℝ≥0∞
q' : Set α → Prop
H : InnerRegular μ p q
H' : InnerRegular μ q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < ↑↑μ U
⊢ ∃ K, K ⊆ U ∧ p K ∧ r < ↑↑μ K
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
q' : Set α → Prop
H : InnerRegular μ p q
H' : InnerRegular μ q q'
⊢ InnerRegular μ p q'
intro U hU r hr
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U✝ : Set α
ε : ℝ≥0∞
q' : Set α → Prop
H : InnerRegular μ p q
H' : InnerRegular μ q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < ↑↑μ U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < ↑↑μ F
⊢ ∃ K, K ⊆ U ∧ p K ∧ r < ↑↑μ K
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U✝ : Set α
ε : ℝ≥0∞
q' : Set α → Prop
H : InnerRegular μ p q
H' : InnerRegular μ q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < ↑↑μ U
⊢ ∃ K, K ⊆ U ∧ p K ∧ r < ↑↑μ K
rcases H' hU r hr with ⟨F, hFU, hqF, hF⟩
case intro.intro.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U✝ : Set α
ε : ℝ≥0∞
q' : Set α → Prop
H : InnerRegular μ p q
H' : InnerRegular μ q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < ↑↑μ U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < ↑↑μ F
K : Set α
hKF : K ⊆ F
hpK : p K
hrK : r < ↑↑μ K
⊢ ∃ K, K ⊆ U ∧ p K ∧ r < ↑↑μ K
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U✝ : Set α
ε : ℝ≥0∞
q' : Set α → Prop
H : InnerRegular μ p q
H' : InnerRegular μ q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < ↑↑μ U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < ↑↑μ F
⊢ ∃ K, K ⊆ U ∧ p K ∧ r < ↑↑μ K
rcases H hqF _ hF with ⟨K, hKF, hpK, hrK⟩
no goals
case intro.intro.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U✝ : Set α
ε : ℝ≥0∞
q' : Set α → Prop
H : InnerRegular μ p q
H' : InnerRegular μ q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < ↑↑μ U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < ↑↑μ F
K : Set α
hKF : K ⊆ F
hpK : p K
hrK : r < ↑↑μ K
⊢ ∃ K, K ⊆ U ∧ p K ∧ r < ↑↑μ K
exact ⟨K, hKF.trans hFU, hpK, hrK⟩