-- Mathlib/MeasureTheory/Measure/Content.lean
theorem innerContent_pos_of_is_mul_left_invariant [Group G] [IsTopologicalGroup G]
    (h3 : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (K : Compacts G)
    (hK : μ K ≠ 0) (U : Opens G) (hU : (U : Set G).Nonempty) : 0 < μ.innerContent U

Proof state:
case intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U
⊢ μ K ≤ ↑s.card * μ.innerContent U

Tactic:
have : (K : Set G) ⊆ ↑(⨆ g ∈ s, Opens.comap (Homeomorph.mulLeft g : C(G, G)) U) := by
  simpa only [Opens.iSup_def, Opens.coe_comap, Subtype.coe_mk]

Result:
case intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this✝ : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U
this : ↑K ⊆ ↑(⨆ g ∈ s, (Opens.comap ↑(Homeomorph.mulLeft g)) U)
⊢ μ K ≤ ↑s.card * μ.innerContent U

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this✝ : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U
this : μ K ≤ ↑s.card * μ.innerContent U
⊢ 0 < μ.innerContent U

Tactic:
exact (ENNReal.mul_pos_iff.mp <| hK.bot_lt.trans_le this).2

Result:
no goals

Proof state:
case intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this✝ : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U
this : ↑K ⊆ ↑(⨆ g ∈ s, (Opens.comap ↑(Homeomorph.mulLeft g)) U)
⊢ ∑ d ∈ s, μ.innerContent ((Opens.comap ↑(Homeomorph.mulLeft d)) U) ≤ ↑s.card * μ.innerContent U

Tactic:
simp only [μ.is_mul_left_invariant_innerContent h3, Finset.sum_const, nsmul_eq_mul, le_refl]

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
⊢ 0 < μ.innerContent U

Tactic:
have : (interior (U : Set G)).Nonempty := by rwa [U.isOpen.interior_eq]

Result:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this : (interior ↑U).Nonempty
⊢ 0 < μ.innerContent U

Proof state:
case intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U
⊢ 0 < μ.innerContent U

Tactic:
suffices μ K ≤ s.card * μ.innerContent U by
  exact (ENNReal.mul_pos_iff.mp <| hK.bot_lt.trans_le this).2

Result:
case intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U
⊢ μ K ≤ ↑s.card * μ.innerContent U

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
⊢ (interior ↑U).Nonempty

Tactic:
rwa [U.isOpen.interior_eq]

Result:
no goals

Proof state:
case intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this✝ : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U
this : ↑K ⊆ ↑(⨆ g ∈ s, (Opens.comap ↑(Homeomorph.mulLeft g)) U)
⊢ μ K ≤ ↑s.card * μ.innerContent U

Tactic:
refine (μ.le_innerContent _ _ this).trans ?_

Result:
case intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this✝ : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U
this : ↑K ⊆ ↑(⨆ g ∈ s, (Opens.comap ↑(Homeomorph.mulLeft g)) U)
⊢ μ.innerContent (⨆ g ∈ s, (Opens.comap ↑(Homeomorph.mulLeft g)) U) ≤ ↑s.card * μ.innerContent U

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this : (interior ↑U).Nonempty
⊢ 0 < μ.innerContent U

Tactic:
rcases compact_covered_by_mul_left_translates K.2 this with ⟨s, hs⟩

Result:
case intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U
⊢ 0 < μ.innerContent U

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x => g * x) ⁻¹' ↑U
⊢ ↑K ⊆ ↑(⨆ g ∈ s, (Opens.comap ↑(Homeomorph.mulLeft g)) U)

Tactic:
simpa only [Opens.iSup_def, Opens.coe_comap, Subtype.coe_mk]

Result:
no goals