case pos
𝕜 : Type ?u.531158
G : Type u_1
H : Type ?u.531164
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
s : Set G
hs : IsOpen s
h3μ : μ = 0
⊢ ↑↑μ s = 0 ↔ s = ∅ ∨ μ = 0

case neg
𝕜 : Type ?u.531158
G : Type u_1
H : Type ?u.531164
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
s : Set G
hs : IsOpen s
h3μ : ¬μ = 0
⊢ ↑↑μ s = 0 ↔ s = ∅ ∨ μ = 0
𝕜 : Type ?u.531158
G : Type u_1
H : Type ?u.531164
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
s : Set G
hs : IsOpen s
⊢ ↑↑μ s = 0 ↔ s = ∅ ∨ μ = 0
by_cases h3μ : μ = 0
no goals
case pos
𝕜 : Type ?u.531158
G : Type u_1
H : Type ?u.531164
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
s : Set G
hs : IsOpen s
h3μ : μ = 0
⊢ ↑↑μ s = 0 ↔ s = ∅ ∨ μ = 0
simp [h3μ]
case neg
𝕜 : Type ?u.531158
G : Type u_1
H : Type ?u.531164
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
s : Set G
hs : IsOpen s
h3μ : ¬μ = 0
this : IsOpenPosMeasure μ
⊢ ↑↑μ s = 0 ↔ s = ∅ ∨ μ = 0
case neg
𝕜 : Type ?u.531158
G : Type u_1
H : Type ?u.531164
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
s : Set G
hs : IsOpen s
h3μ : ¬μ = 0
⊢ ↑↑μ s = 0 ↔ s = ∅ ∨ μ = 0
haveI := isOpenPosMeasure_of_mulLeftInvariant_of_regular h3μ
no goals
case neg
𝕜 : Type ?u.531158
G : Type u_1
H : Type ?u.531164
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
s : Set G
hs : IsOpen s
h3μ : ¬μ = 0
this : IsOpenPosMeasure μ
⊢ ↑↑μ s = 0 ↔ s = ∅ ∨ μ = 0
simp only [h3μ, or_false_iff, hs.measure_eq_zero_iff μ]