-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem measurableSet_of_isOpen [OuterRegular μ] (H : InnerRegularWRT μ p IsOpen)
    (hd : ∀ ⦃s U⦄, p s → IsOpen U → p (s \ U)) :
    InnerRegularWRT μ p fun s => MeasurableSet s ∧ μ s ≠ ∞

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : μ U < ⊤
hμU : μ (U \ s) < ε
U' : Set α
hsU' : U' ⊇ U \ s
hU'o : IsOpen U'
hμU' : μ U' < ε
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K

Tactic:
replace hsU' := diff_subset_comm.1 hsU'

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : μ U < ⊤
hμU : μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : μ U' < ε
hsU' : U \ U' ⊆ s
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : μ U < ⊤
hμU : μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : μ U' < ε
hsU' : U \ U' ⊆ s
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K

Tactic:
rcases H.exists_subset_lt_add h0 hUo hUt.ne hε with ⟨K, hKU, hKc, hKr⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : μ U < ⊤
hμU : μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : μ U < μ K + ε
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : μ U < ⊤
hμU : μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : μ U < μ K + ε
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K

Tactic:
refine ⟨K \ U', fun x hx => hsU' ⟨hKU hx.1, hx.2⟩, hd hKc hU'o, ENNReal.sub_lt_of_lt_add hεs ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : μ U < ⊤
hμU : μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : μ U < μ K + ε
⊢ μ s < μ (K \ U') + (ε + ε)

Proof state:
case intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
r : ℝ≥0∞
hr : r < μ s
⊢ ∃ K ⊆ s, p K ∧ r < μ K

Tactic:
have h0 : p ∅ := by
  have : 0 < μ univ := (bot_le.trans_lt hr).trans_le (measure_mono (subset_univ _))
  obtain ⟨K, -, hK, -⟩ : ∃ K, K ⊆ univ ∧ p K ∧ 0 < μ K := H isOpen_univ _ this
  simpa using hd hK isOpen_univ

Result:
case intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
r : ℝ≥0∞
hr : r < μ s
h0 : p ∅
⊢ ∃ K ⊆ s, p K ∧ r < μ K

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
⊢ μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤

Tactic:
rintro s ⟨hs, hμs⟩ r hr

Result:
case intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
r : ℝ≥0∞
hr : r < μ s
⊢ ∃ K ⊆ s, p K ∧ r < μ K

Proof state:
case intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
r : ℝ≥0∞
hr : r < μ s
this : 0 < μ univ
K : Set α
hK : p K
⊢ p ∅

Tactic:
simpa using hd hK isOpen_univ

Result:
no goals