awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : Subset.{u_1} (α := Set α) univ (⋃ (n : ℕ), s n)
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n)
hBU : ⋃ (n : ℕ), F ∩ s n = F
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n) : ℝ≥0∞)
n : ℕ
hn : r < (μ.restrict (s n) : (a : Set α) → ℝ≥0∞) F
rcases :
  ∀ (K : Set α) (KF : K ⊆ F) (hKp : p K) (hK : r < (μ.restrict (s n) : (a : Set α) → ℝ≥0∞) K),
    ∃ K ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases h n hF _ hn with ⟨K, KF, hKp, hK⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : Subset.{u_1} (α := Set α) univ (⋃ (n : ℕ), s n)
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n)
hBU : ⋃ (n : ℕ), F ∩ s n = F
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n) : ℝ≥0∞)
n : ℕ
hn : r < (μ.restrict (s n) : (a : Set α) → ℝ≥0∞) F
K : Set α
KF : K ⊆ F
hKp : p K
hK : r < (μ.restrict (s n) : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
⟨K, KF, hKp, hK.trans_le (restrict_apply_le _ _)⟩

Premises used: MeasureTheory.Measure.restrict_apply_le, LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : Subset.{u_1} (α := Set α) univ (⋃ (n : ℕ), s n)
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n)
hBU : ⋃ (n : ℕ), F ∩ s n = F
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n) : ℝ≥0∞)
n : ℕ
hn : r < (μ.restrict (s n) : (a : Set α) → ℝ≥0∞) F
K : Set α
KF : K ⊆ F
hKp : p K
hK : r < (μ.restrict (s n) : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
exact ⟨K, KF, hKp, hK.trans_le (restrict_apply_le _ _)⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
rw :
  ∀ (hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)) (r : ℝ≥0∞)
    (hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s), ∃ K ⊆ s, p K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, p K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K

Tactic:
rw [restrict_apply s_meas] at hs

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
apply :
  LE.le (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)
⊢ r < (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s)

Tactic:
apply hr.trans_le

Premises used: LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
rw :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)

Tactic:
rw [restrict_apply s_meas]

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)

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

Premises used: Set.inter_subset_left, MeasureTheory.subset_toMeasurable, Inter.inter, Set.subset_inter, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)

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

Premises used: Set.inter_subset_left, MeasureTheory.subset_toMeasurable, Inter.inter, Set.subset_inter, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
⊢ r < (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s)

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
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
this : r < (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s)
⊢ ∃ K ⊆ toMeasurable μ (s ∩ A) ∩ s, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

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

Premises used: MeasureTheory.measurableSet_toMeasurable, And.intro, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
this : r < (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s)
refine : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ K ⊆ toMeasurable μ (s ∩ A) ∩ s, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

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

Premises used: MeasureTheory.measurableSet_toMeasurable, And.intro, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
this : r < (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s)
apply :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

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

Premises used: lt_of_le_of_lt, Ne.lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
this : r < (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s)
rw :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A)) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)

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

Premises used: Inter.inter, MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
this : r < (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A)) : ℝ≥0∞)

Tactic:
measure_mono inter_subset_left

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
this : r < (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A)) : ℝ≥0∞)

Tactic:
exact measure_mono inter_subset_left

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
obtain :
  ∀ (K : Set α) (K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s) (pK : p K) (rK : r < (μ : (a : Set α) → ℝ≥0∞) K),
    ∃ K ⊆ s, p K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, p K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) 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

Premises used: Inter.inter, MeasureTheory.toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, p K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K

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

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < (μ : (a : Set α) → ℝ≥0∞) K
refine : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, p K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K

