α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
hU : q U
r : ℝ≥0∞
hr : r < ↑↑μ U
⊢ r < ⨆ (K : Set α) (_ : K ⊆ U) (_ : p K), ↑↑μ K
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
hU : q U
⊢ ↑↑μ U = ⨆ (K : Set α) (_ : K ⊆ U) (_ : p K), ↑↑μ K
refine'
  le_antisymm (le_of_forall_lt fun r hr => _) (iSup₂_le fun K hK => iSup_le fun _ => μ.mono hK)
no goals
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
hU : q U
r : ℝ≥0∞
hr : r < ↑↑μ U
⊢ r < ⨆ (K : Set α) (_ : K ⊆ U) (_ : p K), ↑↑μ K
simpa only [lt_iSup_iff, exists_prop] using H hU r hr