awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
r : ℝ≥0∞
hr : r < HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
ν : Measure G := μ'.haarScalarFactor μ • μ
this : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ r < (ν : (a : Set G) → ℝ≥0∞) s

Tactic:
convert! hr
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
r : ℝ≥0∞
hr : r < HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
ν : Measure G := μ'.haarScalarFactor μ • μ
this : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
obtain :
  ∀ (f : G → ℝ) (f_cont : Continuous[inst, _] f) (f_comp : HasCompactSupport f) (hf : f ⁻¹' {1} ⊆ s)
    (νf : r < (ν : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1})), r < (μ' : (a : Set G) → ℝ≥0∞) s
⊢ r < (μ' : (a : Set G) → ℝ≥0∞) s

Tactic:
obtain ⟨-, hf, ⟨f, f_cont, f_comp, rfl⟩, νf⟩ :
      ∃ K ⊆ s, (∃ f, Continuous f ∧ HasCompactSupport f ∧ K = f ⁻¹' {1}) ∧ r < ν K :=
    innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group ⟨hs, this⟩ r
      (by convert! hr)

Premises used: MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group, And.intro, rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
r : ℝ≥0∞
hr : r < HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
ν : Measure G := μ'.haarScalarFactor μ • μ
this : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
hf : f ⁻¹' {1} ⊆ s
νf : r < (ν : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1})
⊢ r < (ν : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1})

Tactic:
νf
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
r : ℝ≥0∞
hr : r < HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
ν : Measure G := μ'.haarScalarFactor μ • μ
this : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
hf : f ⁻¹' {1} ⊆ s
νf : r < (ν : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1})
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)

Tactic:
(measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport _ _ f_cont f_comp).symm

Premises used: MeasureTheory.Measure.measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
r : ℝ≥0∞
hr : r < HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
ν : Measure G := μ'.haarScalarFactor μ • μ
this : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
hf : f ⁻¹' {1} ⊆ s
νf : r < (ν : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1})
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_mono hf

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
r : ℝ≥0∞
hr : r < HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
ν : Measure G := μ'.haarScalarFactor μ • μ
this : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : G → ℝ
f_cont : Continuous[inst, _] f
f_comp : HasCompactSupport f
hf : f ⁻¹' {1} ⊆ s
νf : r < (ν : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1})
⊢ r < (μ' : (a : Set G) → ℝ≥0∞) s

Tactic:
calc
  r < ν (f ⁻¹' {1}) := νf
  _ = μ' (f ⁻¹' {1}) :=
    (measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport _ _ f_cont f_comp).symm
  _ ≤ μ' s := measure_mono hf

Premises used: Set.preimage, MeasureTheory.Measure.measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport, MeasureTheory.measure_mono, Singleton.singleton, OfNat.ofNat, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
apply :
  (μ' : (a : Set G) → ℝ≥0∞) s ≤ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply le_antisymm ?_ (smul_measure_isMulInvariant_le_of_isCompact_closure μ' μ hs h's)

Premises used: MeasureTheory.Measure.smul_measure_isMulInvariant_le_of_isCompact_closure, le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
change : LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ' : (a : Set G) → ℝ≥0∞) s ≤ HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
change μ' s ≤ ν s

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
⊢ ∃ (f : C(G, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : G) → ℝ) 1 (closure[inst] s) ∧
      EqOn (α := G) (β := ℝ) (⇑f : (a : G) → ℝ) 0 ∅ ∧
        HasCompactSupport (α := G) (β := ℝ) (⇑f : (a : G) → ℝ) ∧
          ∀ (x : G), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : G) → ℝ) x : ℝ)

Tactic:
exists_continuous_one_zero_of_isCompact h's isClosed_empty (disjoint_empty _)

Premises used: exists_continuous_one_zero_of_isCompact, isClosed_empty, Set.disjoint_empty
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
obtain :
  ∀ (f : G → ℝ) (f_cont : Continuous[inst, _] f)
    (hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s))
    (f_comp :
      HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)),
    LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
obtain ⟨⟨f, f_cont⟩, hf, -, f_comp, -⟩ : ∃ f : C(G, ℝ), EqOn f 1 (closure s) ∧ EqOn f 0 ∅
      ∧ HasCompactSupport f ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
    exists_continuous_one_zero_of_isCompact h's isClosed_empty (disjoint_empty _)

Premises used: exists_continuous_one_zero_of_isCompact, isClosed_empty, Set.disjoint_empty
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
⊢ IsClosed[inst] t

Tactic:
have t_closed : IsClosed t := isClosed_singleton.preimage f_cont
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
⊢ 0 ∉ {1}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
⊢ IsCompact t

Tactic:
have t_comp : IsCompact t := f_comp.isCompact_preimage f_cont isClosed_singleton (by simp)
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
⊢ s ⊆ t

Tactic:
have st : s ⊆ t := (IsClosed.closure_subset_iff t_closed).mp hf
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
apply : IsCompact (closure[inst] (t \ s))
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
apply smul_measure_isMulInvariant_le_of_isCompact_closure _ _ (t_closed.measurableSet.diff hs)

Premises used: MeasurableSet.diff, IsClosed.measurableSet, MeasureTheory.Measure.smul_measure_isMulInvariant_le_of_isCompact_closure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
⊢ IsCompact (closure[inst] (t \ s))

Tactic:
t_comp.closure_of_subset diff_subset

Premises used: Set.diff_subset, IsCompact.closure_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
⊢ IsCompact (closure[inst] (t \ s))

Tactic:
exact t_comp.closure_of_subset diff_subset

Premises used: Set.diff_subset, IsCompact.closure_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
have A : ν (t \ s) ≤ μ' (t \ s) := by
    apply smul_measure_isMulInvariant_le_of_isCompact_closure _ _ (t_closed.measurableSet.diff hs)
    exact t_comp.closure_of_subset diff_subset
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
A : LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
have B : μ' t = ν t :=
    measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport _ _ f_cont f_comp
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
A : LE.le (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h :
  ∀
    (A :
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
        HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
    (B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h' :
  ∀
    (A :
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
        HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
    (B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
    Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rwa :
  ∀
    (A :
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
        (μ' : (a : Set G) → ℝ≥0∞) (t \ s))
    (B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
    Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rwa₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rwa [measure_diff st hs.nullMeasurableSet, measure_diff st hs.nullMeasurableSet, ← B,
    ENNReal.sub_le_sub_iff_left] at A

Premises used: MeasurableSet.nullMeasurableSet, ENNReal.sub_le_sub_iff_left, MeasureTheory.measure_diff
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
A :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
measure_mono st

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
μ' μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
inst_9 : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst, _] f
hf : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 (closure[inst] s)
f_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ)
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst] t
t_comp : IsCompact t
st : s ⊆ t
A :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
B : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact measure_mono st

Premises used: MeasureTheory.measure_mono