awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h :
  ∀ ⦃K : Compacts G⦄,
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (⇑f : (a : G) → G) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
U : Opens G
K : Compacts G
hK : (↑K : Set G) ⊆ (↑((Opens.comap (↑f : C(G, G)) : (a : Opens G) → Opens G) U : Opens G) : Set G)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (⇑f : (a : G) → G) ⋯ K) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
apply h
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
h :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
g : G
U : Opens G
⊢ μ.innerContent ((Opens.comap (↑(Homeomorph.mulLeft g) : C(G, G)) : (a : Opens G) → Opens G) U) = μ.innerContent U

Tactic:
μ.innerContent_comap (Homeomorph.mulLeft g) (fun K => h g) U

Premises used: Homeomorph.mulLeft, MeasureTheory.Content.innerContent_comap
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
h :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
g : G
U : Opens G
⊢ μ.innerContent ((Opens.comap (↑(Homeomorph.mulLeft g) : C(G, G)) : (a : Opens G) → Opens G) U) = μ.innerContent U

Tactic:
convert! μ.innerContent_comap (Homeomorph.mulLeft g) (fun K => h g) U

Premises used: Homeomorph.mulLeft, MeasureTheory.Content.innerContent_comap
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU rwa rwa₁ rwa₂ rwa₃ : (↑U : Set G).Nonempty
⊢ (interior (↑U : Set G)).Nonempty

Tactic:
rwa [U.isOpen.interior_eq]

Premises used: TopologicalSpace.Opens.isOpen, IsOpen.interior_eq
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU : (↑U : Set G).Nonempty
⊢ (interior (↑U : Set G)).Nonempty

