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

Tactic:
obtain ⟨K, K_subs, pK, rK⟩ : ∃ K, K ⊆ (toMeasurable μ (s ∩ A)) ∩ s ∧ p K ∧ r < μ K := by
  have : r < μ ((toMeasurable μ (s ∩ A)) ∩ s) := by
    apply hr.trans_le
    rw [restrict_apply s_meas]
    exact measure_mono <| subset_inter (subset_toMeasurable μ (s ∩ A)) inter_subset_left
  refine h ⟨(measurableSet_toMeasurable _ _).inter s_meas, ?_⟩ _ this
  apply (lt_of_le_of_lt _ hs.lt_top).ne
  rw [← measure_toMeasurable (s ∩ A)]
  exact measure_mono inter_subset_left

Result:
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
⊢ ∃ K ⊆ s, p K ∧ r < (μ.restrict A) K

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
⊢ r < μ (toMeasurable μ (s ∩ A) ∩ s)

Tactic:
apply hr.trans_le

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
⊢ (μ.restrict 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 ⊆ toMeasurable μ (s ∩ A) ∩ s, p K ∧ r < μ K

Tactic:
have : r < μ ((toMeasurable μ (s ∩ A)) ∩ s) := by
  apply hr.trans_le
  rw [restrict_apply s_meas]
  exact measure_mono <| subset_inter (subset_toMeasurable μ (s ∩ A)) inter_subset_left

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)
⊢ ∃ K ⊆ toMeasurable μ (s ∩ A) ∩ s, p K ∧ r < μ K

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) ≤ μ (s ∩ A)

Tactic:
rw [← measure_toMeasurable (s ∩ A)]

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) ≤ μ (toMeasurable μ (s ∩ A))

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
⊢ (μ.restrict A) s ≤ μ (toMeasurable μ (s ∩ A) ∩ s)

Tactic:
rw [restrict_apply s_meas]

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
⊢ μ (s ∩ A) ≤ μ (toMeasurable μ (s ∩ A) ∩ s)

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
⊢ ∃ K ⊆ s, p K ∧ r < (μ.restrict A) K

Tactic:
refine ⟨K, K_subs.trans inter_subset_right, pK, ?_⟩

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

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 = (μ.restrict (toMeasurable μ (s ∩ A))) K

Tactic:
rw [restrict_apply' (measurableSet_toMeasurable μ (s ∩ A))]

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
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < μ K
⊢ μ K = μ (K ∩ toMeasurable μ (s ∩ A))

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) ≤ μ (toMeasurable μ (s ∩ A))

Tactic:
exact measure_mono 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
⊢ μ (s ∩ A) ≤ μ (toMeasurable μ (s ∩ A) ∩ s)

Tactic:
exact measure_mono <| subset_inter (subset_toMeasurable μ (s ∩ A)) inter_subset_left

Result:
no goals

Proof state:
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)

Tactic:
apply (inter_eq_left.2 ?_).symm

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
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < μ K
⊢ K ⊆ toMeasurable μ (s ∩ A)