G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
⊢ ∃ L, MeasurableSet L ∧ L ⊆ E ∧ 0 < ↑↑μ L ∧ ↑↑μ L < ⊤

case intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
⊢ E / E ∈ 𝓝 1
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
⊢ E / E ∈ 𝓝 1
obtain ⟨L, hL, hLE, hLpos, hLtop⟩ : ∃ L : Set G, MeasurableSet L ∧ L ⊆ E ∧ 0 < μ L ∧ μ L < ∞
case intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
⊢ E / E ∈ 𝓝 1
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
⊢ ∃ L, MeasurableSet L ∧ L ⊆ E ∧ 0 < ↑↑μ L ∧ ↑↑μ L < ⊤

case intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
⊢ E / E ∈ 𝓝 1
exact exists_subset_measure_lt_top hE hEpos
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
⊢ ∃ K, K ⊆ L ∧ IsCompact K ∧ 0 < ↑↑μ K

case intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
⊢ E / E ∈ 𝓝 1
case intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
⊢ E / E ∈ 𝓝 1
obtain ⟨K, hKL, hK, hKpos⟩ : ∃ (K : Set G), K ⊆ L ∧ IsCompact K ∧ 0 < μ K
case intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
⊢ E / E ∈ 𝓝 1
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
⊢ ∃ K, K ⊆ L ∧ IsCompact K ∧ 0 < ↑↑μ K

case intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
⊢ E / E ∈ 𝓝 1
exact MeasurableSet.exists_lt_isCompact_of_ne_top hL (ne_of_lt hLtop) hLpos
case intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
⊢ E / E ∈ 𝓝 1
case intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
⊢ E / E ∈ 𝓝 1
have hKtop : μ K ≠ ∞ := by
  apply ne_top_of_le_ne_top (ne_of_lt hLtop)
  apply measure_mono hKL
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
⊢ ∃ U, U ⊇ K ∧ IsOpen U ∧ ↑↑μ U < ↑↑μ K + ↑↑μ K

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
⊢ E / E ∈ 𝓝 1
case intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
⊢ E / E ∈ 𝓝 1
obtain ⟨U, hUK, hU, hμUK⟩ : ∃ (U : Set G), U ⊇ K ∧ IsOpen U ∧ μ U < μ K + μ K
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
⊢ E / E ∈ 𝓝 1
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
⊢ ∃ U, U ⊇ K ∧ IsOpen U ∧ ↑↑μ U < ↑↑μ K + ↑↑μ K

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
⊢ E / E ∈ 𝓝 1
exact Set.exists_isOpen_lt_add K hKtop hKpos.ne'
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
⊢ ∃ V, V ∈ 𝓝 1 ∧ V * K ⊆ U

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
⊢ E / E ∈ 𝓝 1
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
⊢ E / E ∈ 𝓝 1
obtain ⟨V, hV1, hVKU⟩ : ∃ V ∈ 𝓝 (1 : G), V * K ⊆ U
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
⊢ E / E ∈ 𝓝 1
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
⊢ ∃ V, V ∈ 𝓝 1 ∧ V * K ⊆ U

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
⊢ E / E ∈ 𝓝 1
exact compact_open_separated_mul_left hK hU hUK
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
⊢ E / E ∈ 𝓝 1
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
⊢ E / E ∈ 𝓝 1
have hv : ∀ v : G, v ∈ V → ¬Disjoint ({v} * K) K := by
  intro v hv hKv
  have hKvsub : {v} * K ∪ K ⊆ U := by
    apply Set.union_subset _ hUK
    apply _root_.subset_trans _ hVKU
    apply Set.mul_subset_mul _ (Set.Subset.refl K)
    simp only [Set.singleton_subset_iff, hv]
  replace hKvsub := @measure_mono _ _ μ _ _ hKvsub
  have hcontr := lt_of_le_of_lt hKvsub hμUK
  rw [measure_union hKv (IsCompact.measurableSet hK)] at hcontr
  have hKtranslate : μ ({v} * K) = μ K := by
    simp only [singleton_mul, image_mul_left, measure_preimage_mul]
  rw [hKtranslate, lt_self_iff_false] at hcontr
  assumption
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
this : V ⊆ E / E
⊢ E / E ∈ 𝓝 1

