𝕜 : Type ?u.525633
G : Type u_1
H : Type ?u.525639
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
h : ↑↑μ K ≠ 0
U : Set G
hU : IsOpen U
hne : Set.Nonempty U
⊢ ↑↑μ U ≠ 0
𝕜 : Type ?u.525633
G : Type u_1
H : Type ?u.525639
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
h : ↑↑μ K ≠ 0
⊢ IsOpenPosMeasure μ
refine' ⟨fun U hU hne => _⟩
𝕜 : Type ?u.525633
G : Type u_1
H : Type ?u.525639
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen U
hne : Set.Nonempty U
h : ↑↑μ U = 0
⊢ ↑↑μ K = 0
𝕜 : Type ?u.525633
G : Type u_1
H : Type ?u.525639
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
h : ↑↑μ K ≠ 0
U : Set G
hU : IsOpen U
hne : Set.Nonempty U
⊢ ↑↑μ U ≠ 0
contrapose! h
𝕜 : Type ?u.525633
G : Type u_1
H : Type ?u.525639
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen U
hne : Set.Nonempty U
h : ↑↑μ U = 0
⊢ ↑↑μ K ≤ 0
𝕜 : Type ?u.525633
G : Type u_1
H : Type ?u.525639
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen U
hne : Set.Nonempty U
h : ↑↑μ U = 0
⊢ ↑↑μ K = 0
rw [← nonpos_iff_eq_zero]
𝕜 : Type ?u.525633
G : Type u_1
H : Type ?u.525639
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen U
hne : Set.Nonempty (interior U)
h : ↑↑μ U = 0
⊢ ↑↑μ K ≤ 0
𝕜 : Type ?u.525633
G : Type u_1
H : Type ?u.525639
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen U
hne : Set.Nonempty U
h : ↑↑μ U = 0
⊢ ↑↑μ K ≤ 0
rw [← hU.interior_eq] at hne
case intro
𝕜 : Type ?u.525633
G : Type u_1
H : Type ?u.525639
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen U
hne : Set.Nonempty (interior U)
h : ↑↑μ U = 0
t : Finset G
hKt : K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' U
⊢ ↑↑μ K ≤ 0
𝕜 : Type ?u.525633
G : Type u_1
H : Type ?u.525639
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen U
hne : Set.Nonempty (interior U)
h : ↑↑μ U = 0
⊢ ↑↑μ K ≤ 0
obtain ⟨t, hKt⟩ : ∃ t : Finset G, K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U :=
  compact_covered_by_mul_left_translates hK hne
no goals
case intro
𝕜 : Type ?u.525633
G : Type u_1
H : Type ?u.525639
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen U
hne : Set.Nonempty (interior U)
h : ↑↑μ U = 0
t : Finset G
hKt : K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' U
⊢ ↑↑μ K ≤ 0
calc
  μ K ≤ μ (⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U) := measure_mono hKt
  _ ≤ ∑ g in t, μ ((fun h : G => g * h) ⁻¹' U) := (measure_biUnion_finset_le _ _)
  _ = 0 := by simp [measure_preimage_mul, h]
no goals
𝕜 : Type ?u.525633
G : Type u_1
H : Type ?u.525639
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen U
hne : Set.Nonempty (interior U)
h : ↑↑μ U = 0
t : Finset G
hKt : K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' U
⊢ ∑ g in t, ↑↑μ ((fun h => g * h) ⁻¹' U) = 0
simp [measure_preimage_mul, h]