-- 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:
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
x : G
hx : x ∈ ⋃ a ∈ c, a
y : G
hy : y ∈ ⋃ a ∈ c, a
hxy : x ≠ y
⊢ (Disjoint on fun x => x • k) x y

Tactic:
simp only [mem_iUnion, exists_prop] at hx hy

Result:
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
x y : G
hxy : x ≠ y
hx : ∃ i ∈ c, x ∈ i
hy : ∃ i ∈ c, y ∈ i
⊢ (Disjoint on fun x => x • k) x y

Proof state:
case h.refine_2.intro.intro.intro.intro
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
x y : G
hxy : x ≠ y
a : Set G
ac : a ∈ c
xa : x ∈ a
b : Set G
bc : b ∈ c
yb : y ∈ b
⊢ (Disjoint on fun x => x • k) x y

Tactic:
obtain ⟨m, mc, am, bm⟩ : ∃ m ∈ c, a ⊆ m ∧ b ⊆ m := hc.directedOn _ ac _ bc

Result:
case h.refine_2.intro.intro.intro.intro.intro.intro.intro
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
x y : G
hxy : x ≠ y
a : Set G
ac : a ∈ c
xa : x ∈ a
b : Set G
bc : b ∈ c
yb : y ∈ b
m : Set G
mc : m ∈ c
am : a ⊆ m
bm : b ⊆ m
⊢ (Disjoint on fun x => x • k) x y

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
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → ρ s = ⊤
Hν : ν.IsEverywherePos s
x : G
_hx : x ∈ s
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ' u = ν u

Tactic:
obtain ⟨t, t_comp, t_mem⟩ : ∃ t, IsCompact t ∧ t ∈ 𝓝 x := exists_compact_mem_nhds x

Result:
case intro.intro
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
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ' u = ν u

Proof state:
case pos.intro.e_f.h.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}
f : ℕ → G
m_max : Maximal (fun x => x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint fun x => x • k
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet (disjointed (fun n => s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ y, f y • (k * k⁻¹)
s_eq : s = ⋃ n, s ∩ f n • (k * k⁻¹)
I : μ' s = ∑' (n : ℕ), μ' (disjointed (fun n => s ∩ f n • (k * k⁻¹)) n)
J : ν s = ∑' (n : ℕ), ν (disjointed (fun n => s ∩ f n • (k * k⁻¹)) n)
n : ℕ
⊢ IsCompact (closure (disjointed (fun n => s ∩ f n • (k * k⁻¹)) n))

Tactic:
have : IsCompact (f n • (k * k⁻¹)) := IsCompact.smul (f n) (k_comp.mul k_comp.inv)

Result:
case pos.intro.e_f.h.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}
f : ℕ → G
m_max : Maximal (fun x => x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint fun x => x • k
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet (disjointed (fun n => s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ y, f y • (k * k⁻¹)
s_eq : s = ⋃ n, s ∩ f n • (k * k⁻¹)
I : μ' s = ∑' (n : ℕ), μ' (disjointed (fun n => s ∩ f n • (k * k⁻¹)) n)
J : ν s = ∑' (n : ℕ), ν (disjointed (fun n => s ∩ f n • (k * k⁻¹)) n)
n : ℕ
this : IsCompact (f n • (k * k⁻¹))
⊢ IsCompact (closure (disjointed (fun n => s ∩ f n • (k * k⁻¹)) n))