awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
a : Finset ι
empty : InnerRegular.{u_1} (α := α) (∑ i ∈ ∅, μ i)
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (ih : InnerRegular.{u_1} (α := α) (∑ i ∈ s, μ i)),
    InnerRegular.{u_1} (α := α) (∑ i ∈ Insert.insert a s, μ i)
⊢ InnerRegular.{u_1} (α := α) (∑ i ∈ a, μ i)

Tactic:
classical
  induction a using Finset.induction with
  | empty => simp only [Finset.sum_empty]; infer_instance
  | insert a s ha ih => simp only [ha, not_false_eq_true, Finset.sum_insert]; infer_instance

Premises used: Insert.insert, Finset.sum_empty, Finset.sum_insert, not_false_eq_true
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
innerRegular : (sum μ).InnerRegularWRT IsCompact MeasurableSet
⊢ (sum μ).InnerRegular

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
simp :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ ∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s) atTop
    (𝓝 (∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) s))
⊢ Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)

Tactic:
simp only [hs, Measure.sum_apply]

Premises used: MeasureTheory.Measure.sum_apply
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
⊢ Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ ∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s) atTop
    (𝓝 (∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) s))

Tactic:
ENNReal.summable.hasSum

Premises used: iInf, ENNReal.summable, Filter.atTop, Summable.hasSum, HasSum
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
⊢ Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ ∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s) atTop
    (𝓝 (∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) s))

Tactic:
exact ENNReal.summable.hasSum

Premises used: ENNReal.summable, Summable.hasSum
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
⊢ Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)

Tactic:
have : Tendsto (fun (a : Finset ι) ↦ ∑ i ∈ a, μ i s) atTop (𝓝 (Measure.sum μ s)) := by
    simp only [hs, Measure.sum_apply]
    exact ENNReal.summable.hasSum
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
simp : ∃ (a : Finset ι), r < ∑ c ∈ a, (μ c : (a : Set α) → ℝ≥0∞) s
⊢ ∃ (a : Finset ι), r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s

Tactic:
simp only [coe_finsetSum, Finset.sum_apply]

Premises used: MeasureTheory.Measure.coe_finsetSum, Finset.sum_apply
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
⊢ ∃ (a : Finset ι), r < ∑ c ∈ a, (μ c : (a : Set α) → ℝ≥0∞) s

Tactic:
((tendsto_order.1 this).1 r hr).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
⊢ ∃ (a : Finset ι), r < ∑ c ∈ a, (μ c : (a : Set α) → ℝ≥0∞) s