case this
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
⊢ V ⊆ E / E
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
⊢ E / E ∈ 𝓝 1
suffices : V ⊆ E / E
case this
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
⊢ V ⊆ E / E
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
this : V ⊆ E / E
⊢ E / E ∈ 𝓝 1

case this
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
⊢ V ⊆ E / E
exact Filter.mem_of_superset hV1 this
case this
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
⊢ v ∈ E / E
case this
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
⊢ V ⊆ E / E
intro v hvV
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
⊢ ∃ x, x ∈ ?m.265493 x * K ∧ x ∈ K

case this.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
x : G
hxK : x ∈ ?m.265493 x * K
hxvK : x ∈ K
⊢ v ∈ E / E
case this
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
⊢ v ∈ E / E
obtain ⟨x, hxK, hxvK⟩ : ∃ x : G, x ∈ {v} * K ∧ x ∈ K
case this.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
x : G
hxK : x ∈ {v} * K
hxvK : x ∈ K
⊢ v ∈ E / E
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
⊢ ∃ x, x ∈ ?m.265493 x * K ∧ x ∈ K

case this.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
x : G
hxK : x ∈ ?m.265493 x * K
hxvK : x ∈ K
⊢ v ∈ E / E
exact Set.not_disjoint_iff.1 (hv v hvV)
case this.intro.intro.refine'_1
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
x : G
hxK : x ∈ {v} * K
hxvK : x ∈ K
⊢ v⁻¹ * x ∈ E

