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 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Hν : ν.IsEverywherePos s
x : G
_hx : x ∈ s
t : Set G
t_comp : IsCompact t
t_mem : t ∈ 𝓝 x
refine :
  ∀ (u : Set G) (hu : u ⊆ t), Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞)
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
refine ⟨t, t_mem, fun u hu ↦ ?_⟩
-- 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 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Hν : ν.IsEverywherePos s
x : G
_hx : x ∈ s
t : Set G
t_comp : IsCompact t
t_mem : t ∈ 𝓝 x
u : Set G
hu : u ⊆ t
h's₁ : IsCompact (closure[inst] u)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
apply measure_isMulInvariant_eq_smul_of_isCompact_closure

Premises used: MeasureTheory.Measure.measure_isMulInvariant_eq_smul_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 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Hν : ν.IsEverywherePos s
x : G
_hx : x ∈ s
t : Set G
t_comp : IsCompact t
t_mem : t ∈ 𝓝 x
u : Set G
hu : u ⊆ t
⊢ IsCompact (closure[inst] u)

Tactic:
t_comp.closure_of_subset hu

Premises used: 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 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Hν : ν.IsEverywherePos s
x : G
_hx : x ∈ s
t : Set G
t_comp : IsCompact t
t_mem : t ∈ 𝓝 x
u : Set G
hu : u ⊆ t
⊢ IsCompact (closure[inst] u)

Tactic:
exact t_comp.closure_of_subset hu

Premises used: 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 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Hν : ν.IsEverywherePos s
⊢ μ'.IsEverywherePos s

Tactic:
have Hμ' : IsEverywherePos μ' s := by
      apply Hν.of_forall_exists_nhds_eq (fun x _hx ↦ ?_)
      obtain ⟨t, t_comp, t_mem⟩ : ∃ t, IsCompact t ∧ t ∈ 𝓝 x := exists_compact_mem_nhds x
      refine ⟨t, t_mem, fun u hu ↦ ?_⟩
      apply measure_isMulInvariant_eq_smul_of_isCompact_closure
      exact t_comp.closure_of_subset hu
-- 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 : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst] k
k_mem : Membership.mem (γ := Filter G) (𝓝 1) k
one_k : 1 ∈ k
A : Set (Set G) := {t : Set G | t ⊆ s ∧ t.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k}
m : Set G
m_max : Maximal (fun (x : Set G) ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint (α := Set G) fun (x : G) ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → Eq (α := ℝ≥0∞) ((ρ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Hν : ν.IsEverywherePos s
Hμ' : μ'.IsEverywherePos s
neg : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
neg₁ neg₂ : Eq (α := ℝ≥0∞) ∞ ∞
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [H ν Hν, H μ' Hμ']
-- 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 : μ'.IsHaarMeasure
s : Set G
hs : IsOpen[inst] s
⊢ (μ' : (a : Set G) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_isHaarMeasure_eq_smul_of_isEverywherePos μ' μ hs.measurableSet hs.isEverywherePos

Premises used: IsOpen.measurableSet, MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isEverywherePos, IsOpen.isEverywherePos
-- 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
inst_10 : μ'.InnerRegularCompactLTTop
s_1 : Set G
hs_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
h's_1 : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [ENNReal.mul_eq_top, hs.ne]

Premises used: ENNReal.mul_eq_top, LT.lt.ne
-- 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
inst_10 : μ'.InnerRegularCompactLTTop
s_1 : Set G
hs_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
h's_1 : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have : (c • μ) s ≠ ∞ := by simp [ENNReal.mul_eq_top, hs.ne]
-- 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
inst_10 : μ'.InnerRegularCompactLTTop
s_1 : Set G
hs_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
h's_1 : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ' : (a : Set G) → ℝ≥0∞) K)
    (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (c • μ : (a : Set G) → ℝ≥0∞) K)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [s_meas.measure_eq_iSup_isCompact_of_ne_top h's.ne,
        s_meas.measure_eq_iSup_isCompact_of_ne_top this]

Premises used: MeasurableSet.measure_eq_iSup_isCompact_of_ne_top, LT.lt.ne
-- 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
inst_10 : μ'.InnerRegularCompactLTTop
s_1 : Set G
hs_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
h's_1 : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (K : Set G) (_Ks : K ⊆ s) (K_comp : IsCompact K),
    Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ' : (a : Set G) → ℝ≥0∞) K)
    (⨆ (K : Set G), ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (c • μ : (a : Set G) → ℝ≥0∞) K)

Tactic:
congr! 4 with K _Ks K_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
inst_10 : μ'.InnerRegularCompactLTTop
s_1 : Set G
hs_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
h's_1 : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set G
_Ks : K ⊆ s
K_comp : IsCompact K
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
measure_isMulInvariant_eq_smul_of_isCompact_closure μ' μ K_comp.closure

Premises used: IsCompact.closure, MeasureTheory.Measure.measure_isMulInvariant_eq_smul_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
inst_10 : μ'.InnerRegularCompactLTTop
s_1 : Set G
hs_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
h's_1 : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set G
_Ks : K ⊆ s
K_comp : IsCompact K
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
exact measure_isMulInvariant_eq_smul_of_isCompact_closure μ' μ K_comp.closure

Premises used: IsCompact.closure, MeasureTheory.Measure.measure_isMulInvariant_eq_smul_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
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
⊢ ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
have B : ∀ s, MeasurableSet s → μ s < ∞ → μ' s < ∞ → μ' s = (c • μ) s := by
    intro s s_meas hs h's
    have : (c • μ) s ≠ ∞ := by simp [ENNReal.mul_eq_top, hs.ne]
    rw [s_meas.measure_eq_iSup_isCompact_of_ne_top h's.ne,
        s_meas.measure_eq_iSup_isCompact_of_ne_top this]
    congr! 4 with K _Ks K_comp
    exact measure_isMulInvariant_eq_smul_of_isCompact_closure μ' μ K_comp.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
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
⊢ s ⊆ t

Tactic:
have st : s ⊆ t := subset_inter (subset_toMeasurable μ' s) (subset_toMeasurable μ s)
-- 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
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
a : LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
a₁ : LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply le_antisymm

Premises used: 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
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
(measure_mono inter_subset_left).trans (measure_toMeasurable s).le

Premises used: Eq.le, Set.inter_subset_left, MeasureTheory.measure_toMeasurable, MeasureTheory.measure_mono, LE.le.trans
-- 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
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
⊢ LE.le (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact (measure_mono inter_subset_left).trans (measure_toMeasurable s).le

Premises used: Eq.le, Set.inter_subset_left, MeasureTheory.measure_toMeasurable, MeasureTheory.measure_mono, LE.le.trans
-- 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
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
⊢ 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
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
⊢ 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
-- 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
inst_10 : μ'.InnerRegularCompactLTTop
s : Set G
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0 := μ'.haarScalarFactor μ
B :
  ∀ (s : Set G),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((c • μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
have mu'_t : μ' t = μ' s := by
    apply le_antisymm
    · exact (measure_mono inter_subset_left).trans (measure_toMeasurable s).le
    · exact measure_mono st