awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
ν : Measure α
inst_2 : μ.OuterRegular
inst_3 : ν.OuterRegular
hμν :
  ∀ (U : Set α),
    IsOpen[inst_1] U → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
s : Set α
ms : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (⨅ (U : Set α), ⨅ (_ : s ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U)
  (⨅ (U : Set α), ⨅ (_ : s ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (ν : (a : Set α) → ℝ≥0∞) U)
Tactic: rw [Set.measure_eq_iInf_isOpen, Set.measure_eq_iInf_isOpen]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
ν : Measure α
inst_2 : μ.OuterRegular
inst_3 : ν.OuterRegular
hμν :
  ∀ (U : Set α),
    IsOpen[inst_1] U → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
s : Set α
ms : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (⨅ (U : Set α), ⨅ (_ : s ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U)
    (⨅ (U : Set α), ⨅ (_ : s ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (ν : (a : Set α) → ℝ≥0∞) U)
have h : ∀ (t : Set α),
  s ⊆ t →
    ∀ (ht2 : IsOpen[inst_1] t), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: congr! 4 with t _ ht2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_3
inst : PseudoMetricSpace α
mα : MeasurableSpace α
μ ν : Measure α
inst_1 : μ.OuterRegular
inst_2 : ν.OuterRegular
hμν :
  ∀ (U : Set α),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U →
      Bornology.IsBounded U → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
⊢ μ = ν
have refine : ∀ (U : Set α) (hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
Tactic: refine ext_isOpen fun U hU ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_3
inst : PseudoMetricSpace α
mα : MeasurableSpace α
μ ν : Measure α
inst_1 : μ.OuterRegular
inst_2 : ν.OuterRegular
hμν :
  ∀ (U : Set α),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U →
      Bornology.IsBounded U → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
have obtain : ∀ (f : ℕ → Set α) (hm : Monotone f) (hu : ⋃ (i : ℕ), f i = U)
  (hf : ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
Tactic: obtain ⟨f, hm, hu, hf⟩ := Metric.eq_countable_union_of_isBounded_of_isOpen hU
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_3
inst : PseudoMetricSpace α
mα : MeasurableSpace α
μ ν : Measure α
inst_1 : μ.OuterRegular
inst_2 : ν.OuterRegular
hμν :
  ∀ (U : Set α),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U →
      Bornology.IsBounded U → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
f : ℕ → Set α
hm : Monotone f
hu : ⋃ (i : ℕ), f i = U
hf : ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i)) (⨆ (i : ℕ), (ν : (a : Set α) → ℝ≥0∞) (f i))
Tactic: rw [← hu, hm.measure_iUnion, hm.measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 < (μ : (a : Set α) → ℝ≥0∞) F
⊢ ⋃ (n : ℕ), F ∩ s n = F
have rw : F ∩ ⋃ (i : ℕ), s i = F
Tactic: rw [← inter_iUnion, univ_subset_iff.mp hs, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 < (μ : (a : Set α) → ℝ≥0∞) F
rw : F ∩ ⋃ (i : ℕ), s i = F
⊢ ⋃ (n : ℕ), F ∩ s n = F
have rw₁ : F ∩ univ = F
Tactic: rw [← inter_iUnion, univ_subset_iff.mp hs, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 < (μ : (a : Set α) → ℝ≥0∞) F
rw : F ∩ ⋃ (i : ℕ), s i = F
rw₁ : F ∩ univ = F
⊢ ⋃ (n : ℕ), F ∩ s n = F
have rw₂ : F = F
Tactic: rw [← inter_iUnion, univ_subset_iff.mp hs, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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 < (μ : (a : Set α) → ℝ≥0∞) F
⊢ ∃ K ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have hBU : ⋃ (n : ℕ), F ∩ s n = F
Tactic: have hBU : ⋃ n, F ∩ s n = F := by rw [← inter_iUnion, univ_subset_iff.mp hs, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 < (μ : (a : Set α) → ℝ≥0∞) F
hBU : ⋃ (n : ℕ), F ∩ s n = F
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), F ∩ s i) : ℝ≥0∞)
Tactic: rw [← (monotone_const.inter hmono).measure_iUnion, hBU]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 < (μ : (a : Set α) → ℝ≥0∞) F
hBU : ⋃ (n : ℕ), F ∩ s n = F
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), F ∩ s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞)
Tactic: rw [← (monotone_const.inter hmono).measure_iUnion, hBU]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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 < (μ : (a : Set α) → ℝ≥0∞) F
hBU : ⋃ (n : ℕ), F ∩ s n = F
⊢ ∃ K ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n) : ℝ≥0∞)
Tactic: have : μ F = ⨆ n, μ (F ∩ s n) := by
    rw [← (monotone_const.inter hmono).measure_iUnion, hBU]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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 < (μ : (a : Set α) → ℝ≥0∞) F
hBU : ⋃ (n : ℕ), F ∩ s n = F
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n) : ℝ≥0∞)
⊢ ∃ K ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have hr₁ : r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n)
Tactic: rw [this] at hr
Cleared hypotheses: hr, hBU, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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∞)
⊢ ∃ K ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have rcases : ∀ (n : ℕ) (hn : r < (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n)), ∃ K ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: rcases lt_iSup_iff.1 hr with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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 < (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n)
⊢ ∃ K ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have hn₁ : r < (μ.restrict (s n) : (a : Set α) → ℝ≥0∞) F
Tactic: rw [← restrict_apply hF] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have 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
Tactic: rcases h n hF _ hn with ⟨K, KF, hKp, hK⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
⊢ ∃ K ⊆ s, p K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
have 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
Tactic: rw [restrict_apply s_meas] at hs
Cleared hypotheses: hs, r, hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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)
have apply : LE.le (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)
Tactic: apply hr.trans_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)
Tactic: rw [restrict_apply s_meas]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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 ⊆ toMeasurable μ (s ∩ A) ∩ s, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
have refine : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine h ⟨(measurableSet_toMeasurable _ _).inter s_meas, ?_⟩ _ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)
Tactic: apply (lt_of_le_of_lt _ hs.lt_top).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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∞) (s ∩ A) : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A) ∩ s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ A)) : ℝ≥0∞)
Tactic: rw [← measure_toMeasurable (s ∩ A)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 ⊆ s, p K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
have 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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
have refine : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
Tactic: refine ⟨K, K_subs.trans inter_subset_right, pK, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    ((μ.restrict (toMeasurable μ (s ∩ A)) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K ∩ toMeasurable μ (s ∩ A)) : ℝ≥0∞)
Tactic: rw [restrict_apply' (measurableSet_toMeasurable μ (s ∩ A))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K ∩ toMeasurable μ (s ∩ A)) : ℝ≥0∞)
have h₁ : K = K ∩ toMeasurable μ (s ∩ A)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 = K ∩ toMeasurable μ (s ∩ A)
have apply : K ⊆ toMeasurable μ (s ∩ A)
Tactic: apply (inter_eq_left.2 ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ (s ∩ A)) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    ((μ.restrict (s ∩ A) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
have rwa : Eq (α := ℝ≥0∞) ((μ.restrict (s ∩ A) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ.restrict (s ∩ A) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: rwa [restrict_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
have r₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ.restrict (toMeasurable μ (s ∩ A)) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
have r₂ : Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ (s ∩ A)) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
  ((μ.restrict (s ∩ A) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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∞)
⊢ (μ.restrict A).InnerRegularWRT p fun (s : Set α) ↦ MeasurableSet s
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have : Fact (μ A < ∞) := ⟨hA.lt_top⟩