awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (fundamentalFrontier G s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa only [fundamentalFrontier, iUnion₂_inter, one_smul, measure_iUnion_null_iff, inter_comm s,
    Function.onFun] using fun g (hg : g ≠ 1) => hs.aedisjoint hg

Premises used: Function.onFun, MeasureTheory.measure_iUnion_null_iff, MeasureTheory.fundamentalFrontier, Set.iUnion₂_inter, one_smul, Set.inter_comm, MeasureTheory.IsFundamentalDomain.aedisjoint
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (fundamentalInterior G s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_diff_null' hs.measure_fundamentalFrontier

Premises used: MeasureTheory.measure_diff_null', MeasureTheory.fundamentalInterior, MeasureTheory.IsFundamentalDomain.measure_fundamentalFrontier
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
simp_rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : G), i⁻¹ • fundamentalInterior G s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, ∃ (g : 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]

Premises used: not_exists, Set.compl_iUnion, Set.setOf_mem_eq, Set.mem_inv_smul_set_iff, MeasureTheory.ae_iff, Set.setOf_forall, Set.compl_setOf
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
simp_rw : Subset.{u_3} (α := Set α) (⋃ (g : G), g⁻¹ • s) (⋃ (g : G), g⁻¹ • s)
⊢ Subset.{u_3} (α := Set α) ((⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s)
    (⋃ (g : G), g⁻¹ • fundamentalInterior G s)

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

Premises used: Set.diff_subset_iff, Set.iUnion_union_distrib, Set.smul_set_union, MeasureTheory.fundamentalFrontier_union_fundamentalInterior
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
⊢ Subset.{u_3} (α := Set α) (⋃ (g : G), g⁻¹ • s) (⋃ (g : G), g⁻¹ • s)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
⊢ Subset.{u_3} (α := Set α) ((⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s)
    (⋃ (g : G), g⁻¹ • fundamentalInterior G s)

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
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
this :
  Subset.{u_3} (α := Set α) ((⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s)
    (⋃ (g : G), g⁻¹ • fundamentalInterior G s)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : G), i⁻¹ • fundamentalInterior G s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

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

Premises used: Iff.mpr, MeasureTheory.OuterMeasure.mono, Set.compl_subset_compl, MeasureTheory.Measure.toOuterMeasure, eq_bot_mono
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
this :
  Subset.{u_3} (α := Set α) ((⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s)
    (⋃ (g : G), g⁻¹ • fundamentalInterior G s)
refine : μ.measureOf ((⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s)ᶜ = ⊥
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : G), i⁻¹ • fundamentalInterior G s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

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

Premises used: Iff.mpr, MeasureTheory.OuterMeasure.mono, Set.compl_subset_compl, MeasureTheory.Measure.toOuterMeasure, eq_bot_mono
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
this :
  Subset.{u_3} (α := Set α) ((⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s)
    (⋃ (g : G), g⁻¹ • fundamentalInterior G s)
simp : μ.measureOf ((⋃ (g : G), g • fundamentalFrontier G s) ∪ {a : α | ∃ (g : G), g • a ∈ s}ᶜ) = 0
⊢ μ.measureOf ((⋃ (g : G), g⁻¹ • s) \ ⋃ (g : 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]

Premises used: compl_sdiff, himp_eq, ENNReal.bot_eq_zero, Set.sup_eq_union, Set.iUnion_inv_smul, Set.iUnion_smul_eq_setOf_exists
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
this :
  Subset.{u_3} (α := Set α) ((⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s)
    (⋃ (g : G), g⁻¹ • fundamentalInterior G s)
⊢ μ.measureOf ((⋃ (g : G), g • fundamentalFrontier G s) ∪ {a : α | ∃ (g : G), g • a ∈ s}ᶜ) = 0

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

Premises used: MeasureTheory.measure_iUnion_null, MeasureTheory.measure_union_null, MeasureTheory.measure_smul_null, MeasureTheory.IsFundamentalDomain.measure_fundamentalFrontier, MeasureTheory.IsFundamentalDomain.ae_covers
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
this :
  Subset.{u_3} (α := Set α) ((⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s)
    (⋃ (g : G), g⁻¹ • fundamentalInterior G s)
⊢ μ.measureOf ((⋃ (g : G), g • fundamentalFrontier G s) ∪ {a : α | ∃ (g : G), g • a ∈ s}ᶜ) = 0

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

Premises used: MeasureTheory.measure_iUnion_null, MeasureTheory.measure_union_null, MeasureTheory.measure_smul_null, MeasureTheory.IsFundamentalDomain.measure_fundamentalFrontier, MeasureTheory.IsFundamentalDomain.ae_covers
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
μ : Measure α
s : Set α
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
rw :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (Quotient.mk α_mod_G) (μ.restrict s) : Measure (Quotient α_mod_G)) :
          (a : Set (Quotient α_mod_G)) → ℝ≥0∞)
        U :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥0∞)

Tactic:
rw [map_apply (f := π) (fun V hV ↦ measurableSet_quotient.mp hV) meas_U,
    Measure.restrict_apply (t := (Quotient.mk α_mod_G ⁻¹' U)) (measurableSet_quotient.mp meas_U)]
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
μ : Measure α
inst_3 : Countable G
s t : Set α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : MeasurableConstSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
h :
  ∀ (U : Set (Quotient α_mod_G)) (meas_U : MeasurableSet U),
    Eq (α := ℝ≥0∞)
      (((Measure.map (Quotient.mk α_mod_G) (μ.restrict s) : Measure (Quotient α_mod_G)) :
            (a : Set (Quotient α_mod_G)) → ℝ≥0∞)
          U :
        ℝ≥0∞)
      (((Measure.map (Quotient.mk α_mod_G) (μ.restrict t) : Measure (Quotient α_mod_G)) :
            (a : Set (Quotient α_mod_G)) → ℝ≥0∞)
          U :
        ℝ≥0∞)
⊢ Eq (α := Measure (Quotient α_mod_G)) (Measure.map (Quotient.mk α_mod_G) (μ.restrict s))
    (Measure.map (Quotient.mk α_mod_G) (μ.restrict t))

Tactic:
ext U meas_U
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
μ : Measure α
inst_3 : Countable G
s t : Set α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : MeasurableConstSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (Quotient.mk α_mod_G) (μ.restrict s) : Measure (Quotient α_mod_G)) :
          (a : Set (Quotient α_mod_G)) → ℝ≥0∞)
        U :
      ℝ≥0∞)
    (((Measure.map (Quotient.mk α_mod_G) (μ.restrict t) : Measure (Quotient α_mod_G)) :
          (a : Set (Quotient α_mod_G)) → ℝ≥0∞)
        U :
      ℝ≥0∞)

Tactic:
rw [measure_map_restrict_apply (meas_U := meas_U), measure_map_restrict_apply (meas_U := meas_U)]

Premises used: MeasureTheory.measure_map_restrict_apply
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
μ : Measure α
inst_3 : Countable G
s t : Set α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : MeasurableConstSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
h : MeasurableSet (Quotient.mk α_mod_G ⁻¹' U)
h₁ : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' Quotient.mk α_mod_G ⁻¹' U = Quotient.mk α_mod_G ⁻¹' U
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ t) : ℝ≥0∞)

Tactic:
apply MeasureTheory.IsFundamentalDomain.measure_set_eq fund_dom_s fund_dom_t

Premises used: MeasureTheory.IsFundamentalDomain.measure_set_eq
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
μ : Measure α
inst_3 : Countable G
s t : Set α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : MeasurableConstSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ MeasurableSet (Quotient.mk α_mod_G ⁻¹' U)

Tactic:
measurableSet_quotient.mp meas_U

Premises used: Iff.mp, measurableSet_quotient
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
μ : Measure α
inst_3 : Countable G
s t : Set α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : MeasurableConstSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ MeasurableSet (Quotient.mk α_mod_G ⁻¹' U)

Tactic:
exact measurableSet_quotient.mp meas_U

Premises used: Iff.mp, measurableSet_quotient
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
μ : Measure α
inst_3 : Countable G
s t : Set α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : MeasurableConstSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
g : G
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (x : α) ↦ g • x) ⁻¹' Quotient.mk α_mod_G ⁻¹' U) x ↔ x ∈ Quotient.mk α_mod_G ⁻¹' U
⊢ (fun (x : α) ↦ g • x) ⁻¹' Quotient.mk α_mod_G ⁻¹' U = Quotient.mk α_mod_G ⁻¹' U

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
μ : Measure α
inst_3 : Countable G
s t : Set α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : MeasurableConstSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
g : G
x : α
a : g • x ≈ x
⊢ ⟦g • x⟧ = ⟦x⟧

Tactic:
apply Quotient.sound

Premises used: Quotient.sound
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
μ : Measure α
inst_3 : Countable G
s t : Set α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : MeasurableConstSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
g : G
x : α
w : G
h : (fun (m : G) ↦ m • x) g = g • x
⊢ g • x ≈ x

Tactic:
use g
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
μ : Measure α
inst_3 : Countable G
s t : Set α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : MeasurableConstSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
g : G
x : α
⊢ ⟦g • x⟧ = ⟦x⟧

Tactic:
have : Quotient.mk α_mod_G (g • x) = Quotient.mk α_mod_G x := by
      apply Quotient.sound
      use g
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
μ : Measure α
inst_3 : Countable G
s t : Set α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : MeasurableConstSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
g : G
x : α
this : ⟦g • x⟧ = ⟦x⟧
⊢ Membership.mem (γ := Set α) ((fun (x : α) ↦ g • x) ⁻¹' Quotient.mk α_mod_G ⁻¹' U) x ↔ x ∈ Quotient.mk α_mod_G ⁻¹' U

Tactic:
simp only [mem_preimage, this]

Premises used: Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ HasFundamentalDomain G α ν

Tactic:
⟨⟨s, fund_dom_s⟩⟩

Premises used: MeasureTheory.HasFundamentalDomain.mk, Exists.intro
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : Countable G
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
simp :
  Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Exists.choose (p := fun (s : Set α) ↦ IsFundamentalDomain G s ν) ⋯) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (if funDom : HasFundamentalDomain G α ν then
        (ν : (a : Set α) → ℝ≥0∞) (Exists.choose (p := fun (s : Set α) ↦ IsFundamentalDomain G s ν) ⋯)
      else 0 :
      ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [(fund_dom_s.hasFundamentalDomain ν), ↓reduceDIte]

Premises used: reduceDIte, MeasureTheory.IsFundamentalDomain.hasFundamentalDomain
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : Countable G
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
rw : IsFundamentalDomain G (Exists.choose (p := fun (s : Set α) ↦ IsFundamentalDomain G s ν) ⋯) ν
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Exists.choose (p := fun (s : Set α) ↦ IsFundamentalDomain G s ν) ⋯) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [fund_dom_s.measure_eq]

Premises used: MeasureTheory.IsFundamentalDomain.measure_eq
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : Countable G
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ IsFundamentalDomain G (Exists.choose (p := fun (s : Set α) ↦ IsFundamentalDomain G s ν) ⋯) ν

Tactic:
(fund_dom_s.hasFundamentalDomain ν).ExistsIsFundamentalDomain.choose_spec

Premises used: Exists.choose_spec, MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : Countable G
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α ν
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ IsFundamentalDomain G (Exists.choose (p := fun (s : Set α) ↦ IsFundamentalDomain G s ν) ⋯) ν

Tactic:
exact (fund_dom_s.hasFundamentalDomain ν).ExistsIsFundamentalDomain.choose_spec

Premises used: Exists.choose_spec, MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
μ : Measure (Quotient α_mod_G)
i : QuotientMeasureEqMeasurePreimage ν μ
t : Set α
fund_dom_t : IsFundamentalDomain G t ν
⊢ μ = Measure.map (Quotient.mk α_mod_G) (ν.restrict t)

Tactic:
i.projection_respects_measure' t fund_dom_t

Premises used: MeasureTheory.QuotientMeasureEqMeasurePreimage.projection_respects_measure'
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
μ : Measure (Quotient α_mod_G)
i : QuotientMeasureEqMeasurePreimage ν μ
t : Set α
fund_dom_t : IsFundamentalDomain G t ν
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
rw :
  Eq (α := ℝ≥0∞)
    (((Measure.map (Quotient.mk α_mod_G) (ν.restrict t) : Measure (Quotient α_mod_G)) :
          (a : Set (Quotient α_mod_G)) → ℝ≥0∞)
        U :
      ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ t) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ t) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) U : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ t) : ℝ≥0∞)

