α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U✝ : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < ↑↑(c • μ) U
⊢ ∃ K, K ⊆ U ∧ p K ∧ r < ↑↑(c • μ) K
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
c : ℝ≥0∞
⊢ InnerRegular (c • μ) p q
intro U hU r hr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U✝ : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < c * ⨆ (K : Set α) (_ : K ⊆ U) (_ : p K), ↑↑μ K
⊢ ∃ K, K ⊆ U ∧ p K ∧ r < ↑↑(c • μ) K
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U✝ : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < ↑↑(c • μ) U
⊢ ∃ K, K ⊆ U ∧ p K ∧ r < ↑↑(c • μ) K
rw [smul_apply, H.measure_eq_iSup hU, smul_eq_mul] at hr
no goals
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U✝ : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < c * ⨆ (K : Set α) (_ : K ⊆ U) (_ : p K), ↑↑μ K
⊢ ∃ K, K ⊆ U ∧ p K ∧ r < ↑↑(c • μ) K
simpa only [ENNReal.mul_iSup, lt_iSup_iff, exists_prop] using hr