-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
theorem measure_isHaarMeasure_eq_smul_of_isEverywherePos [LocallyCompactSpace G]
    (μ' μ : Measure G) [IsHaarMeasure μ] [IsHaarMeasure μ']
    {s : Set G} (hs : MeasurableSet s) (h's : IsEverywherePos μ s) :
    μ' s = haarScalarFactor μ' μ • μ s

Proof state:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x => x • k}
m : Set G
m_max : Maximal (fun x => x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint fun x => x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : ↑m), MeasurableSet (s ∩ ↑i • k)
h'm : ρ s ≠ ⊤
this : ∑' (x : ↑m), ρ (s ∩ ↑x • k) < ⊤
C : (support fun i => ρ (s ∩ ↑i • k)).Countable
i : ↑m
⊢ s ∩ ↑i • k ∈ 𝓝[s] ↑i

Tactic:
exact inter_mem_nhdsWithin s (by simpa)

Result:
no goals

Proof state:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x => x • k}
m : Set G
m_max : Maximal (fun x => x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint fun x => x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : ↑m), MeasurableSet (s ∩ ↑i • k)
h'm : ρ s ≠ ⊤
I : m.PairwiseDisjoint fun x => s ∩ x • k
⊢ Pairwise (Disjoint on fun i => s ∩ ↑i • k)

Tactic:
exact I.on_injective Subtype.val_injective (fun x ↦ x.2)

Result:
no goals

Proof state:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x => x • k}
m : Set G
m_max : Maximal (fun x => x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint fun x => x • k
y : G
hy : y ∈ s
h'y : m ∪ {y} ∉ A
x : G
xm : x ∈ m
z : G
zy : z ∈ y • k
zx : z ∈ x • k
⊢ y ∈ x • (k * k⁻¹)

Tactic:
rw [show y = x * ((x⁻¹ * z) * (y⁻¹ * z)⁻¹) by group]

Result:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x => x • k}
m : Set G
m_max : Maximal (fun x => x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint fun x => x • k
y : G
hy : y ∈ s
h'y : m ∪ {y} ∉ A
x : G
xm : x ∈ m
z : G
zy : z ∈ y • k
zx : z ∈ x • k
⊢ x * (x⁻¹ * z * (y⁻¹ * z)⁻¹) ∈ x • (k * k⁻¹)

Proof state:
case pos
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x => x • k}
m : Set G
m_max : Maximal (fun x => x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint fun x => x • k
y : G
hy : y ∈ s
h'y : m ∪ {y} ∈ A
ym : y ∈ m
this : y ∈ y • (k * k⁻¹)
⊢ y ∈ ⋃ x ∈ m, x • (k * k⁻¹)

Tactic:
exact mem_biUnion ym this

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x => x • k}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
⊢ ∃ ub ∈ A, ∀ s ∈ c, s ⊆ ub

Tactic:
refine ⟨⋃ a ∈ c, a, ⟨?_, ?_⟩, ?_⟩

Result:
case h.refine_1
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x => x • k}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
⊢ ⋃ a ∈ c, a ⊆ s

case h.refine_2
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x => x • k}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
⊢ (⋃ a ∈ c, a).PairwiseDisjoint fun x => x • k

case h.refine_3
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x => x • k}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
⊢ ∀ s ∈ c, s ⊆ ⋃ a ∈ c, a

Proof state:
case intro.intro.h's
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x => x • k}
m : Set G
m_max : Maximal (fun x => x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint fun x => x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → ρ s = ⊤
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 u)

Tactic:
exact t_comp.closure_of_subset hu

Result:
no goals