Tactic:
exact ((tendsto_order.1 this).1 r hr).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
innerRegular :
  ∀ (a : Finset ι) (ha : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s),
    ∃ K ⊆ s, IsCompact K ∧ r < (sum μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (sum μ : (a : Set α) → ℝ≥0∞) K

Tactic:
obtain ⟨a, ha⟩ : ∃ (a : Finset ι), r < (∑ i ∈ a, μ i) s := by
    simp only [coe_finsetSum, Finset.sum_apply]
    exact ((tendsto_order.1 this).1 r hr).exists

Premises used: Finset
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : Finset ι
ha : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s
innerRegular :
  ∀ (K : Set α) (Ks : K ⊆ s) (hK : IsCompact K) (h'K : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K),
    ∃ K ⊆ s, IsCompact K ∧ r < (sum μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (sum μ : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases MeasurableSet.exists_lt_isCompact hs ha with ⟨K, Ks, hK, h'K⟩

Premises used: MeasurableSet.exists_lt_isCompact
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : Finset ι
ha : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (sum μ : (a : Set α) → ℝ≥0∞) K

Tactic:
⟨K, Ks, hK, h'K.trans_le ?_⟩

Premises used: LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : Finset ι
ha : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K
innerRegular :
  LE.le (α := ℝ≥0∞) (((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (sum μ : (a : Set α) → ℝ≥0∞) K

Tactic:
refine ⟨K, Ks, hK, h'K.trans_le ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : Finset ι
ha : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K
innerRegular : LE.le (α := ℝ≥0∞) (∑ c ∈ a, (μ c : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
simp only [coe_finsetSum, Finset.sum_apply]

Premises used: MeasureTheory.Measure.coe_finsetSum, Finset.sum_apply
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : Finset ι
ha : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K
⊢ LE.le (α := ℝ≥0∞) (∑ c ∈ a, (μ c : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
(ENNReal.sum_le_tsum _).trans (le_sum_apply _ _)

Premises used: MeasureTheory.Measure.le_sum_apply, ENNReal.sum_le_tsum, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : Finset ι
ha : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K
⊢ LE.le (α := ℝ≥0∞) (∑ c ∈ a, (μ c : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
exact (ENNReal.sum_le_tsum _).trans (le_sum_apply _ _)

Premises used: MeasureTheory.Measure.le_sum_apply, ENNReal.sum_le_tsum, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ K ⊆ A, IsCompact K ∧ (μ : (a : Set α) → ℝ≥0∞) A < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε

Tactic:
InnerRegularCompactLTTop.innerRegular.exists_subset_lt_add isCompact_empty ⟨hA, h'A⟩ h'A hε

Premises used: MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular, And.intro, isCompact_empty, MeasureTheory.Measure.InnerRegularWRT.exists_subset_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : R1Space α
inst_4 : BorelSpace α
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hK : IsCompact K
hμK rwa rwa₁ rwa₂ rwa₃ : (μ : (a : Set α) → ℝ≥0∞) A < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
⊢ (μ : (a : Set α) → ℝ≥0∞) A < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[inst_1] K) : ℝ≥0∞) ε

Tactic:
rwa [hK.measure_closure]

Premises used: IsCompact.measure_closure
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : T2Space α
inst_4 : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
rcases :
  ∀ (K : Set α) (hKA : K ⊆ A) (hKc : IsCompact K)
    (hK : (μ : (a : Set α) → ℝ≥0∞) A < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε),
    ∃ K ⊆ A, IsCompact K ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < ε
⊢ ∃ K ⊆ A, IsCompact K ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < ε

Tactic:
rcases hA.exists_isCompact_lt_add h'A hε with ⟨K, hKA, hKc, hK⟩

Premises used: MeasurableSet.exists_isCompact_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : T2Space α
inst_4 : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hKc : IsCompact K
hK : (μ : (a : Set α) → ℝ≥0∞) A < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
⊢ ∃ K ⊆ A, IsCompact K ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < ε

Tactic:
⟨K, hKA, hKc, measure_diff_lt_of_lt_add hKc.nullMeasurableSet hKA
    (ne_top_of_le_ne_top h'A <| measure_mono hKA) hK⟩

Premises used: MeasureTheory.measure_diff_lt_of_lt_add, ne_top_of_le_ne_top, And.intro, MeasureTheory.measure_mono, Exists.intro, IsCompact.nullMeasurableSet
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : T2Space α
inst_4 : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hKc : IsCompact K
hK : (μ : (a : Set α) → ℝ≥0∞) A < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
⊢ ∃ K ⊆ A, IsCompact K ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < ε

Tactic:
exact ⟨K, hKA, hKc, measure_diff_lt_of_lt_add hKc.nullMeasurableSet hKA
    (ne_top_of_le_ne_top h'A <| measure_mono hKA) hK⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : R1Space α
inst_4 : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
rcases :
  ∀ (K : Set α) (hKA : K ⊆ A) (hKco : IsCompact K) (hKcl : IsClosed[inst_1] K)
    (hK : (μ : (a : Set α) → ℝ≥0∞) A < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε),
    ∃ K ⊆ A, IsCompact K ∧ IsClosed[inst_1] K ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < ε
⊢ ∃ K ⊆ A, IsCompact K ∧ IsClosed[inst_1] K ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < ε

Tactic:
rcases hA.exists_isCompact_isClosed_lt_add h'A hε with ⟨K, hKA, hKco, hKcl, hK⟩

Premises used: MeasurableSet.exists_isCompact_isClosed_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : R1Space α
inst_4 : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hK : (μ : (a : Set α) → ℝ≥0∞) A < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
⊢ ∃ K ⊆ A, IsCompact K ∧ IsClosed[inst_1] K ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < ε

Tactic:
⟨K, hKA, hKco, hKcl, measure_diff_lt_of_lt_add hKcl.nullMeasurableSet hKA
    (ne_top_of_le_ne_top h'A <| measure_mono hKA) hK⟩

Premises used: MeasureTheory.measure_diff_lt_of_lt_add, ne_top_of_le_ne_top, And.intro, IsClosed.nullMeasurableSet, MeasureTheory.measure_mono, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : R1Space α
inst_4 : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hK : (μ : (a : Set α) → ℝ≥0∞) A < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
⊢ ∃ K ⊆ A, IsCompact K ∧ IsClosed[inst_1] K ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < ε

Tactic:
exact ⟨K, hKA, hKco, hKcl, measure_diff_lt_of_lt_add hKcl.nullMeasurableSet hKA
    (ne_top_of_le_ne_top h'A <| measure_mono hKA) hK⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
⊢ ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
InnerRegularCompactLTTop.innerRegular ⟨hA, h'A⟩ _ hr

Premises used: MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular, And.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (⨆ (K : Set α), ⨆ (_ : K ⊆ A), ⨆ (_ : IsCompact K), (μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
InnerRegularCompactLTTop.innerRegular.measure_eq_iSup ⟨hA, h'A⟩

Premises used: MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular, And.intro, MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
A : Set α
⊢ (μ.restrict A).InnerRegularCompactLTTop

Tactic:
⟨InnerRegularWRT.restrict h.innerRegular A⟩

Premises used: MeasureTheory.Measure.InnerRegularWRT.restrict, MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular, MeasureTheory.Measure.InnerRegularCompactLTTop.mk
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
inst_2 : IsFiniteMeasure μ
innerRegular : μ.InnerRegularWRT IsCompact MeasurableSet
⊢ μ.InnerRegular

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
inst_2 : IsFiniteMeasure μ
⊢ μ.InnerRegularWRT IsCompact fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
h.innerRegular

Premises used: MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
inst_2 : IsFiniteMeasure μ
h₁ : ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.InnerRegularWRT IsCompact MeasurableSet

Tactic:
convert! h.innerRegular with s

Premises used: MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
inst_2 : IsFiniteMeasure μ
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [measure_ne_top μ s]

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : R1Space α
inst_4 : μ.InnerRegularCompactLTTop
inst_5 : IsFiniteMeasure μ
⊢ μ.WeaklyRegular

Tactic:
InnerRegular.innerRegularWRT_isClosed_isOpen.weaklyRegular_of_finite _

Premises used: MeasureTheory.Measure.InnerRegular.innerRegularWRT_isClosed_isOpen, MeasureTheory.Measure.InnerRegularWRT.weaklyRegular_of_finite
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) K < r
rcases :
  ∀ (V : Set α) (hKV : V ⊇ K) (hVo : IsOpen[inst_1] V)
    (hμV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
⊢ ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
rcases hK.exists_open_superset_measure_lt_top μ with ⟨V, hKV, hVo, hμV⟩

Premises used: IsCompact.exists_open_superset_measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) K < r
V : Set α
hKV : V ⊇ K
hVo : IsOpen[inst_1] V
hμV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have := Fact.mk hμV
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) K < r
V : Set α
hKV : V ⊇ K
hVo : IsOpen[inst_1] V
hμV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ.restrict V : (a : Set α) → ℝ≥0∞) U < r

Tactic:
exists_isOpen_lt_of_lt K r <| (restrict_apply_le _ _).trans_lt hr

Premises used: MeasureTheory.Measure.restrict_apply_le, Set.exists_isOpen_lt_of_lt, LE.le.trans_lt