Tactic:
refine ⟨K, K_subs.trans inter_subset_right, pK, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
rK
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < (μ : (a : Set α) → ℝ≥0∞) K
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K ∩ toMeasurable μ (s ∩ A)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    ((μ.restrict (toMeasurable μ (s ∩ A)) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

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

Premises used: Inter.inter, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < (μ : (a : Set α) → ℝ≥0∞) K
h₁ : K = K ∩ toMeasurable μ (s ∩ A)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K ∩ toMeasurable μ (s ∩ A)) : ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < (μ : (a : Set α) → ℝ≥0∞) K
apply : K ⊆ toMeasurable μ (s ∩ A)
⊢ K = K ∩ toMeasurable μ (s ∩ A)

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

Premises used: Set.inter_eq_left, Iff.mpr, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ K ⊆ toMeasurable μ (s ∩ A)

Tactic:
K_subs.trans inter_subset_left

Premises used: HasSubset.Subset.trans, Set.inter_subset_left
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ K ⊆ toMeasurable μ (s ∩ A)

Tactic:
exact K_subs.trans inter_subset_left

Premises used: HasSubset.Subset.trans, Set.inter_subset_left
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < (μ : (a : Set α) → ℝ≥0∞) K
rwa :
  Eq (α := ℝ≥0∞) ((μ.restrict (s ∩ A) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    ((μ.restrict (s ∩ A) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
rwa₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
rwa₂ :
  Eq (α := ℝ≥0∞) ((μ.restrict (s ∩ A) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    ((μ.restrict (s ∩ A) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
rwa₃ rwa₄ rwa₅ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ (s ∩ A)) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    ((μ.restrict (s ∩ A) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
rwa [restrict_toMeasurable]

Premises used: MeasureTheory.Measure.restrict_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ LE.le (α := ℝ≥0∞) ((μ.restrict (s ∩ A) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
Measure.le_iff'.1 (restrict_mono inter_subset_right le_rfl) K

Premises used: le_rfl, MeasureTheory.Measure.restrict_mono, MeasureTheory.Measure.le_iff', Iff.mp, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A s : Set α
s_meas : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < (μ : (a : Set α) → ℝ≥0∞) K
r₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    ((μ.restrict (toMeasurable μ (s ∩ A)) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
r₂ :
  Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ (s ∩ A)) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    ((μ.restrict (s ∩ A) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
⊢ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) 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

Premises used: le_rfl, MeasureTheory.Measure.restrict_mono, MeasureTheory.Measure.le_iff', MeasureTheory.Measure.restrict, Inter.inter, Iff.mp, MeasureTheory.toMeasurable, DFunLike.coe, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A : Set α
hA : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have : Fact (μ A < ∞) := ⟨hA.lt_top⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A : Set α
hA : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ (μ.restrict A).InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s

Tactic:
(restrict h A).trans (of_imp (fun s hs ↦ ⟨hs, measure_ne_top _ _⟩))

Premises used: MeasureTheory.Measure.InnerRegularWRT.restrict, MeasureTheory.measure_ne_top, MeasureTheory.Measure.restrict, MeasureTheory.Measure.InnerRegularWRT.trans, And.intro, MeasureTheory.Measure.InnerRegularWRT.of_imp
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h :
  μ.InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A : Set α
hA : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ (μ.restrict A).InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s

Tactic:
exact (restrict h A).trans (of_imp (fun s hs ↦ ⟨hs, measure_ne_top _ _⟩))

Premises used: MeasureTheory.Measure.InnerRegularWRT.restrict, MeasureTheory.measure_ne_top, MeasureTheory.Measure.restrict, MeasureTheory.Measure.InnerRegularWRT.trans, And.intro, MeasureTheory.Measure.InnerRegularWRT.of_imp
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
B : ℕ → Set α := spanningSets μ
rw : s ∩ ⋃ (i : ℕ), B i = s
rw₁ : s ∩ univ = s
rw₂ rw₃ : s = s
⊢ ⋃ (n : ℕ), s ∩ B n = s

Tactic:
rw [← inter_iUnion, iUnion_spanningSets, inter_univ]

Premises used: Set.inter_univ, MeasureTheory.iUnion_spanningSets, Set.inter_iUnion