awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegular
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
⊢ ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
InnerRegular.innerRegular hA _ hr

Premises used: MeasureTheory.Measure.InnerRegular.innerRegular
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
h : μ.InnerRegular
f : α → β
hf : Continuous[inst_1, inst_4] f
⊢ InnerRegular (map f μ)

Tactic:
⟨InnerRegularWRT.map h.innerRegular hf.aemeasurable (fun _s hs ↦ hf.measurable hs)
    (fun _K hK ↦ hK.image hf) (fun _s hs ↦ hs)⟩

Premises used: Continuous.aemeasurable, MeasureTheory.Measure.InnerRegularWRT.map, Continuous.measurable, IsCompact.image, MeasureTheory.Measure.InnerRegular.innerRegular, MeasureTheory.Measure.InnerRegular.mk
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
inst_6 : μ.InnerRegular
f : α ≃ₜ β
⊢ InnerRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)

Tactic:
InnerRegular.map_of_continuous f.continuous

Premises used: Homeomorph.continuous, MeasureTheory.Measure.InnerRegular.map_of_continuous
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
⊢ InnerRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ) ↔ μ.InnerRegular

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.map f⟩

Premises used: MeasureTheory.Measure.InnerRegular.map, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
refine : ∀ (h : InnerRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)), μ.InnerRegular
⊢ InnerRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ) ↔ μ.InnerRegular

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.map f⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
h : InnerRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
⊢ InnerRegular.{u_1} (α := α) (map.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) (map (⇑f : (a : α) → β) μ))

Tactic:
h.map f.symm

Premises used: MeasureTheory.Measure.InnerRegular.map, Homeomorph.symm
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
h : InnerRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
h₁ : μ = map.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) (map (⇑f : (a : α) → β) μ)
⊢ μ.InnerRegular

Tactic:
convert! h.map f.symm

Premises used: MeasureTheory.Measure.InnerRegular.map, Homeomorph.symm
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
h : InnerRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
h₁ : μ = map (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)) μ
⊢ μ = map.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) (map (⇑f : (a : α) → β) μ)

Tactic:
rw [map_map f.symm.continuous.measurable f.continuous.measurable]

Premises used: Homeomorph.continuous, Homeomorph.symm, Continuous.measurable, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
h : InnerRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
⊢ μ = map (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)) μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
mβ : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
μ : Measure β
inst_5 : μ.InnerRegular
f : α ≃ₜ β
⊢ InnerRegular.{u_1} (α := α) (comap (⇑f : (a : α) → β) μ)

Tactic:
InnerRegular.comap' μ f.isOpenEmbedding

Premises used: MeasureTheory.Measure.InnerRegular.comap', Homeomorph.isOpenEmbedding
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
innerRegular : (μ + ν).InnerRegularWRT IsCompact MeasurableSet
⊢ (μ + ν).InnerRegular

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
innerRegular :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
innerRegular₁ :
  ∀ (h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases eq_or_ne (μ s) 0 with h | h

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ r < (ν : (a : Set α) → ℝ≥0∞) s

Tactic:
simp only [h, zero_add] at hr

Premises used: zero_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hr : r < (ν : (a : Set α) → ℝ≥0∞) s
innerRegular :
  ∀ (K : Set α) (Ks : K ⊆ s) (hK : IsCompact K) (h'K : r < (ν : (a : Set α) → ℝ≥0∞) K),
    ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases MeasurableSet.exists_lt_isCompact hs hr 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 α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hr : r < (ν : (a : Set α) → ℝ≥0∞) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < (ν : (a : Set α) → ℝ≥0∞) K
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hr : r < (ν : (a : Set α) → ℝ≥0∞) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < (ν : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K

Tactic:
exact ⟨K, Ks, hK, h'K.trans_le (by simp)⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
innerRegular :
  ∀ (h' : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
innerRegular₁ :
  ∀ (h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases eq_or_ne (ν s) 0 with h' | h'

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ r < (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
simp only [h', add_zero] at hr

Premises used: add_zero
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
innerRegular :
  ∀ (K : Set α) (Ks : K ⊆ s) (hK : IsCompact K) (h'K : r < (μ : (a : Set α) → ℝ≥0∞) K),
    ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases MeasurableSet.exists_lt_isCompact hs hr 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 α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K

Tactic:
exact ⟨K, Ks, hK, h'K.trans_le (by simp)⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
innerRegular :
  ∀ (u : ℝ≥0∞) (hu : u < (μ : (a : Set α) → ℝ≥0∞) s) (v : ℝ≥0∞) (hv : v < (ν : (a : Set α) → ℝ≥0∞) s) (huv : r < u + v),
    ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases ENNReal.exists_lt_add_of_lt_add hr h h' with ⟨u, hu, v, hv, huv⟩

Premises used: ENNReal.exists_lt_add_of_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
innerRegular :
  ∀ (K : Set α) (Ks : K ⊆ s) (hK : IsCompact K) (h'K : u < (μ : (a : Set α) → ℝ≥0∞) K),
    ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases MeasurableSet.exists_lt_isCompact hs hu 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 α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
innerRegular :
  ∀ (K' : Set α) (K's : K' ⊆ s) (hK' : IsCompact K') (h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'),
    ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases MeasurableSet.exists_lt_isCompact hs hv with ⟨K', K's, 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 α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K

Tactic:
⟨K ∪ K', union_subset Ks K's, hK.union hK', huv.trans_le ?_⟩

Premises used: Set.union_subset, LT.lt.trans_le, And.intro, Exists.intro, IsCompact.union, Union.union
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'
innerRegular : u + v ≤ (μ + ν : (a : Set α) → ℝ≥0∞) (K ∪ K')
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K

Tactic:
refine ⟨K ∪ K', union_subset Ks K's, hK.union hK', huv.trans_le ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'
innerRegular :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) K' : ℝ≥0∞) ≤
    (μ + ν : (a : Set α) → ℝ≥0∞) (K ∪ K')
⊢ u + v ≤ (μ + ν : (a : Set α) → ℝ≥0∞) (K ∪ K')

Tactic:
apply (add_le_add h'K.le h'K'.le).trans

Premises used: add_le_add, LT.lt.le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'
innerRegular :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) K' : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K ∪ K') : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (K ∪ K') : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) K' : ℝ≥0∞) ≤
    (μ + ν : (a : Set α) → ℝ≥0∞) (K ∪ K')

Tactic:
simp only [Measure.coe_add, Pi.add_apply]

Premises used: MeasureTheory.Measure.coe_add, Pi.add_apply
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'
innerRegular : K ⊆ K ∪ K'
innerRegular₁ : K' ⊆ K ∪ K'
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) K' : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K ∪ K') : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (K ∪ K') : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'
⊢ K ⊆ K ∪ K'

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'
⊢ K' ⊆ K ∪ K'

Tactic:
simp
-- 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.{u_1} (α := α) 0

Tactic:
infer_instance
-- 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 : ι
s : Finset ι
ha : a ∉ s
ih : InnerRegular.{u_1} (α := α) (∑ i ∈ s, μ i)
insert : (μ a + ∑ i ∈ s, μ i).InnerRegular
⊢ InnerRegular.{u_1} (α := α) (∑ i ∈ Insert.insert a s, μ i)

Tactic:
simp only [ha, not_false_eq_true, Finset.sum_insert]

Premises used: 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
a : ι
s : Finset ι
ha : a ∉ s
ih : InnerRegular.{u_1} (α := α) (∑ i ∈ s, μ i)
⊢ (μ a + ∑ i ∈ s, μ i).InnerRegular

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