-- Mathlib/MeasureTheory/Measure/Regular.lean
/-- If `μ` is inner regular for measurable finite measure sets with respect to some class of sets,
then its restriction to any set is also inner regular for measurable finite measure sets, with
respect to the same class of sets. -/
lemma restrict (h : InnerRegularWRT μ p (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞)) (A : Set α) :
    InnerRegularWRT (μ.restrict A) p (fun s ↦ MeasurableSet s ∧ μ.restrict A s ≠ ∞)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ⊤
r : ℝ≥0∞
hr : r < (μ.restrict A) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < μ K
⊢ μ K = μ (K ∩ toMeasurable μ (s ∩ A))

Tactic:
congr

Result:
case h.e_6.h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ⊤
r : ℝ≥0∞
hr : r < (μ.restrict A) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < μ K
⊢ K = K ∩ toMeasurable μ (s ∩ A)

Proof state:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A s : Set α
s_meas : MeasurableSet s
hs : (μ.restrict A) s ≠ ⊤
r : ℝ≥0∞
hr : r < (μ.restrict A) s
⊢ ∃ K ⊆ s, p K ∧ r < (μ.restrict A) K

Tactic:
rw [restrict_apply s_meas] at hs

Result:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ⊤
r : ℝ≥0∞
hr : r < (μ.restrict A) s
⊢ ∃ K ⊆ s, p K ∧ r < (μ.restrict A) K

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ⊤
r : ℝ≥0∞
hr : r < (μ.restrict A) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < μ K
⊢ r < (μ.restrict A) K

Tactic:
calc
r < μ K := rK
_ = μ.restrict (toMeasurable μ (s ∩ A)) K := by
  rw [restrict_apply' (measurableSet_toMeasurable μ (s ∩ A))]
  congr
  apply (inter_eq_left.2 ?_).symm
  exact K_subs.trans inter_subset_left
_ = μ.restrict (s ∩ A) K := by rwa [restrict_toMeasurable]
_ ≤ μ.restrict A K := Measure.le_iff'.1 (restrict_mono inter_subset_right le_rfl) K

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ⊤
r : ℝ≥0∞
hr : r < (μ.restrict A) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < μ K
⊢ K ⊆ toMeasurable μ (s ∩ A)

Tactic:
exact K_subs.trans inter_subset_left

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ⊤
r : ℝ≥0∞
hr : r < (μ.restrict A) s
this : r < μ (toMeasurable μ (s ∩ A) ∩ s)
⊢ ∃ K ⊆ toMeasurable μ (s ∩ A) ∩ s, p K ∧ r < μ K

Tactic:
refine h ⟨(measurableSet_toMeasurable _ _).inter s_meas, ?_⟩ _ this

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ⊤
r : ℝ≥0∞
hr : r < (μ.restrict A) s
this : r < μ (toMeasurable μ (s ∩ A) ∩ s)
⊢ μ (toMeasurable μ (s ∩ A) ∩ s) ≠ ⊤

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ⊤
r : ℝ≥0∞
hr : r < (μ.restrict A) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < μ K
⊢ (μ.restrict (toMeasurable μ (s ∩ A))) K = (μ.restrict (s ∩ A)) K

Tactic:
rwa [restrict_toMeasurable]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ⊤
r : ℝ≥0∞
hr : r < (μ.restrict A) s
this : r < μ (toMeasurable μ (s ∩ A) ∩ s)
⊢ μ (toMeasurable μ (s ∩ A) ∩ s) ≠ ⊤

Tactic:
apply (lt_of_le_of_lt _ hs.lt_top).ne

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ⊤
r : ℝ≥0∞
hr : r < (μ.restrict A) s
this : r < μ (toMeasurable μ (s ∩ A) ∩ s)
⊢ μ (toMeasurable μ (s ∩ A) ∩ s) ≤ μ (s ∩ A)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A : Set α
⊢ (μ.restrict A).InnerRegularWRT p fun s => MeasurableSet s ∧ (μ.restrict A) s ≠ ⊤

Tactic:
rintro s ⟨s_meas, hs⟩ r hr

Result:
case intro
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A s : Set α
s_meas : MeasurableSet s
hs : (μ.restrict A) s ≠ ⊤
r : ℝ≥0∞
hr : r < (μ.restrict A) s
⊢ ∃ K ⊆ s, p K ∧ r < (μ.restrict A) K