awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst_1] (s n)
h'' : Subset.{u_1} (α := Set α) univ (⋃ (n : ℕ), s n)
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet.{u_1} (α := α) (⋃ (n : ℕ), A n)
hr : r > (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n)
HA : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∞ : ℝ≥0∞)
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∑' (i : ℕ), δ i : ℝ≥0∞) < r
U : (n : ℕ) → Set α
hAU : ∀ (n : ℕ), U n ⊇ A n
hUo : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hU : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A n) : ℝ≥0∞) (δ n)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), U n) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) : ℝ≥0∞)

Tactic:
measure_iUnion_le _

Premises used: MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst_1] (s n)
h'' : Subset.{u_1} (α := Set α) univ (⋃ (n : ℕ), s n)
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet.{u_1} (α := α) (⋃ (n : ℕ), A n)
hr : r > (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n)
HA : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∞ : ℝ≥0∞)
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∑' (i : ℕ), δ i : ℝ≥0∞) < r
U : (n : ℕ) → Set α
hAU : ∀ (n : ℕ), U n ⊇ A n
hUo : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hU : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A n) : ℝ≥0∞) (δ n)
⊢ LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n))
    (∑' (n : ℕ), HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A n) : ℝ≥0∞) (δ n))

Tactic:
ENNReal.tsum_le_tsum fun n => (hU n).le

Premises used: ENNReal.tsum_le_tsum, LT.lt.le
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst_1] (s n)
h'' : Subset.{u_1} (α := Set α) univ (⋃ (n : ℕ), s n)
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet.{u_1} (α := α) (⋃ (n : ℕ), A n)
hr : r > (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n)
HA : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∞ : ℝ≥0∞)
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∑' (i : ℕ), δ i : ℝ≥0∞) < r
U : (n : ℕ) → Set α
hAU : ∀ (n : ℕ), U n ⊇ A n
hUo : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hU : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A n) : ℝ≥0∞) (δ n)
⊢ ∑' (n : ℕ), HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A n) : ℝ≥0∞) (δ n) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (A n)) (∑' (n : ℕ), δ n)

Tactic:
ENNReal.tsum_add

Premises used: ENNReal.tsum_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst_1] (s n)
h'' : Subset.{u_1} (α := Set α) univ (⋃ (n : ℕ), s n)
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet.{u_1} (α := α) (⋃ (n : ℕ), A n)
hr : r > (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n)
HA : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∞ : ℝ≥0∞)
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∑' (i : ℕ), δ i : ℝ≥0∞) < r
U : (n : ℕ) → Set α
hAU : ∀ (n : ℕ), U n ⊇ A n
hUo : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hU : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A n) : ℝ≥0∞) (δ n)
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (A n)) (∑' (n : ℕ), δ n) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∑' (n : ℕ), δ n : ℝ≥0∞)

Tactic:
(congr_arg₂ (· + ·) (measure_iUnion hAd hAm).symm rfl)

Premises used: MeasureTheory.measure_iUnion, HAdd.hAdd, Eq.symm, rfl, congr_arg₂
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst_1] (s n)
h'' : Subset.{u_1} (α := Set α) univ (⋃ (n : ℕ), s n)
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet.{u_1} (α := α) (⋃ (n : ℕ), A n)
hr : r > (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n)
HA : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∞ : ℝ≥0∞)
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∑' (i : ℕ), δ i : ℝ≥0∞) < r
U : (n : ℕ) → Set α
hAU : ∀ (n : ℕ), U n ⊇ A n
hUo : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hU : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A n) : ℝ≥0∞) (δ n)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∑' (n : ℕ), δ n : ℝ≥0∞) < r

Tactic:
hδε
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst_1] (s n)
h'' : Subset.{u_1} (α := Set α) univ (⋃ (n : ℕ), s n)
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet.{u_1} (α := α) (⋃ (n : ℕ), A n)
hr : r > (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n)
HA : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∞ : ℝ≥0∞)
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), A n) : ℝ≥0∞) (∑' (i : ℕ), δ i : ℝ≥0∞) < r
U : (n : ℕ) → Set α
hAU : ∀ (n : ℕ), U n ⊇ A n
hUo : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hU : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A n) : ℝ≥0∞) (δ n)
⊢ (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), U n) < r

Tactic:
calc
    μ (⋃ n, U n) ≤ ∑' n, μ (U n) := measure_iUnion_le _
    _ ≤ ∑' n, (μ (A n) + δ n) := ENNReal.tsum_le_tsum fun n => (hU n).le
    _ = ∑' n, μ (A n) + ∑' n, δ n := ENNReal.tsum_add
    _ = μ (⋃ n, A n) + ∑' n, δ n := (congr_arg₂ (· + ·) (measure_iUnion hAd hAm).symm rfl)
    _ < r := hδε

Premises used: ENNReal.tsum_le_tsum, ENNReal.tsum_add, LT.lt.le, MeasureTheory.measure_iUnion, MeasureTheory.measure_iUnion_le, HAdd.hAdd, Eq.symm, DFunLike.coe, Set.iUnion, rfl, congr_arg₂
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
inst_3 : μ.OuterRegular
k : Set α
hk : IsCompact k
apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[inst_1] k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) k : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[inst_1] k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) k : ℝ≥0∞)

Tactic:
apply le_antisymm ?_ (measure_mono subset_closure)

Premises used: subset_closure, le_antisymm, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
inst_3 : μ.OuterRegular
k : Set α
hk : IsCompact k
simp :
  ∀ (i : Set α) (i_1 : k ⊆ i) (i_2 : IsOpen[inst_1] i),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[inst_1] k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[inst_1] k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) k : ℝ≥0∞)