Tactic:
have : (interior (U : Set G)).Nonempty := by rwa [U.isOpen.interior_eq]
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU : (↑U : Set G).Nonempty
this : (interior (↑U : Set G)).Nonempty
rcases : ∀ (s : Finset G) (hs : K.carrier ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' (↑U : Set G)), 0 < μ.innerContent U
⊢ 0 < μ.innerContent U

Tactic:
rcases compact_covered_by_mul_left_translates K.2 this with ⟨s, hs⟩

Premises used: TopologicalSpace.Compacts.isCompact', compact_covered_by_mul_left_translates
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU : (↑U : Set G).Nonempty
this_1 : (interior (↑U : Set G)).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' (↑U : Set G)
this : (μ : (a : Compacts G) → ℝ≥0∞) K ≤ (↑s.card : ℝ≥0∞) * μ.innerContent U
⊢ 0 < μ.innerContent U

Tactic:
(ENNReal.mul_pos_iff.mp <| hK.bot_lt.trans_le this).2

Premises used: And.right, LT.lt.trans_le, Iff.mp, Ne.bot_lt, ENNReal.mul_pos_iff
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU : (↑U : Set G).Nonempty
this_1 : (interior (↑U : Set G)).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' (↑U : Set G)
this : (μ : (a : Compacts G) → ℝ≥0∞) K ≤ (↑s.card : ℝ≥0∞) * μ.innerContent U
⊢ 0 < μ.innerContent U

Tactic:
exact (ENNReal.mul_pos_iff.mp <| hK.bot_lt.trans_le this).2

Premises used: And.right, LT.lt.trans_le, Iff.mp, Ne.bot_lt, ENNReal.mul_pos_iff
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU : (↑U : Set G).Nonempty
this : (interior (↑U : Set G)).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' (↑U : Set G)
suffices : (μ : (a : Compacts G) → ℝ≥0∞) K ≤ (↑s.card : ℝ≥0∞) * μ.innerContent U
⊢ 0 < μ.innerContent U

Tactic:
suffices μ K ≤ s.card * μ.innerContent U by
    exact (ENNReal.mul_pos_iff.mp <| hK.bot_lt.trans_le this).2
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU : (↑U : Set G).Nonempty
this : (interior (↑U : Set G)).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' (↑U : Set G)
⊢ (↑K : Set G) ⊆ (↑(⨆ g ∈ s, (Opens.comap (↑(Homeomorph.mulLeft g) : C(G, G)) : (a : Opens G) → Opens G) U) : Set G)

Tactic:
simpa only [Opens.iSup_def, Opens.coe_comap, Subtype.coe_mk]

Premises used: Subtype.coe_mk, TopologicalSpace.Opens.iSup_def, TopologicalSpace.Opens.coe_comap
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU : (↑U : Set G).Nonempty
this : (interior (↑U : Set G)).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' (↑U : Set G)
⊢ (↑K : Set G) ⊆ (↑(⨆ g ∈ s, (Opens.comap (↑(Homeomorph.mulLeft g) : C(G, G)) : (a : Opens G) → Opens G) U) : Set G)

Tactic:
have : (K : Set G) ⊆ ↑(⨆ g ∈ s, Opens.comap (Homeomorph.mulLeft g : C(G, G)) U) := by
    simpa only [Opens.iSup_def, Opens.coe_comap, Subtype.coe_mk]
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU : (↑U : Set G).Nonempty
this_1 : (interior (↑U : Set G)).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' (↑U : Set G)
this :
  (↑K : Set G) ⊆ (↑(⨆ g ∈ s, (Opens.comap (↑(Homeomorph.mulLeft g) : C(G, G)) : (a : Opens G) → Opens G) U) : Set G)
⊢ (μ : (a : Compacts G) → ℝ≥0∞) K ≤ (↑s.card : ℝ≥0∞) * μ.innerContent U

Tactic:
(μ.le_innerContent _ _ this).trans ?_

Premises used: MeasureTheory.Content.le_innerContent, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU : (↑U : Set G).Nonempty
this_1 : (interior (↑U : Set G)).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' (↑U : Set G)
this :
  (↑K : Set G) ⊆ (↑(⨆ g ∈ s, (Opens.comap (↑(Homeomorph.mulLeft g) : C(G, G)) : (a : Opens G) → Opens G) U) : Set G)
refine :
  μ.innerContent (⨆ g ∈ s, (Opens.comap (↑(Homeomorph.mulLeft g) : C(G, G)) : (a : Opens G) → Opens G) U) ≤
    (↑s.card : ℝ≥0∞) * μ.innerContent U
⊢ (μ : (a : Compacts G) → ℝ≥0∞) K ≤ (↑s.card : ℝ≥0∞) * μ.innerContent U

Tactic:
refine (μ.le_innerContent _ _ this).trans ?_

Premises used: MeasureTheory.Content.le_innerContent, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU : (↑U : Set G).Nonempty
this_1 : (interior (↑U : Set G)).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' (↑U : Set G)
this :
  (↑K : Set G) ⊆ (↑(⨆ g ∈ s, (Opens.comap (↑(Homeomorph.mulLeft g) : C(G, G)) : (a : Opens G) → Opens G) U) : Set G)
⊢ μ.innerContent (⨆ g ∈ s, (Opens.comap (↑(Homeomorph.mulLeft g) : C(G, G)) : (a : Opens G) → Opens G) U) ≤
    (↑s.card : ℝ≥0∞) * μ.innerContent U

Tactic:
(rel_iSup_sum μ.innerContent μ.innerContent_bot (· ≤ ·) μ.innerContent_iSup_nat _ _).trans ?_

Premises used: MeasureTheory.Content.innerContent_iSup_nat, MeasureTheory.Content.innerContent_bot, LE.le, rel_iSup_sum, LE.le.trans, MeasureTheory.Content.innerContent
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU : (↑U : Set G).Nonempty
this_1 : (interior (↑U : Set G)).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' (↑U : Set G)
this :
  (↑K : Set G) ⊆ (↑(⨆ g ∈ s, (Opens.comap (↑(Homeomorph.mulLeft g) : C(G, G)) : (a : Opens G) → Opens G) U) : Set G)
_ :
  ∑ d ∈ s, μ.innerContent ((Opens.comap (↑(Homeomorph.mulLeft d) : C(G, G)) : (a : Opens G) → Opens G) U) ≤
    (↑s.card : ℝ≥0∞) * μ.innerContent U
⊢ μ.innerContent (⨆ g ∈ s, (Opens.comap (↑(Homeomorph.mulLeft g) : C(G, G)) : (a : Opens G) → Opens G) U) ≤
    (↑s.card : ℝ≥0∞) * μ.innerContent U

Tactic:
refine
    (rel_iSup_sum μ.innerContent μ.innerContent_bot (· ≤ ·) μ.innerContent_iSup_nat _ _).trans ?_

Premises used: MeasureTheory.Content.innerContent_iSup_nat, MeasureTheory.Content.innerContent_bot, LE.le, rel_iSup_sum, LE.le.trans, MeasureTheory.Content.innerContent
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    Eq (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (Compacts.map (fun (x : G) ↦ g * x) ⋯ K) : ℝ≥0∞)
      ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
K : Compacts G
hK : Ne (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Opens G
hU : (↑U : Set G).Nonempty
this_1 : (interior (↑U : Set G)).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun (x : G) ↦ g * x) ⁻¹' (↑U : Set G)
this :
  (↑K : Set G) ⊆ (↑(⨆ g ∈ s, (Opens.comap (↑(Homeomorph.mulLeft g) : C(G, G)) : (a : Opens G) → Opens G) U) : Set G)
⊢ ∑ d ∈ s, μ.innerContent ((Opens.comap (↑(Homeomorph.mulLeft d) : C(G, G)) : (a : Opens G) → Opens G) U) ≤
    (↑s.card : ℝ≥0∞) * μ.innerContent U

Tactic:
simp only [μ.is_mul_left_invariant_innerContent h3, Finset.sum_const, nsmul_eq_mul, le_refl]

Premises used: le_refl, MeasureTheory.Content.is_mul_left_invariant_innerContent, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
U : Opens G
⊢ (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U : Set G) = μ.innerContent U

Tactic:
inducedOuterMeasure_eq' (fun _ => isOpen_iUnion) μ.innerContent_iUnion_nat μ.innerContent_mono U.2

Premises used: MeasureTheory.inducedOuterMeasure_eq', isOpen_iUnion, TopologicalSpace.Opens.is_open', MeasureTheory.Content.innerContent_mono
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
U : Set G
hU : IsOpen U
⊢ (μ.outerMeasure : (a : Set G) → ℝ≥0∞) U = μ.innerContent { carrier := U, is_open' := hU : Opens G }

Tactic:
μ.outerMeasure_opens ⟨U, hU⟩

Premises used: TopologicalSpace.Opens.mk, MeasureTheory.Content.outerMeasure_opens
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
U : Opens G
K : Compacts G
hUK : (↑U : Set G) ⊆ (↑K : Set G)
⊢ LE.le (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U : Set G) : ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
(μ.outerMeasure_opens U).le.trans <| μ.innerContent_le U K hUK

Premises used: Eq.le, MeasureTheory.Content.outerMeasure_opens, LE.le.trans, MeasureTheory.Content.innerContent_le
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
K : Compacts G
rw :
  LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
    (⨅ (t : Set G), ⨅ (ht : IsOpen t), ⨅ (_ : (↑K : Set G) ⊆ t), μ.innerContent { carrier := t, is_open' := ht } : ℝ≥0∞)
PU : ∀ ⦃f : ℕ → Set G⦄ (_hm : ∀ (i : ℕ), IsOpen (f i)), IsOpen.{w} (X := G) (⋃ (i : ℕ), f i)
msU :
  ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    μ.innerContent { carrier := ⋃ (i : ℕ), f i, is_open' := ⋯ : Opens G } ≤
      ∑' (i : ℕ), μ.innerContent { carrier := f i, is_open' := ⋯ }
m_mono :
  ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ →
      μ.innerContent { carrier := s₁, is_open' := hs₁ : Opens G } ≤ μ.innerContent { carrier := s₂, is_open' := hs₂ }
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)

Tactic:
rw [Content.outerMeasure, inducedOuterMeasure_eq_iInf]

Premises used: MeasureTheory.inducedOuterMeasure_eq_iInf, MeasureTheory.Content.outerMeasure
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
K : Compacts G
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
    (⨅ (t : Set G), ⨅ (ht : IsOpen t), ⨅ (_ : (↑K : Set G) ⊆ t), μ.innerContent { carrier := t, is_open' := ht } : ℝ≥0∞)

Tactic:
le_iInf fun U => le_iInf fun hU => le_iInf <| μ.le_innerContent K ⟨U, hU⟩

Premises used: MeasureTheory.Content.le_innerContent, le_iInf, TopologicalSpace.Opens.mk
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
K : Compacts G
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
    (⨅ (t : Set G), ⨅ (ht : IsOpen t), ⨅ (_ : (↑K : Set G) ⊆ t), μ.innerContent { carrier := t, is_open' := ht } : ℝ≥0∞)

Tactic:
exact le_iInf fun U => le_iInf fun hU => le_iInf <| μ.le_innerContent K ⟨U, hU⟩

Premises used: MeasureTheory.Content.le_innerContent, le_iInf, TopologicalSpace.Opens.mk
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄ (_hm : ∀ (i : ℕ), IsOpen (f i)), IsOpen.{w} (X := G) (⋃ (i : ℕ), f i)

Tactic:
fun U hU => isOpen_iUnion hU

Premises used: isOpen_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄ (_hm : ∀ (i : ℕ), IsOpen (f i)), IsOpen.{w} (X := G) (⋃ (i : ℕ), f i)

Tactic:
exact fun U hU => isOpen_iUnion hU

Premises used: isOpen_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    μ.innerContent { carrier := ⋃ (i : ℕ), f i, is_open' := ⋯ : Opens G } ≤
      ∑' (i : ℕ), μ.innerContent { carrier := f i, is_open' := ⋯ }

Tactic:
μ.innerContent_iUnion_nat

Premises used: MeasureTheory.Content.innerContent_iUnion_nat
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    μ.innerContent { carrier := ⋃ (i : ℕ), f i, is_open' := ⋯ : Opens G } ≤
      ∑' (i : ℕ), μ.innerContent { carrier := f i, is_open' := ⋯ }

Tactic:
exact μ.innerContent_iUnion_nat

Premises used: MeasureTheory.Content.innerContent_iUnion_nat
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
K : Compacts G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ →
      μ.innerContent { carrier := s₁, is_open' := hs₁ : Opens G } ≤ μ.innerContent { carrier := s₂, is_open' := hs₂ }

Tactic:
μ.innerContent_mono

Premises used: MeasureTheory.Content.innerContent_mono
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
K : Compacts G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ →
      μ.innerContent { carrier := s₁, is_open' := hs₁ : Opens G } ≤ μ.innerContent { carrier := s₂, is_open' := hs₂ }

Tactic:
exact μ.innerContent_mono

Premises used: MeasureTheory.Content.innerContent_mono
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
A : Set G
⊢ Eq (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
    (⨅ (U : Set G), ⨅ (hU : IsOpen U), ⨅ (_ : A ⊆ U), μ.innerContent { carrier := U, is_open' := hU } : ℝ≥0∞)

Tactic:
inducedOuterMeasure_eq_iInf _ μ.innerContent_iUnion_nat μ.innerContent_mono A

Premises used: MeasureTheory.inducedOuterMeasure_eq_iInf, MeasureTheory.Content.innerContent_mono
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
K : Compacts G
⊢ LE.le (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (interior (↑K : Set G)) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
(μ.outerMeasure_opens <| Opens.interior K).le.trans <| μ.innerContent_le _ _ interior_subset

Premises used: interior_subset, TopologicalSpace.Opens.interior, setOf, Set.sUnion, Eq.le, SetLike.coe, interior, MeasureTheory.Content.outerMeasure_opens, LE.le.trans, MeasureTheory.Content.innerContent_le
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
U : Opens G
hU : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U : Set G) : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0
hε : ε ≠ 0
rw :
  ∀ (hU : μ.innerContent U ≠ ∞) {ε : ℝ≥0} (hε : ε ≠ 0),
    ∃ (K : Compacts G),
      (↑K : Set G) ⊆ (↑U : Set G) ∧
        μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U : Set G) ∧
      (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U : Set G) ≤
        HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
rw [μ.outerMeasure_opens] at hU ⊢

Premises used: MeasureTheory.Content.outerMeasure_opens
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
rcases :
  ∀ (K : Compacts G) (h1K : (↑K : Set G) ⊆ (↑U : Set G))
    (h2K : μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)),
    ∃ (K : Compacts G),
      (↑K : Set G) ⊆ (↑U : Set G) ∧
        μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U : Set G) ∧
      μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
rcases μ.innerContent_exists_compact hU hε with ⟨K, h1K, h2K⟩

Premises used: MeasureTheory.Content.innerContent_exists_compact
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
K : Compacts G
h1K : (↑K : Set G) ⊆ (↑U : Set G)
h2K : μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
grw :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑ε : ℝ≥0∞)
grw₁ grw₂ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑ε : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
grw [h2K, μ.le_outerMeasure_compacts K]

Premises used: MeasureTheory.Content.le_outerMeasure_compacts
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
K : Compacts G
h1K : (↑K : Set G) ⊆ (↑U : Set G)
h2K : μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ ∃ (K : Compacts G),
    (↑K : Set G) ⊆ (↑U : Set G) ∧
      μ.innerContent U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
exact ⟨K, h1K, by grw [h2K, μ.le_outerMeasure_compacts K]⟩