case h.e'_4
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Set G
h1U : IsOpen U
h2U : Set.Nonempty U
⊢ ↑(Content.outerMeasure μ) U = innerContent μ { carrier := U, is_open' := h1U }
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Set G
h1U : IsOpen U
h2U : Set.Nonempty U
⊢ 0 < ↑(Content.outerMeasure μ) U
convert μ.innerContent_pos_of_is_mul_left_invariant h3 K hK ⟨U, h1U⟩ h2U
no goals
case h.e'_4
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h3 :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
K : Compacts G
hK : (fun s => ↑(toFun μ s)) K ≠ 0
U : Set G
h1U : IsOpen U
h2U : Set.Nonempty U
⊢ ↑(Content.outerMeasure μ) U = innerContent μ { carrier := U, is_open' := h1U }
exact μ.outerMeasure_opens ⟨U, h1U⟩