-- Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
theorem innerRegular_isCompact_isClosed_measurableSet_of_finite [PseudoEMetricSpace α]
    [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
    (P : Measure α) [IsFiniteMeasure P] :
    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet

Proof state:
case h.e'_5.h.a
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
this : P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) fun s => MeasurableSet s ∧ P s ≠ ⊤
x✝ : Set α
⊢ MeasurableSet x✝ ↔ MeasurableSet x✝ ∧ P x✝ ≠ ⊤

Tactic:
simp only [iff_self_and]

Result:
case h.e'_5.h.a
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
this : P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) fun s => MeasurableSet s ∧ P s ≠ ⊤
x✝ : Set α
⊢ MeasurableSet x✝ → P x✝ ≠ ⊤

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet

Tactic:
suffices P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s)
    fun s ↦ MeasurableSet s ∧ P s ≠ ∞ by
  convert this
  simp only [iff_self_and]
  exact fun _ ↦ measure_ne_top P _

Result:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) fun s => MeasurableSet s ∧ P s ≠ ⊤

Proof state:
case refine_2.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
s t : Set α
hs_compact : IsCompact s
hs_closed : IsClosed s
ht_open : IsOpen t
⊢ IsCompact (s \ t) ∧ IsClosed (s \ t)

Tactic:
rw [diff_eq]

Result:
case refine_2.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
s t : Set α
hs_compact : IsCompact s
hs_closed : IsClosed s
ht_open : IsOpen t
⊢ IsCompact (s ∩ tᶜ) ∧ IsClosed (s ∩ tᶜ)

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
this : P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) fun s => MeasurableSet s ∧ P s ≠ ⊤
⊢ P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet

Tactic:
convert this

Result:
case h.e'_5.h.a
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
this : P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) fun s => MeasurableSet s ∧ P s ≠ ⊤
x✝ : Set α
⊢ MeasurableSet x✝ ↔ MeasurableSet x✝ ∧ P x✝ ≠ ⊤

Proof state:
case h.e'_5.h.a
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
this : P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) fun s => MeasurableSet s ∧ P s ≠ ⊤
x✝ : Set α
⊢ MeasurableSet x✝ → P x✝ ≠ ⊤

Tactic:
exact fun _ ↦ measure_ne_top P _

Result:
no goals

Proof state:
case refine_2.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
s t : Set α
hs_compact : IsCompact s
hs_closed : IsClosed s
ht_open : IsOpen t
⊢ IsCompact (s ∩ tᶜ) ∧ IsClosed (s ∩ tᶜ)

Tactic:
exact ⟨hs_compact.inter_right ht_open.isClosed_compl,
  hs_closed.inter (isClosed_compl_iff.mpr ht_open)⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) fun s => MeasurableSet s ∧ P s ≠ ⊤

Tactic:
refine Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_

Result:
case refine_1
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) IsOpen

case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ ∀ ⦃s U : Set α⦄, IsCompact s ∧ IsClosed s → IsOpen U → IsCompact (s \ U) ∧ IsClosed (s \ U)

Proof state:
case refine_1
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) IsOpen

Tactic:
exact innerRegularWRT_isCompact_isClosed_isOpen P

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ ∀ ⦃s U : Set α⦄, IsCompact s ∧ IsClosed s → IsOpen U → IsCompact (s \ U) ∧ IsClosed (s \ U)

Tactic:
rintro s t ⟨hs_compact, hs_closed⟩ ht_open

Result:
case refine_2.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : CompleteSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
s t : Set α
hs_compact : IsCompact s
hs_closed : IsClosed s
ht_open : IsOpen t
⊢ IsCompact (s \ t) ∧ IsClosed (s \ t)