Tactic:
simp only [measure_eq_iInf_isOpen k, le_iInf_iff]

Premises used: le_iInf_iff, Set.measure_eq_iInf_isOpen
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
inst_3 : μ.OuterRegular
k : Set α
hk : IsCompact k
u : Set α
ku : k ⊆ u
u_open : IsOpen[inst_1] u
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[inst_1] k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
measure_mono (hk.closure_subset_of_isOpen u_open ku)

Premises used: IsCompact.closure_subset_of_isOpen, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
inst_3 : μ.OuterRegular
k : Set α
hk : IsCompact k
u : Set α
ku : k ⊆ u
u_open : IsOpen[inst_1] u
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[inst_1] k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
exact measure_mono (hk.closure_subset_of_isOpen u_open ku)

Premises used: IsCompact.closure_subset_of_isOpen, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
h :
  ∀ (s : Set α) (ms : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν

Tactic:
ext s ms
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
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)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Set.measure_eq_iInf_isOpen, Set.measure_eq_iInf_isOpen]

Premises used: Set.measure_eq_iInf_isOpen
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
h :
  ∀ (t : Set α),
    s ⊆ t →
      ∀ (ht2 : IsOpen[inst_1] t), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ 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:
congr! 4 with t _ ht2
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
t : Set α
h : s ⊆ t
ht2 : IsOpen[inst_1] t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
hμν t ht2
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
t : Set α
h : s ⊆ t
ht2 : IsOpen[inst_1] t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact hμν t ht2
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
⊢ μ = ν

Tactic:
ext_isOpen fun U hU ↦ ?_

Premises used: MeasureTheory.Measure.OuterRegular.ext_isOpen
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
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 ↦ ?_

Premises used: MeasureTheory.Measure.OuterRegular.ext_isOpen
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
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∞)
⊢ 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

Premises used: Metric.eq_countable_union_of_isBounded_of_isOpen
-- Module: Mathlib.MeasureTheory.Measure.Regular
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)
rw : Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i)) (⨆ (i : ℕ), (ν : (a : Set α) → ℝ≥0∞) (f i))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
rw [← hu, hm.measure_iUnion, hm.measure_iUnion]

Premises used: Monotone.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i)) (⨆ (i : ℕ), (ν : (a : Set α) → ℝ≥0∞) (f i))

Tactic:
iSup_congr fun i ↦ hμν (f i) (hf i).2 (hf i).1

Premises used: And.right, And.left, iSup_congr
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i)) (⨆ (i : ℕ), (ν : (a : Set α) → ℝ≥0∞) (f i))

Tactic:
exact iSup_congr fun i ↦ hμν (f i) (hf i).2 (hf i).1

Premises used: And.right, And.left, iSup_congr
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : μ.FiniteSpanningSetsIn {U : Set α | IsOpen[inst_1] U ∧ (μ.restrict U).OuterRegular}
⊢ μ.OuterRegular

Tactic:
OuterRegular.of_restrict (s := fun n ↦ s.set n) (fun n ↦ (s.set_mem n).2)
    (fun n ↦ (s.set_mem n).1) s.spanning.symm.subset

Premises used: MeasureTheory.Measure.OuterRegular.of_restrict, MeasureTheory.Measure.FiniteSpanningSetsIn.spanning, Eq.subset, And.right, And.left, Eq.symm, MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem
-- 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 < (μ : (a : Set α) → ℝ≥0∞) F
rw : F ∩ ⋃ (i : ℕ), s i = F
rw₁ : F ∩ univ = F
rw₂ rw₃ : F = F
⊢ ⋃ (n : ℕ), F ∩ s n = F

Tactic:
rw [← inter_iUnion, univ_subset_iff.mp hs, inter_univ]

Premises used: Set.univ_subset_iff, Set.inter_univ, Iff.mp, Set.inter_iUnion
-- 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 < (μ : (a : Set α) → ℝ≥0∞) F
⊢ ⋃ (n : ℕ), F ∩ s n = F

Tactic:
have hBU : ⋃ n, F ∩ s n = F := by rw [← inter_iUnion, univ_subset_iff.mp hs, inter_univ]
-- 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 < (μ : (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∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n) : ℝ≥0∞)

Tactic:
rw [← (monotone_const.inter hmono).measure_iUnion, hBU]

Premises used: monotone_const, Monotone.inter, Monotone.measure_iUnion
-- 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 < (μ : (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∞)

Tactic:
have : μ F = ⨆ n, μ (F ∩ s n) := by
    rw [← (monotone_const.inter hmono).measure_iUnion, hBU]
-- 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 < (μ : (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∞)
⊢ r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n)

Tactic:
rw [this] at hr
-- 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 < (μ : (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∞)
hr₁ : r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n)
⊢ ⋃ (n : ℕ), F ∩ s n = F

Tactic:
rw [this] at hr
-- 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 < (μ : (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∞)
hr₁ : r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n)
hBU₁ : ⋃ (n : ℕ), F ∩ s n = F
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n) : ℝ≥0∞)

Tactic:
rw [this] at hr
-- 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∞)
rcases : ∀ (n : ℕ) (hn : r < (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n)), ∃ K ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ F, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases lt_iSup_iff.1 hr with ⟨n, hn⟩

Premises used: Iff.mp, lt_iSup_iff
-- 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 < (μ : (a : Set α) → ℝ≥0∞) (F ∩ s n)
⊢ r < (μ.restrict (s n) : (a : Set α) → ℝ≥0∞) F

Tactic:
rw [← restrict_apply hF] at hn

Premises used: MeasureTheory.Measure.restrict_apply