Tactic:
rw [fund_dom_t.projection_respects_measure (μ := μ), measure_map_restrict_apply ν t meas_U]

Premises used: MeasureTheory.measure_map_restrict_apply, MeasureTheory.IsFundamentalDomain.projection_respects_measure
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
hasFun : HasFundamentalDomain G α ν
μ μ' : Measure (Quotient α_mod_G)
inst_3 : QuotientMeasureEqMeasurePreimage ν μ
inst_4 : QuotientMeasureEqMeasurePreimage ν μ'
obtain : ∀ (𝓕 : Set α) (h𝓕 : IsFundamentalDomain G 𝓕 ν), μ = μ'
⊢ μ = μ'

Tactic:
obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain

Premises used: MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
hasFun : HasFundamentalDomain G α ν
μ μ' : Measure (Quotient α_mod_G)
inst_3 : QuotientMeasureEqMeasurePreimage ν μ
inst_4 : QuotientMeasureEqMeasurePreimage ν μ'
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
rw : Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕) = μ'
rw₁ rw₂ :
  Eq (α := Measure (Quotient α_mod_G)) (Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕))
    (Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕))
⊢ μ = μ'

Tactic:
rw [h𝓕.projection_respects_measure (μ := μ), h𝓕.projection_respects_measure (μ := μ')]

Premises used: MeasureTheory.IsFundamentalDomain.projection_respects_measure
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
μ : Measure (Quotient α_mod_G)
inst_3 : QuotientMeasureEqMeasurePreimage ν μ
⊢ HasFundamentalDomain G α ν

Tactic:
haveI : HasFundamentalDomain G α ν := ⟨𝓕, h𝓕⟩
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
μ : Measure (Quotient α_mod_G)
inst_3 : QuotientMeasureEqMeasurePreimage ν μ
this : HasFundamentalDomain G α ν
rw rw₁ :
  Eq (α := Measure (Quotient α_mod_G)) (Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕))
    (Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕))
⊢ Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕) = μ

Tactic:
rw [h𝓕.projection_respects_measure (μ := μ)]

Premises used: MeasureTheory.IsFundamentalDomain.projection_respects_measure
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
t : Set α
fund_dom_t : IsFundamentalDomain G t ν
rw rw₁ :
  Eq (α := Measure (Quotient α_mod_G)) (Measure.map (Quotient.mk α_mod_G) (ν.restrict t))
    (Measure.map (Quotient.mk α_mod_G) (ν.restrict t))
⊢ Eq (α := Measure (Quotient α_mod_G)) (Measure.map (Quotient.mk α_mod_G) (ν.restrict s))
    (Measure.map (Quotient.mk α_mod_G) (ν.restrict t))

Tactic:
rw [fund_dom_s.quotientMeasure_eq _ fund_dom_t]

Premises used: MeasureTheory.IsFundamentalDomain.quotientMeasure_eq
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
h : μ = Measure.map (Quotient.mk α_mod_G) (ν.restrict s)
⊢ QuotientMeasureEqMeasurePreimage ν μ

Tactic:
simpa [h] using fund_dom_s.quotientMeasureEqMeasurePreimage_quotientMeasure

Premises used: MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure