-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem fundamentalInterior : IsFundamentalDomain G (fundamentalInterior G s) μ where
  nullMeasurableSet := hs.nullMeasurableSet.fundamentalInterior _ _
  ae_covers

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ fundamentalInterior G s

Tactic:
simp_rw [ae_iff, not_exists, ← mem_inv_smul_set_iff, setOf_forall, ← compl_setOf,
  setOf_mem_eq, ← compl_iUnion]

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ μ (⋃ i, i⁻¹ • fundamentalInterior G s)ᶜ = 0

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
this : (⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s ⊆ ⋃ g, g⁻¹ • fundamentalInterior G s
⊢ μ.measureOf ((⋃ g, g • fundamentalFrontier G s) ∪ {a | ∃ g, g • a ∈ s}ᶜ) = 0

Tactic:
exact measure_union_null
  (measure_iUnion_null fun _ => measure_smul_null hs.measure_fundamentalFrontier _) hs.ae_covers

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ ⋃ i, i⁻¹ • s ⊆ ⋃ i, i⁻¹ • s

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
this : (⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s ⊆ ⋃ g, g⁻¹ • fundamentalInterior G s
⊢ μ.measureOf ((⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s)ᶜ = ⊥

Tactic:
simp only [iUnion_inv_smul, compl_sdiff, ENNReal.bot_eq_zero, himp_eq, sup_eq_union,
  @iUnion_smul_eq_setOf_exists _ _ _ _ s]

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
this : (⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s ⊆ ⋃ g, g⁻¹ • fundamentalInterior G s
⊢ μ.measureOf ((⋃ g, g • fundamentalFrontier G s) ∪ {a | ∃ g, g • a ∈ s}ᶜ) = 0

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ (⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s ⊆ ⋃ g, g⁻¹ • fundamentalInterior G s

Tactic:
simp_rw [diff_subset_iff, ← iUnion_union_distrib, ← smul_set_union (α := G) (β := α),
  fundamentalFrontier_union_fundamentalInterior]

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ ⋃ i, i⁻¹ • s ⊆ ⋃ i, i⁻¹ • s

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ μ (⋃ i, i⁻¹ • fundamentalInterior G s)ᶜ = 0

Tactic:
have :
  ((⋃ g : G, g⁻¹ • s) \ ⋃ g : G, g⁻¹ • fundamentalFrontier G s) ⊆
    ⋃ g : G, g⁻¹ • fundamentalInterior G s := by
  simp_rw [diff_subset_iff, ← iUnion_union_distrib, ← smul_set_union (α := G) (β := α),
    fundamentalFrontier_union_fundamentalInterior]; rfl

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
this : (⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s ⊆ ⋃ g, g⁻¹ • fundamentalInterior G s
⊢ μ (⋃ i, i⁻¹ • fundamentalInterior G s)ᶜ = 0

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
this : (⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s ⊆ ⋃ g, g⁻¹ • fundamentalInterior G s
⊢ μ (⋃ i, i⁻¹ • fundamentalInterior G s)ᶜ = 0

Tactic:
refine eq_bot_mono (μ.mono <| compl_subset_compl.2 this) ?_

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
this : (⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s ⊆ ⋃ g, g⁻¹ • fundamentalInterior G s
⊢ μ.measureOf ((⋃ g, g⁻¹ • s) \ ⋃ g, g⁻¹ • fundamentalFrontier G s)ᶜ = ⊥