awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
U : Set G
hU : Membership.mem (γ := Set (Set G)) {s : Set G | IsOpen s} U
U' : Opens G
this_1 : Nonempty.{max 1 (w + 1)} { L : Compacts G // (↑L : Set G) ⊆ (↑U' : Set G) ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure (↑L : Set G), isCompact' := ⋯ }
hL : (↑L : Set G) ⊆ (↑U' : Set G) ∧ (↑L : Set G) ⊆ U
hL'U : (↑L' : Set G) ⊆ U
hL'U' : (↑L' : Set G) ⊆ (↑U' : Set G)
this_2 : (↑U' : Set G) \ U ⊆ (↑U' : Set G) \ (↑L' : Set G)
this_3 : Nonempty.{max 1 (w + 1)} { M : Compacts G // (↑M : Set G) ⊆ (↑U' : Set G) \ closure (↑L : Set G) }
M : Compacts G
hM : (↑M : Set G) ⊆ (↑U' : Set G) \ (↑L' : Set G)
M' : Compacts G := { carrier := closure (↑M : Set G), isCompact' := ⋯ }
hM' : (↑M' : Set G) ⊆ (↑U' : Set G) \ (↑L' : Set G)
this : (↑(L' ⊔ M') : Set G) ⊆ (↑U' : Set G)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) L' : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) M' : ℝ≥0∞) ≤
    μ.innerContent { carrier := (↑U' : Set G), is_open' := ⋯ }
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) L' : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) M' : ℝ≥0∞) ≤
    (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U' : Set G)

Tactic:
rw [μ.outerMeasure_of_isOpen (↑U') U'.2]

Premises used: SetLike.coe, TopologicalSpace.Opens.is_open', MeasureTheory.Content.outerMeasure_of_isOpen
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
U : Set G
hU : Membership.mem (γ := Set (Set G)) {s : Set G | IsOpen s} U
U' : Opens G
this_1 : Nonempty.{max 1 (w + 1)} { L : Compacts G // (↑L : Set G) ⊆ (↑U' : Set G) ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure (↑L : Set G), isCompact' := ⋯ }
hL : (↑L : Set G) ⊆ (↑U' : Set G) ∧ (↑L : Set G) ⊆ U
hL'U : (↑L' : Set G) ⊆ U
hL'U' : (↑L' : Set G) ⊆ (↑U' : Set G)
this_2 : (↑U' : Set G) \ U ⊆ (↑U' : Set G) \ (↑L' : Set G)
this_3 : Nonempty.{max 1 (w + 1)} { M : Compacts G // (↑M : Set G) ⊆ (↑U' : Set G) \ closure (↑L : Set G) }
M : Compacts G
hM : (↑M : Set G) ⊆ (↑U' : Set G) \ (↑L' : Set G)
M' : Compacts G := { carrier := closure (↑M : Set G), isCompact' := ⋯ }
hM' : (↑M' : Set G) ⊆ (↑U' : Set G) \ (↑L' : Set G)
this : (↑(L' ⊔ M') : Set G) ⊆ (↑U' : Set G)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) L' : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) M' : ℝ≥0∞) ≤
    μ.innerContent { carrier := (↑U' : Set G), is_open' := ⋯ }

Tactic:
le_trans (ge_of_eq ?_) (μ.le_innerContent _ _ this)

Premises used: MeasureTheory.Content.le_innerContent, ge_of_eq, le_trans
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
U : Set G
hU : Membership.mem (γ := Set (Set G)) {s : Set G | IsOpen s} U
U' : Opens G
this_1 : Nonempty.{max 1 (w + 1)} { L : Compacts G // (↑L : Set G) ⊆ (↑U' : Set G) ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure (↑L : Set G), isCompact' := ⋯ }
hL : (↑L : Set G) ⊆ (↑U' : Set G) ∧ (↑L : Set G) ⊆ U
hL'U : (↑L' : Set G) ⊆ U
hL'U' : (↑L' : Set G) ⊆ (↑U' : Set G)
this_2 : (↑U' : Set G) \ U ⊆ (↑U' : Set G) \ (↑L' : Set G)
this_3 : Nonempty.{max 1 (w + 1)} { M : Compacts G // (↑M : Set G) ⊆ (↑U' : Set G) \ closure (↑L : Set G) }
M : Compacts G
hM : (↑M : Set G) ⊆ (↑U' : Set G) \ (↑L' : Set G)
M' : Compacts G := { carrier := closure (↑M : Set G), isCompact' := ⋯ }
hM' : (↑M' : Set G) ⊆ (↑U' : Set G) \ (↑L' : Set G)
this : (↑(L' ⊔ M') : Set G) ⊆ (↑U' : Set G)
refine :
  (μ : (a : Compacts G) → ℝ≥0∞) (L' ⊔ M') =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) L' : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) M' : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) L' : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) M' : ℝ≥0∞) ≤
    μ.innerContent { carrier := (↑U' : Set G), is_open' := ⋯ }

Tactic:
refine le_trans (ge_of_eq ?_) (μ.le_innerContent _ _ this)

Premises used: MeasureTheory.Content.le_innerContent, ge_of_eq, le_trans
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
U : Set G
hU : Membership.mem (γ := Set (Set G)) {s : Set G | IsOpen s} U
U' : Opens G
this_1 : Nonempty.{max 1 (w + 1)} { L : Compacts G // (↑L : Set G) ⊆ (↑U' : Set G) ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure (↑L : Set G), isCompact' := ⋯ }
hL : (↑L : Set G) ⊆ (↑U' : Set G) ∧ (↑L : Set G) ⊆ U
hL'U : (↑L' : Set G) ⊆ U
hL'U' : (↑L' : Set G) ⊆ (↑U' : Set G)
this_2 : (↑U' : Set G) \ U ⊆ (↑U' : Set G) \ (↑L' : Set G)
this_3 : Nonempty.{max 1 (w + 1)} { M : Compacts G // (↑M : Set G) ⊆ (↑U' : Set G) \ closure (↑L : Set G) }
M : Compacts G
hM : (↑M : Set G) ⊆ (↑U' : Set G) \ (↑L' : Set G)
M' : Compacts G := { carrier := closure (↑M : Set G), isCompact' := ⋯ }
hM' : (↑M' : Set G) ⊆ (↑U' : Set G) \ (↑L' : Set G)
this : (↑(L' ⊔ M') : Set G) ⊆ (↑U' : Set G)
⊢ (μ : (a : Compacts G) → ℝ≥0∞) (L' ⊔ M') =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) L' : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) M' : ℝ≥0∞)

Tactic:
μ.sup_disjoint L' M' (subset_diff.1 hM').2.symm isClosed_closure isClosed_closure

Premises used: Set.subset_diff, Disjoint.symm, And.right, Iff.mp, isClosed_closure, MeasureTheory.Content.sup_disjoint
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
U : Set G
hU : Membership.mem (γ := Set (Set G)) {s : Set G | IsOpen s} U
U' : Opens G
this_1 : Nonempty.{max 1 (w + 1)} { L : Compacts G // (↑L : Set G) ⊆ (↑U' : Set G) ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure (↑L : Set G), isCompact' := ⋯ }
hL : (↑L : Set G) ⊆ (↑U' : Set G) ∧ (↑L : Set G) ⊆ U
hL'U : (↑L' : Set G) ⊆ U
hL'U' : (↑L' : Set G) ⊆ (↑U' : Set G)
this_2 : (↑U' : Set G) \ U ⊆ (↑U' : Set G) \ (↑L' : Set G)
this_3 : Nonempty.{max 1 (w + 1)} { M : Compacts G // (↑M : Set G) ⊆ (↑U' : Set G) \ closure (↑L : Set G) }
M : Compacts G
hM : (↑M : Set G) ⊆ (↑U' : Set G) \ (↑L' : Set G)
M' : Compacts G := { carrier := closure (↑M : Set G), isCompact' := ⋯ }
hM' : (↑M' : Set G) ⊆ (↑U' : Set G) \ (↑L' : Set G)
this : (↑(L' ⊔ M') : Set G) ⊆ (↑U' : Set G)
⊢ (μ : (a : Compacts G) → ℝ≥0∞) (L' ⊔ M') =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) L' : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) M' : ℝ≥0∞)

Tactic:
exact μ.sup_disjoint L' M' (subset_diff.1 hM').2.symm isClosed_closure isClosed_closure

Premises used: Set.subset_diff, Disjoint.symm, And.right, Iff.mp, isClosed_closure, MeasureTheory.Content.sup_disjoint
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
toMeasure_apply _ _ hs

Premises used: MeasureTheory.toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
⊢ Measure.OuterRegular μ.measure

Tactic:
⟨fun A hA r (hr : _ < _) ↦ ?_⟩

Premises used: MeasureTheory.Measure.OuterRegular.mk
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
refine :
  ∀ (A : Set G) (hA : MeasurableSet A) (r : ℝ≥0∞) (hr : ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) A < r),
    ∃ U ⊇ A, IsOpen U ∧ ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) U < r
⊢ Measure.OuterRegular μ.measure

Tactic:
refine ⟨fun A hA r (hr : _ < _) ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
hr : ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) A < r
⊢ ⨅ (U : Set G), ⨅ (hU : IsOpen U), ⨅ (_ : A ⊆ U), μ.innerContent { carrier := U, is_open' := hU } < r

Tactic:
rw [μ.measure_apply hA, outerMeasure_eq_iInf] at hr

Premises used: MeasureTheory.Content.outerMeasure_eq_iInf, MeasureTheory.Content.measure_apply
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
hr : ⨅ (U : Set G), ⨅ (hU : IsOpen U), ⨅ (_ : A ⊆ U), μ.innerContent { carrier := U, is_open' := hU } < r
⊢ ∃ (i : Set G) (h : IsOpen i) (_ : A ⊆ i), μ.innerContent { carrier := i, is_open' := ⋯ : Opens G } < r

Tactic:
simp only [iInf_lt_iff] at hr

Premises used: iInf_lt_iff
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
hr : ∃ (i : Set G) (h : IsOpen i) (_ : A ⊆ i), μ.innerContent { carrier := i, is_open' := ⋯ : Opens G } < r
rcases :
  ∀ (U : Set G) (hUo : IsOpen U) (hAU : A ⊆ U) (hr : μ.innerContent { carrier := U, is_open' := ⋯ : Opens G } < r),
    ∃ U ⊇ A, IsOpen U ∧ ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) U < r
⊢ ∃ U ⊇ A, IsOpen U ∧ ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) U < r

Tactic:
rcases hr with ⟨U, hUo, hAU, hr⟩
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
U : Set G
hUo : IsOpen U
hAU : A ⊆ U
hr : μ.innerContent { carrier := U, is_open' := ⋯ : Opens G } < r
⊢ ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) U < r

Tactic:
rw [← μ.outerMeasure_of_isOpen U hUo, ← μ.measure_apply hUo.measurableSet] at hr

Premises used: IsOpen.measurableSet, MeasureTheory.Content.outerMeasure_of_isOpen, MeasureTheory.Content.measure_apply
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
U : Set G
hUo : IsOpen U
hAU : A ⊆ U
hr : ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) U < r
⊢ ∃ U ⊇ A, IsOpen U ∧ ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) U < r

Tactic:
⟨U, hAU, hUo, hr⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
U : Set G
hUo : IsOpen U
hAU : A ⊆ U
hr : ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) U < r
⊢ ∃ U ⊇ A, IsOpen U ∧ ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) U < r

Tactic:
exact ⟨U, hAU, hUo, hr⟩
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
⊢ IsFiniteMeasureOnCompacts (m0 := S) μ.measure

Tactic:
⟨fun K hK => ?_⟩

Premises used: MeasureTheory.IsFiniteMeasureOnCompacts.mk
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
refine :
  ∀ (K : Set G) (hK : IsCompact K),
    LT.lt (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasureOnCompacts (m0 := S) μ.measure

Tactic:
refine ⟨fun K hK => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
apply : LT.lt (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (closure K) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply (measure_mono subset_closure).trans_lt _

Premises used: subset_closure, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
rw : LT.lt (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (closure K) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (closure K) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [measure_apply _ isClosed_closure.measurableSet]

Premises used: IsClosed.measurableSet, isClosed_closure, MeasureTheory.Content.measure_apply
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (closure K) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
μ.outerMeasure_lt_top_of_isCompact hK.closure

Premises used: IsCompact.closure, MeasureTheory.Content.outerMeasure_lt_top_of_isCompact
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (closure K) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact μ.outerMeasure_lt_top_of_isCompact hK.closure

Premises used: IsCompact.closure, MeasureTheory.Content.outerMeasure_lt_top_of_isCompact
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
⊢ IsFiniteMeasureOnCompacts (m0 := S) μ.measure

Tactic:
have : IsFiniteMeasureOnCompacts μ.measure := by
    refine ⟨fun K hK => ?_⟩
    apply (measure_mono subset_closure).trans_lt _
    rw [measure_apply _ isClosed_closure.measurableSet]
    exact μ.outerMeasure_lt_top_of_isCompact hK.closure
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
this : IsFiniteMeasureOnCompacts (m0 := S) μ.measure
⊢ Measure.Regular μ.measure

Tactic:
⟨fun U hU r hr => ?_⟩

Premises used: MeasureTheory.Measure.Regular.mk
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
this : IsFiniteMeasureOnCompacts (m0 := S) μ.measure
refine :
  ∀ (U : Set G) (hU : IsOpen U) (r : ℝ≥0∞) (hr : r < ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) U),
    ∃ K ⊆ U, IsCompact K ∧ r < ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) K
⊢ Measure.Regular μ.measure

Tactic:
refine ⟨fun U hU r hr => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
this : IsFiniteMeasureOnCompacts (m0 := S) μ.measure
U : Set G
hU : IsOpen U
r : ℝ≥0∞
hr : r < ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) U
⊢ r < μ.innerContent { carrier := U, is_open' := hU }

Tactic:
rw [measure_apply _ hU.measurableSet, μ.outerMeasure_of_isOpen U hU] at hr

Premises used: IsOpen.measurableSet, MeasureTheory.Content.outerMeasure_of_isOpen, MeasureTheory.Content.measure_apply
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
this : IsFiniteMeasureOnCompacts (m0 := S) μ.measure
U : Set G
hU : IsOpen U
r : ℝ≥0∞
hr : r < μ.innerContent { carrier := U, is_open' := hU }
⊢ ∃ (i : Compacts G) (_ : (↑i : Set G) ⊆ (↑{ carrier := U, is_open' := hU : Opens G } : Set G)),
    r < (μ : (a : Compacts G) → ℝ≥0∞) i

Tactic:
simp only [innerContent, lt_iSup_iff] at hr

Premises used: MeasureTheory.Content.innerContent, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
this : IsFiniteMeasureOnCompacts (m0 := S) μ.measure
U : Set G
hU : IsOpen U
r : ℝ≥0∞
hr :
  ∃ (i : Compacts G) (_ : (↑i : Set G) ⊆ (↑{ carrier := U, is_open' := hU : Opens G } : Set G)),
    r < (μ : (a : Compacts G) → ℝ≥0∞) i
rcases :
  ∀ (K : Compacts G) (hKU : (↑K : Set G) ⊆ (↑{ carrier := U, is_open' := hU : Opens G } : Set G))
    (hr : r < (μ : (a : Compacts G) → ℝ≥0∞) K),
    ∃ K ⊆ U, IsCompact K ∧ r < ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, IsCompact K ∧ r < ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) K

Tactic:
rcases hr with ⟨K, hKU, hr⟩
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
this : IsFiniteMeasureOnCompacts (m0 := S) μ.measure
U : Set G
hU : IsOpen U
r : ℝ≥0∞
K : Compacts G
hKU : (↑K : Set G) ⊆ (↑{ carrier := U, is_open' := hU : Opens G } : Set G)
hr : r < (μ : (a : Compacts G) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, IsCompact K ∧ r < ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) K

Tactic:
⟨K, hKU, K.2, hr.trans_le ?_⟩

Premises used: TopologicalSpace.Compacts.isCompact', SetLike.coe, LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
this : IsFiniteMeasureOnCompacts (m0 := S) μ.measure
U : Set G
hU : IsOpen U
r : ℝ≥0∞
K : Compacts G
hKU : (↑K : Set G) ⊆ (↑{ carrier := U, is_open' := hU : Opens G } : Set G)
hr : r < (μ : (a : Compacts G) → ℝ≥0∞) K
refine :
  LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
    (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
⊢ ∃ K ⊆ U, IsCompact K ∧ r < ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) K

Tactic:
refine ⟨K, hKU, K.2, hr.trans_le ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
this : IsFiniteMeasureOnCompacts (m0 := S) μ.measure
U : Set G
hU : IsOpen U
r : ℝ≥0∞
K : Compacts G
hKU : (↑K : Set G) ⊆ (↑{ carrier := U, is_open' := hU : Opens G } : Set G)
hr : r < (μ : (a : Compacts G) → ℝ≥0∞) K
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
    (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)

Tactic:
(μ.le_outerMeasure_compacts K).trans (le_toMeasure_apply _ _ _)

Premises used: MeasureTheory.Content.le_outerMeasure_compacts, MeasureTheory.le_toMeasure_apply, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
S : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : WeaklyLocallyCompactSpace G
this : IsFiniteMeasureOnCompacts (m0 := S) μ.measure
U : Set G
hU : IsOpen U
r : ℝ≥0∞
K : Compacts G
hKU : (↑K : Set G) ⊆ (↑{ carrier := U, is_open' := hU : Opens G } : Set G)
hr : r < (μ : (a : Compacts G) → ℝ≥0∞) K
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
    (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)

Tactic:
exact (μ.le_outerMeasure_compacts K).trans (le_toMeasure_apply _ _ _)

Premises used: MeasureTheory.Content.le_outerMeasure_compacts, MeasureTheory.le_toMeasure_apply, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
by_contra :
  ∀
    (hc :
      ¬∃ (K' : Compacts G),
          K.carrier ⊆ interior K'.carrier ∧
            (μ : (a : Compacts G) → ℝ≥0∞) K' ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)),
    False
⊢ ∃ (K' : Compacts G),
    K.carrier ⊆ interior K'.carrier ∧
      (μ : (a : Compacts G) → ℝ≥0∞) K' ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
by_contra hc
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc :
  ¬∃ (K' : Compacts G),
      K.carrier ⊆ interior K'.carrier ∧
        (μ : (a : Compacts G) → ℝ≥0∞) K' ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ ∀ (x : Compacts G),
    K.carrier ⊆ interior x.carrier →
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) < (μ : (a : Compacts G) → ℝ≥0∞) x

Tactic:
simp only [not_exists, not_and, not_le] at hc

Premises used: not_le, not_exists, not_and
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc :
  ∀ (x : Compacts G),
    K.carrier ⊆ interior x.carrier →
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) < (μ : (a : Compacts G) → ℝ≥0∞) x
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) ≤
    ⨅ (K' : Compacts G), ⨅ (_ : (↑K : Set G) ⊆ interior (↑K' : Set G)), (μ : (a : Compacts G) → ℝ≥0∞) K'

Tactic:
have lower_bound_iInf : μ K + ε ≤
      ⨅ (K' : TopologicalSpace.Compacts G) (_ : (K : Set G) ⊆ interior (K' : Set G)), μ K' :=
    le_iInf fun K' => le_iInf fun K'_hyp => le_of_lt (hc K' K'_hyp)
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc :
  ∀ (x : Compacts G),
    K.carrier ⊆ interior x.carrier →
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) < (μ : (a : Compacts G) → ℝ≥0∞) x
lower_bound_iInf :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) ≤
    ⨅ (K' : Compacts G), ⨅ (_ : (↑K : Set G) ⊆ interior (↑K' : Set G)), (μ : (a : Compacts G) → ℝ≥0∞) K'
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) ≤ (μ : (a : Compacts G) → ℝ≥0∞) K

Tactic:
rw [← H] at lower_bound_iInf
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc :
  ∀ (x : Compacts G),
    K.carrier ⊆ interior x.carrier →
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) < (μ : (a : Compacts G) → ℝ≥0∞) x
lower_bound_iInf :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) ≤ (μ : (a : Compacts G) → ℝ≥0∞) K
⊢ False

Tactic:
(lt_self_iff_false (μ K)).mp (lt_of_le_of_lt' lower_bound_iInf
    (ENNReal.lt_add_right (ne_top_of_lt (μ.lt_top K)) (ENNReal.coe_ne_zero.mpr hε)))

Premises used: Iff.mpr, ENNReal.lt_add_right, MeasureTheory.Content.lt_top, lt_of_le_of_lt', ENNReal.coe_ne_zero, lt_self_iff_false, Iff.mp, ne_top_of_lt, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
hε : ε ≠ 0
hc :
  ∀ (x : Compacts G),
    K.carrier ⊆ interior x.carrier →
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) < (μ : (a : Compacts G) → ℝ≥0∞) x
lower_bound_iInf :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) ≤ (μ : (a : Compacts G) → ℝ≥0∞) K
⊢ False

Tactic:
exact (lt_self_iff_false (μ K)).mp (lt_of_le_of_lt' lower_bound_iInf
    (ENNReal.lt_add_right (ne_top_of_lt (μ.lt_top K)) (ENNReal.coe_ne_zero.mpr hε)))

Premises used: Iff.mpr, ENNReal.lt_add_right, MeasureTheory.Content.lt_top, lt_of_le_of_lt', ENNReal.coe_ne_zero, lt_self_iff_false, Iff.mp, ne_top_of_lt, DFunLike.coe