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
A : Set G
hA : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0
hε : ε ≠ 0
rcases :
  ∀ (U : Set G) (hU : IsOpen U) (h2U : A ⊆ U)
    (h3U :
      ((inducedOuterMeasure (P := IsOpen)
                (fun (s₁ : Set G) (hs₁ : IsOpen s₁) ↦ μ.innerContent { carrier := s₁, is_open' := hs₁ }) ⋯ ⋯ :
              OuterMeasure G) :
            (a : Set G) → ℝ≥0∞)
          U ≤
        HAdd.hAdd (α := ℝ≥0∞)
          (((inducedOuterMeasure (P := IsOpen)
                    (fun (s₁ : Set G) (hs₁ : IsOpen s₁) ↦ μ.innerContent { carrier := s₁, is_open' := hs₁ : Opens G }) ⋯
                    ⋯ :
                  OuterMeasure G) :
                (a : Set G) → ℝ≥0∞)
              A :
            ℝ≥0∞)
          (↑ε : ℝ≥0∞)),
    ∃ (U : Opens G),
      A ⊆ (↑U : Set G) ∧
        (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U : Set G) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ ∃ (U : Opens G),
    A ⊆ (↑U : Set G) ∧
      (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U : Set G) ≤
        HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
rcases inducedOuterMeasure_exists_set _ μ.innerContent_iUnion_nat μ.innerContent_mono hA
      (ENNReal.coe_ne_zero.2 hε) with
    ⟨U, hU, h2U, h3U⟩

Premises used: Iff.mpr, MeasureTheory.inducedOuterMeasure_exists_set, ENNReal.coe_ne_zero, 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
hA : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0
hε : ε ≠ 0
U : Set G
hU : IsOpen U
h2U : A ⊆ U
h3U :
  ((inducedOuterMeasure (P := IsOpen)
            (fun (s₁ : Set G) (hs₁ : IsOpen s₁) ↦ μ.innerContent { carrier := s₁, is_open' := hs₁ }) ⋯ ⋯ :
          OuterMeasure G) :
        (a : Set G) → ℝ≥0∞)
      U ≤
    HAdd.hAdd (α := ℝ≥0∞)
      (((inducedOuterMeasure (P := IsOpen)
                (fun (s₁ : Set G) (hs₁ : IsOpen s₁) ↦ μ.innerContent { carrier := s₁, is_open' := hs₁ : Opens G }) ⋯ ⋯ :
              OuterMeasure G) :
            (a : Set G) → ℝ≥0∞)
          A :
        ℝ≥0∞)
      (↑ε : ℝ≥0∞)
⊢ ∃ (U : Opens G),
    A ⊆ (↑U : Set G) ∧
      (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U : Set G) ≤
        HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
⟨⟨U, hU⟩, h2U, h3U⟩

Premises used: TopologicalSpace.Opens.mk, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
A : Set G
hA : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0
hε : ε ≠ 0
U : Set G
hU : IsOpen U
h2U : A ⊆ U
h3U :
  ((inducedOuterMeasure (P := IsOpen)
            (fun (s₁ : Set G) (hs₁ : IsOpen s₁) ↦ μ.innerContent { carrier := s₁, is_open' := hs₁ }) ⋯ ⋯ :
          OuterMeasure G) :
        (a : Set G) → ℝ≥0∞)
      U ≤
    HAdd.hAdd (α := ℝ≥0∞)
      (((inducedOuterMeasure (P := IsOpen)
                (fun (s₁ : Set G) (hs₁ : IsOpen s₁) ↦ μ.innerContent { carrier := s₁, is_open' := hs₁ : Opens G }) ⋯ ⋯ :
              OuterMeasure G) :
            (a : Set G) → ℝ≥0∞)
          A :
        ℝ≥0∞)
      (↑ε : ℝ≥0∞)
⊢ ∃ (U : Opens G),
    A ⊆ (↑U : Set G) ∧
      (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U : Set G) ≤
        HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
exact ⟨⟨U, hU⟩, h2U, h3U⟩
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space 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∞)
A : Set G
⊢ Eq (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((⇑f : (a : G) → G) ⁻¹' A) : ℝ≥0∞)
    ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
inducedOuterMeasure_preimage _ μ.innerContent_iUnion_nat μ.innerContent_mono _
    (fun _ => f.isOpen_preimage) ?_

Premises used: MeasureTheory.inducedOuterMeasure_preimage, MeasureTheory.Content.innerContent_mono, Homeomorph.isOpen_preimage
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space 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∞)
A : Set G
refine :
  ∀ (s : Set G) (hs : IsOpen s),
    μ.innerContent { carrier := (⇑f.toEquiv : (a : G) → G) ⁻¹' s, is_open' := ⋯ : Opens G } =
      μ.innerContent { carrier := s, is_open' := hs }
⊢ Eq (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((⇑f : (a : G) → G) ⁻¹' A) : ℝ≥0∞)
    ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
refine inducedOuterMeasure_preimage _ μ.innerContent_iUnion_nat μ.innerContent_mono _
    (fun _ => f.isOpen_preimage) ?_

Premises used: MeasureTheory.inducedOuterMeasure_preimage, MeasureTheory.Content.innerContent_mono, Homeomorph.isOpen_preimage
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space 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∞)
A s : Set G
hs : IsOpen s
⊢ μ.innerContent ((Opens.comap (↑f : C(G, G)) : (a : Opens G) → Opens G) { carrier := s, is_open' := hs : Opens G }) =
    μ.innerContent { carrier := s, is_open' := hs }

Tactic:
μ.innerContent_comap f h ⟨s, hs⟩

Premises used: TopologicalSpace.Opens.mk, MeasureTheory.Content.innerContent_comap
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space 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∞)
A s : Set G
hs : IsOpen s
⊢ μ.innerContent { carrier := (⇑f.toEquiv : (a : G) → G) ⁻¹' s, is_open' := ⋯ : Opens G } =
    μ.innerContent { carrier := s, is_open' := hs }

Tactic:
convert! μ.innerContent_comap f h ⟨s, hs⟩

Premises used: TopologicalSpace.Opens.mk, MeasureTheory.Content.innerContent_comap
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
inst_2 : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
rcases :
  ∀ (F : Set G) (h1F : IsCompact F) (h2F : K ⊆ interior F),
    LT.lt (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rcases exists_compact_superset hK with ⟨F, h1F, h2F⟩

Premises used: exists_compact_superset
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
inst_2 : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
F : Set G
h1F : IsCompact F
h2F : K ⊆ interior F
⊢ LE.le (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
    ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (interior F) : ℝ≥0∞)

Tactic:
measure_mono h2F

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
inst_2 : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
F : Set G
h1F : IsCompact F
h2F : K ⊆ interior F
⊢ LE.le (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (interior F) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) { carrier := F, isCompact' := h1F } : ℝ≥0∞)

Tactic:
apply μ.outerMeasure_le ⟨interior F, isOpen_interior⟩ ⟨F, h1F⟩ interior_subset

Premises used: interior_subset, isOpen_interior, MeasureTheory.Content.outerMeasure_le, TopologicalSpace.Compacts.mk, TopologicalSpace.Opens.mk, interior
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
inst_2 : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
F : Set G
h1F : IsCompact F
h2F : K ⊆ interior F
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) { carrier := F, isCompact' := h1F } : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
μ.lt_top _

Premises used: MeasureTheory.Content.lt_top
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
inst_2 : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
F : Set G
h1F : IsCompact F
h2F : K ⊆ interior F
K₁ :
  LE.le (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (interior F) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) { carrier := F, isCompact' := h1F } : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
calc
    μ.outerMeasure K ≤ μ.outerMeasure (interior F) := measure_mono h2F
    _ ≤ μ ⟨F, h1F⟩ := by
      apply μ.outerMeasure_le ⟨interior F, isOpen_interior⟩ ⟨F, h1F⟩ interior_subset
    _ < ⊤ := μ.lt_top _

Premises used: MeasureTheory.Content.lt_top, TopologicalSpace.Compacts.mk, MeasureTheory.Content.outerMeasure, interior, MeasureTheory.measure_mono, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
inst_2 : Group G
inst_3 : 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
A : Set G
⊢ Eq (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((⇑(Homeomorph.mulLeft g) : (a : G) → G) ⁻¹' A) : ℝ≥0∞)
    ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
μ.outerMeasure_preimage (Homeomorph.mulLeft g) (fun K => h g) A

Premises used: MeasureTheory.Content.outerMeasure_preimage, Homeomorph.mulLeft
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
inst_2 : Group G
inst_3 : 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
A : Set G
⊢ Eq (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' A) : ℝ≥0∞)
    ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)

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

Premises used: MeasureTheory.Content.outerMeasure_preimage, Homeomorph.mulLeft
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
A : Set G
rw :
  MeasurableSet A ↔
    ∀ (U : Set G) (hU : IsOpen U),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑{ carrier := U, is_open' := hU : Opens G } : Set G) ∩ A) : ℝ≥0∞)
          ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑{ carrier := U, is_open' := hU : Opens G } : Set G) \ A) : ℝ≥0∞) ≤
        (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑{ carrier := U, is_open' := hU : Opens G } : Set G)
⊢ MeasurableSet A ↔
    ∀ (U : Opens G),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U : Set G) ∩ A) : ℝ≥0∞)
          ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U : Set G) \ A) : ℝ≥0∞) ≤
        (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U : Set G)

Tactic:
rw [Opens.forall]

Premises used: TopologicalSpace.Opens.forall
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
A : Set G
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₂ }
PU : ∀ ⦃f : ℕ → Set G⦄ (_hm : ∀ (i : ℕ), IsOpen (f i)), IsOpen.{w} (X := G) (⋃ (i : ℕ), f i)
⊢ MeasurableSet A ↔
    ∀ (U : Set G) (hU : IsOpen U),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑{ carrier := U, is_open' := hU : Opens G } : Set G) ∩ A) : ℝ≥0∞)
          ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑{ carrier := U, is_open' := hU : Opens G } : Set G) \ A) : ℝ≥0∞) ≤
        (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑{ carrier := U, is_open' := hU : Opens G } : Set G)

Tactic:
apply inducedOuterMeasure_caratheodory

Premises used: MeasureTheory.inducedOuterMeasure_caratheodory
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
A : Set 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:
apply 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
A : Set 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:
apply 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
inst_2 : Group G
inst_3 : 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 : Set G
h1U : IsOpen U
h2U : U.Nonempty
⊢ 0 < μ.innerContent { carrier := U, is_open' := h1U : Opens G }

Tactic:
μ.innerContent_pos_of_is_mul_left_invariant h3 K hK ⟨U, h1U⟩ h2U

Premises used: TopologicalSpace.Opens.mk, MeasureTheory.Content.innerContent_pos_of_is_mul_left_invariant
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
inst_2 : Group G
inst_3 : 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 : Set G
h1U : IsOpen U
h2U : U.Nonempty
h : (μ.outerMeasure : (a : Set G) → ℝ≥0∞) U = μ.innerContent { carrier := U, is_open' := h1U : Opens G }
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
convert! μ.innerContent_pos_of_is_mul_left_invariant h3 K hK ⟨U, h1U⟩ h2U

Premises used: TopologicalSpace.Opens.mk, MeasureTheory.Content.innerContent_pos_of_is_mul_left_invariant
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : R1Space G
inst_2 : Group G
inst_3 : 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 : Set G
h1U : IsOpen U
h2U : U.Nonempty
⊢ (μ.outerMeasure : (a : Set G) → ℝ≥0∞) U = μ.innerContent { carrier := U, is_open' := h1U : Opens G }

Tactic:
μ.outerMeasure_opens ⟨U, h1U⟩

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
inst_2 : Group G
inst_3 : 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 : Set G
h1U : IsOpen U
h2U : U.Nonempty
⊢ (μ.outerMeasure : (a : Set G) → ℝ≥0∞) U = μ.innerContent { carrier := U, is_open' := h1U : Opens G }

Tactic:
exact μ.outerMeasure_opens ⟨U, h1U⟩

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
S : MeasurableSpace G
inst_2 : BorelSpace G
rw : borel G ≤ μ.outerMeasure.caratheodory
⊢ S ≤ μ.outerMeasure.caratheodory

Tactic:
rw [BorelSpace.measurable_eq (α := G)]

Premises used: BorelSpace.measurable_eq
-- 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
⊢ borel G ≤ μ.outerMeasure.caratheodory

Tactic:
MeasurableSpace.generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_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
refine : ∀ (t : Set G), Membership.mem (γ := Set (Set G)) {s : Set G | IsOpen s} t → MeasurableSet t
⊢ borel G ≤ μ.outerMeasure.caratheodory

Tactic:
refine MeasurableSpace.generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_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
U : Set G
hU : Membership.mem (γ := Set (Set G)) {s : Set G | IsOpen s} U
rw :
  ∀ (U_1 : Opens G),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U_1 : Set G) ∩ U) : ℝ≥0∞)
        ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U_1 : Set G) \ U) : ℝ≥0∞) ≤
      (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U_1 : Set G)
⊢ MeasurableSet U

Tactic:
rw [μ.outerMeasure_caratheodory]

Premises used: MeasureTheory.Content.outerMeasure_caratheodory
-- 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
rw :
  HAdd.hAdd (β := ℝ≥0∞) (μ.innerContent { carrier := (↑U' : Set G) ∩ U, is_open' := ⋯ : Opens G })
      ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U' : Set G) \ U) : ℝ≥0∞) ≤
    (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U' : Set G)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U' : Set G) ∩ U) : ℝ≥0∞)
      ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U' : Set G) \ U) : ℝ≥0∞) ≤
    (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U' : Set G)

Tactic:
rw [μ.outerMeasure_of_isOpen ((U' : Set G) ∩ U) (U'.isOpen.inter hU)]

Premises used: Inter.inter, SetLike.coe, TopologicalSpace.Opens.isOpen, IsOpen.inter, 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
simp :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (⨆ (x :
          { i : Compacts G // (↑i : Set G) ⊆ (↑{ carrier := (↑U' : Set G) ∩ U, is_open' := ⋯ : Opens G } : Set G) }),
          (μ : (a : Compacts G) → ℝ≥0∞) (↑x : Compacts G) :
        ℝ≥0∞)
      ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U' : Set G) \ U) : ℝ≥0∞) ≤
    (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U' : Set G)
⊢ HAdd.hAdd (β := ℝ≥0∞) (μ.innerContent { carrier := (↑U' : Set G) ∩ U, is_open' := ⋯ : Opens G })
      ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U' : Set G) \ U) : ℝ≥0∞) ≤
    (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U' : Set G)

Tactic:
simp only [innerContent, iSup_subtype']

Premises used: iSup_subtype', MeasureTheory.Content.innerContent
-- 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
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (⨆ (x : { i : Compacts G // (↑i : Set G) ⊆ (↑U' : Set G) ∩ U }), (μ : (a : Compacts G) → ℝ≥0∞) (↑x : Compacts G) :
        ℝ≥0∞)
      ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U' : Set G) \ U) : ℝ≥0∞) ≤
    (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U' : Set G)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (⨆ (x :
          { i : Compacts G // (↑i : Set G) ⊆ (↑{ carrier := (↑U' : Set G) ∩ U, is_open' := ⋯ : Opens G } : Set G) }),
          (μ : (a : Compacts G) → ℝ≥0∞) (↑x : Compacts G) :
        ℝ≥0∞)
      ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U' : Set G) \ U) : ℝ≥0∞) ≤
    (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U' : Set G)

Tactic:
rw [Opens.coe_mk]

Premises used: TopologicalSpace.Opens.coe_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
U : Set G
hU : Membership.mem (γ := Set (Set G)) {s : Set G | IsOpen s} U
U' : Opens G
⊢ Nonempty.{max 1 (w + 1)} { L : Compacts G // (↑L : Set G) ⊆ (↑U' : Set G) ∩ U }

Tactic:
haveI : Nonempty { L : Compacts G // (L : Set G) ⊆ U' ∩ U } := ⟨⟨⊥, empty_subset _⟩⟩
-- 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 : Nonempty.{max 1 (w + 1)} { L : Compacts G // (↑L : Set G) ⊆ (↑U' : Set G) ∩ U }
rw :
  LE.le (α := ℝ≥0∞)
    (⨆ (i : { i : Compacts G // (↑i : Set G) ⊆ (↑U' : Set G) ∩ U }),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (↑i : Compacts G) : ℝ≥0∞)
          ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U' : Set G) \ U) : ℝ≥0∞) :
      ℝ≥0∞)
    ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U' : Set G) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (⨆ (x : { i : Compacts G // (↑i : Set G) ⊆ (↑U' : Set G) ∩ U }), (μ : (a : Compacts G) → ℝ≥0∞) (↑x : Compacts G) :
        ℝ≥0∞)
      ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U' : Set G) \ U) : ℝ≥0∞) ≤
    (μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U' : Set G)

Tactic:
rw [ENNReal.iSup_add]

Premises used: ENNReal.iSup_add
-- 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 : Nonempty.{max 1 (w + 1)} { L : Compacts G // (↑L : Set G) ⊆ (↑U' : Set G) ∩ U }
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (i : { i : Compacts G // (↑i : Set G) ⊆ (↑U' : Set G) ∩ U }),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) (↑i : Compacts G) : ℝ≥0∞)
          ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) ((↑U' : Set G) \ U) : ℝ≥0∞) :
      ℝ≥0∞)
    ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (↑U' : Set G) : ℝ≥0∞)

Tactic:
iSup_le ?_

Premises used: iSup_le