𝕜 : Type ?u.535820
G : Type u_1
H : Type ?u.535826
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
U : Set G
hU : IsOpen U
h'U : Set.Nonempty (interior U)
h : ↑↑μ U ≠ ⊤
K : Set G
hK : IsCompact K
⊢ ↑↑μ K < ⊤
𝕜 : Type ?u.535820
G : Type u_1
H : Type ?u.535826
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
U : Set G
hU : IsOpen U
h'U : Set.Nonempty U
h : ↑↑μ U ≠ ⊤
K : Set G
hK : IsCompact K
⊢ ↑↑μ K < ⊤
rw [← hU.interior_eq] at h'U
case intro
𝕜 : Type ?u.535820
G : Type u_1
H : Type ?u.535826
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
U : Set G
hU : IsOpen U
h'U : Set.Nonempty (interior U)
h : ↑↑μ U ≠ ⊤
K : Set G
hK : IsCompact K
t : Finset G
hKt : K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' U
⊢ ↑↑μ K < ⊤
𝕜 : Type ?u.535820
G : Type u_1
H : Type ?u.535826
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
U : Set G
hU : IsOpen U
h'U : Set.Nonempty (interior U)
h : ↑↑μ U ≠ ⊤
K : Set G
hK : IsCompact K
⊢ ↑↑μ K < ⊤
obtain ⟨t, hKt⟩ : ∃ t : Finset G, K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U :=
  compact_covered_by_mul_left_translates hK h'U
no goals
case intro
𝕜 : Type ?u.535820
G : Type u_1
H : Type ?u.535826
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
U : Set G
hU : IsOpen U
h'U : Set.Nonempty (interior U)
h : ↑↑μ U ≠ ⊤
K : Set G
hK : IsCompact K
t : Finset G
hKt : K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' U
⊢ ↑↑μ K < ⊤
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 _ _)
  _ = Finset.card t * μ U := by simp only [measure_preimage_mul, Finset.sum_const, nsmul_eq_mul]
  _ < ∞ := ENNReal.mul_lt_top (ENNReal.nat_ne_top _) h
no goals
𝕜 : Type ?u.535820
G : Type u_1
H : Type ?u.535826
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : IsMulLeftInvariant μ
U : Set G
hU : IsOpen U
h'U : Set.Nonempty (interior U)
h : ↑↑μ U ≠ ⊤
K : Set G
hK : IsCompact K
t : Finset G
hKt : K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' U
⊢ ∑ g in t, ↑↑μ ((fun h => g * h) ⁻¹' U) = ↑(Finset.card t) * ↑↑μ U
simp only [measure_preimage_mul, Finset.sum_const, nsmul_eq_mul]