-- 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
α : 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) < ε
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K

Tactic:
rcases (U \ s).exists_isOpen_lt_of_lt _ hμU with ⟨U', hsU', hU'o, hμU'⟩

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 α
hsU' : U' ⊇ U \ s
hU'o : IsOpen U'
hμU' : μ U' < ε
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ 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)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
r : ℝ≥0∞
hr : r < μ s
⊢ p ∅

Tactic:
have : 0 < μ univ := (bot_le.trans_lt hr).trans_le (measure_mono (subset_univ _))

Result:
α : 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
⊢ p ∅

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)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
r : ℝ≥0∞
hr : r < μ s
h0 : p ∅
⊢ ∃ ε, ε ≠ 0 ∧ ε + ε ≤ μ s ∧ r = μ s - (ε + ε)

Tactic:
use (μ s - r) / 2

Result:
case h
α : 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 ∅
⊢ (μ s - r) / 2 ≠ 0 ∧ (μ s - r) / 2 + (μ s - r) / 2 ≤ μ s ∧ r = μ s - ((μ s - r) / 2 + (μ s - r) / 2)

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
h0 : p ∅
⊢ ∃ K ⊆ s, p K ∧ r < μ K

Tactic:
obtain ⟨ε, hε, hεs, rfl⟩ : ∃ ε ≠ 0, ε + ε ≤ μ s ∧ r = μ s - (ε + ε) := by
  use (μ s - r) / 2
  simp [*, hr.le, ENNReal.add_halves, ENNReal.sub_sub_cancel, le_add_right, tsub_eq_zero_iff_le]

Result:
case 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
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ 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)
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 \ U') + μ U' + ε ≤ μ (K \ U') + ε + ε

Tactic:
gcongr

Result:
no goals

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 + ε
⊢ μ s < μ (K \ U') + (ε + ε)

Tactic:
calc
  μ s ≤ μ U := μ.mono hsU
  _ < μ K + ε := hKr
  _ ≤ μ (K \ U') + μ U' + ε := add_le_add_right (tsub_le_iff_right.1 le_measure_diff) _
  _ ≤ μ (K \ U') + ε + ε := by gcongr
  _ = μ (K \ U') + (ε + ε) := add_assoc _ _ _

Result:
no goals

Proof state:
case h
α : 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 ∅
⊢ (μ s - r) / 2 ≠ 0 ∧ (μ s - r) / 2 + (μ s - r) / 2 ≤ μ s ∧ r = μ s - ((μ s - r) / 2 + (μ s - r) / 2)

Tactic:
simp [*, hr.le, ENNReal.add_halves, ENNReal.sub_sub_cancel, le_add_right, tsub_eq_zero_iff_le]

Result:
no goals

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)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
r : ℝ≥0∞
hr : r < μ s
this : 0 < μ univ
⊢ p ∅

Tactic:
obtain ⟨K, -, hK, -⟩ : ∃ K, K ⊆ univ ∧ p K ∧ 0 < μ K := H isOpen_univ _ this

Result:
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 ∅

Proof state:
case 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
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K

Tactic:
rcases hs.exists_isOpen_diff_lt hμs hε with ⟨U, hsU, hUo, hUt, hμU⟩

Result:
case 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) < ε
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K