case this.intro.intro.refine'_2
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
x : G
hxK : x ∈ {v} * K
hxvK : x ∈ K
⊢ (fun x x_1 => x / x_1) x (v⁻¹ * x) = v
case this.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
x : G
hxK : x ∈ {v} * K
hxvK : x ∈ K
⊢ v ∈ E / E
refine' ⟨x, v⁻¹ * x, hLE (hKL hxvK), _, _⟩
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
⊢ ↑↑μ K ≤ ↑↑μ L
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
⊢ ↑↑μ K ≠ ⊤
apply ne_top_of_le_ne_top (ne_of_lt hLtop)
no goals
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
⊢ ↑↑μ K ≤ ↑↑μ L
apply measure_mono hKL
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
⊢ False
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
⊢ ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
intro v hv hKv
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : {v} * K ∪ K ⊆ U
⊢ False
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
⊢ False
have hKvsub : {v} * K ∪ K ⊆ U := by
  apply Set.union_subset _ hUK
  apply _root_.subset_trans _ hVKU
  apply Set.mul_subset_mul _ (Set.Subset.refl K)
  simp only [Set.singleton_subset_iff, hv]
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : ↑↑μ ({v} * K ∪ K) ≤ ↑↑μ U
⊢ False
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : {v} * K ∪ K ⊆ U
⊢ False
replace hKvsub := @measure_mono _ _ μ _ _ hKvsub
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : ↑↑μ ({v} * K ∪ K) ≤ ↑↑μ U
hcontr : ↑↑μ ({v} * K ∪ K) < ↑↑μ K + ↑↑μ K
⊢ False
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : ↑↑μ ({v} * K ∪ K) ≤ ↑↑μ U
⊢ False
have hcontr := lt_of_le_of_lt hKvsub hμUK
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : ↑↑μ ({v} * K ∪ K) ≤ ↑↑μ U
hcontr : ↑↑μ ({v} * K) + ↑↑μ K < ↑↑μ K + ↑↑μ K
⊢ False
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : ↑↑μ ({v} * K ∪ K) ≤ ↑↑μ U
hcontr : ↑↑μ ({v} * K ∪ K) < ↑↑μ K + ↑↑μ K
⊢ False
rw [measure_union hKv (IsCompact.measurableSet hK)] at hcontr
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : ↑↑μ ({v} * K ∪ K) ≤ ↑↑μ U
hcontr : ↑↑μ ({v} * K) + ↑↑μ K < ↑↑μ K + ↑↑μ K
hKtranslate : ↑↑μ ({v} * K) = ↑↑μ K
⊢ False
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : ↑↑μ ({v} * K ∪ K) ≤ ↑↑μ U
hcontr : ↑↑μ ({v} * K) + ↑↑μ K < ↑↑μ K + ↑↑μ K
⊢ False
have hKtranslate : μ ({v} * K) = μ K := by
  simp only [singleton_mul, image_mul_left, measure_preimage_mul]
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : ↑↑μ ({v} * K ∪ K) ≤ ↑↑μ U
hcontr : False
hKtranslate : ↑↑μ ({v} * K) = ↑↑μ K
⊢ False
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : ↑↑μ ({v} * K ∪ K) ≤ ↑↑μ U
hcontr : ↑↑μ ({v} * K) + ↑↑μ K < ↑↑μ K + ↑↑μ K
hKtranslate : ↑↑μ ({v} * K) = ↑↑μ K
⊢ False
rw [hKtranslate, lt_self_iff_false] at hcontr
no goals
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : ↑↑μ ({v} * K ∪ K) ≤ ↑↑μ U
hcontr : False
hKtranslate : ↑↑μ ({v} * K) = ↑↑μ K
⊢ False
assumption
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
⊢ {v} * K ⊆ U
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
⊢ {v} * K ∪ K ⊆ U
apply Set.union_subset _ hUK
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
⊢ {v} * K ⊆ V * K
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
⊢ {v} * K ⊆ U
apply _root_.subset_trans _ hVKU
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
⊢ {v} ⊆ V
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
⊢ {v} * K ⊆ V * K
apply Set.mul_subset_mul _ (Set.Subset.refl K)
no goals
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
⊢ {v} ⊆ V
simp only [Set.singleton_subset_iff, hv]
no goals
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
v : G
hv : v ∈ V
hKv : Disjoint ({v} * K) K
hKvsub : ↑↑μ ({v} * K ∪ K) ≤ ↑↑μ U
hcontr : ↑↑μ ({v} * K) + ↑↑μ K < ↑↑μ K + ↑↑μ K
⊢ ↑↑μ ({v} * K) = ↑↑μ K
simp only [singleton_mul, image_mul_left, measure_preimage_mul]
case this.intro.intro.refine'_1.a
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
x : G
hxK : x ∈ {v} * K
hxvK : x ∈ K
⊢ v⁻¹ * x ∈ K
case this.intro.intro.refine'_1
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
x : G
hxK : x ∈ {v} * K
hxvK : x ∈ K
⊢ v⁻¹ * x ∈ E
apply hKL.trans hLE
no goals
case this.intro.intro.refine'_1.a
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
x : G
hxK : x ∈ {v} * K
hxvK : x ∈ K
⊢ v⁻¹ * x ∈ K
simpa only [singleton_mul, image_mul_left, mem_preimage] using hxK
no goals
case this.intro.intro.refine'_2
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEpos : 0 < ↑↑μ E
L : Set G
hL : MeasurableSet L
hLE : L ⊆ E
hLpos : 0 < ↑↑μ L
hLtop : ↑↑μ L < ⊤
K : Set G
hKL : K ⊆ L
hK : IsCompact K
hKpos : 0 < ↑↑μ K
hKtop : ↑↑μ K ≠ ⊤
U : Set G
hUK : U ⊇ K
hU : IsOpen U
hμUK : ↑↑μ U < ↑↑μ K + ↑↑μ K
V : Set G
hV1 : V ∈ 𝓝 1
hVKU : V * K ⊆ U
hv : ∀ (v : G), v ∈ V → ¬Disjoint ({v} * K) K
v : G
hvV : v ∈ V
x : G
hxK : x ∈ {v} * K
hxvK : x ∈ K
⊢ (fun x x_1 => x / x_1) x (v⁻¹ * x) = v
simp only [div_eq_iff_eq_mul, ← mul_assoc, mul_right_inv, one_mul]