case mp
𝕜 : Type ?u.524091
G : Type u_1
H : Type ?u.524097
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
⊢ Regular (Measure.inv μ) → Regular μ

case mpr
𝕜 : Type ?u.524091
G : Type u_1
H : Type ?u.524097
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
⊢ Regular μ → Regular (Measure.inv μ)
𝕜 : Type ?u.524091
G : Type u_1
H : Type ?u.524097
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
⊢ Regular (Measure.inv μ) ↔ Regular μ
constructor
case mp
𝕜 : Type ?u.524091
G : Type u_1
H : Type ?u.524097
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
h : Regular (Measure.inv μ)
⊢ Regular μ
case mp
𝕜 : Type ?u.524091
G : Type u_1
H : Type ?u.524097
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
⊢ Regular (Measure.inv μ) → Regular μ
intro h
case mp
𝕜 : Type ?u.524091
G : Type u_1
H : Type ?u.524097
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
h : Regular (Measure.inv μ)
⊢ Regular (Measure.inv (Measure.inv μ))
case mp
𝕜 : Type ?u.524091
G : Type u_1
H : Type ?u.524097
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
h : Regular (Measure.inv μ)
⊢ Regular μ
rw [← μ.inv_inv]
no goals
case mp
𝕜 : Type ?u.524091
G : Type u_1
H : Type ?u.524097
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
h : Regular (Measure.inv μ)
⊢ Regular (Measure.inv (Measure.inv μ))
exact Measure.Regular.inv
case mpr
𝕜 : Type ?u.524091
G : Type u_1
H : Type ?u.524097
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
h : Regular μ
⊢ Regular (Measure.inv μ)
case mpr
𝕜 : Type ?u.524091
G : Type u_1
H : Type ?u.524097
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
⊢ Regular μ → Regular (Measure.inv μ)
intro h
no goals
case mpr
𝕜 : Type ?u.524091
G : Type u_1
H : Type ?u.524097
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSpace H
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
h : Regular μ
⊢ Regular (Measure.inv μ)
exact Measure.Regular.inv