awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ν
vol_s : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
apply : Eq (α := Measure (Quotient α_mod_G)) 0 (Measure.map (Quotient.mk α_mod_G) (ν.restrict s))
⊢ QuotientMeasureEqMeasurePreimage.{u_1, u_3} (G := G) ν 0

Tactic:
apply fund_dom_s.quotientMeasureEqMeasurePreimage

Premises used: MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage
-- 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 ν
vol_s : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  ∀ (U : Set (Quotient α_mod_G)) (meas_U : MeasurableSet U),
    Eq (α := ℝ≥0∞) (((0 : Measure (Quotient α_mod_G)) : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) U : ℝ≥0∞)
      (((Measure.map (Quotient.mk α_mod_G) (ν.restrict s) : Measure (Quotient α_mod_G)) :
            (a : Set (Quotient α_mod_G)) → ℝ≥0∞)
          U :
        ℝ≥0∞)
⊢ Eq (α := Measure (Quotient α_mod_G)) 0 (Measure.map (Quotient.mk α_mod_G) (ν.restrict s))

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 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
vol_s : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥0∞)

Tactic:
(measure_inter_null_of_null_right (h := vol_s) (Quotient.mk α_mod_G ⁻¹' U)).symm

Premises used: MulAction.orbitRel, Quotient.mk, MeasureTheory.measure_inter_null_of_null_right, Set.preimage, Eq.symm
-- 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 ν
vol_s : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
h :
  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∞)
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
    (((Measure.map (Quotient.mk α_mod_G) (ν.restrict s) : Measure (Quotient α_mod_G)) :
          (a : Set (Quotient α_mod_G)) → ℝ≥0∞)
        U :
      ℝ≥0∞)

Tactic:
convert! (measure_inter_null_of_null_right (h := vol_s) (Quotient.mk α_mod_G ⁻¹' U)).symm
-- 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 ν
vol_s : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
h h₁ :
  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 [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 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
rw : Nonempty.{u_3 + 1} (μ.FiniteSpanningSetsIn univ)
⊢ SigmaFinite μ

Tactic:
rw [sigmaFinite_iff]

Premises used: MeasureTheory.sigmaFinite_iff
-- 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 α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
obtain :
  ∀ (A : ℕ → Set α) (hA_meas : ∀ (i : ℕ), Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} (A i))
    (hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ), Nonempty.{u_3 + 1} (μ.FiniteSpanningSetsIn univ)
⊢ Nonempty.{u_3 + 1} (μ.FiniteSpanningSetsIn univ)

Tactic:
obtain ⟨A, hA_meas, hA, hA'⟩ := Measure.toFiniteSpanningSetsIn (h := i)

Premises used: MeasureTheory.Measure.toFiniteSpanningSetsIn
-- 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 α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
⊢ ∀ (i : ℕ), Membership.mem (γ := Set (Set (Quotient α_mod_G))) univ ((fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) i)

Tactic:
simp
-- 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 α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
refine_1 :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) ((fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) n) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
refine_2 : Eq.{u_3 + 1} (α := Set (Quotient α_mod_G)) (⋃ (i : ℕ), (fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) i) univ
⊢ Nonempty.{u_3 + 1} (μ.FiniteSpanningSetsIn univ)

Tactic:
refine ⟨⟨fun n ↦ π '' (A n), by simp, fun n ↦ ?_, ?_⟩⟩
-- 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 α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
refine_1 :
  ∀ (s : Set α) (fund_dom_s : IsFundamentalDomain G s ν),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) ((fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) n) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) ((fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
obtain ⟨s, fund_dom_s⟩ := i'
-- 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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n

Tactic:
have : π ⁻¹' π '' (A n) = _ := MulAction.quotient_preimage_image_eq_union_mul (A n) (G := 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 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
x : Setoid α := α_mod_G
rw : MeasurableSet.{u_3} (α := α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' A n)
⊢ MeasurableSet (Quotient.mk α_mod_G '' A n)

Tactic:
rw [measurableSet_quotient, Quotient.mk''_eq_mk, this]

Premises used: measurableSet_quotient, Quotient.mk''_eq_mk
-- 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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
x : Setoid α := α_mod_G
h : ∀ (b : G), MeasurableSet (α := α) ((fun (x : α) ↦ b • x) '' A n)
⊢ MeasurableSet.{u_3} (α := α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' A n)

Tactic:
apply MeasurableSet.iUnion

Premises used: MeasurableSet.iUnion
-- 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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
x : Setoid α := α_mod_G
⊢ ∀ (b : G), MeasurableSet (α := α) ((fun (x : α) ↦ b • x) '' A n)

Tactic:
fun g ↦ MeasurableSet.const_smul (hA_meas n) g

Premises used: MeasurableSet.const_smul
-- 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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
x : Setoid α := α_mod_G
⊢ ∀ (b : G), MeasurableSet (α := α) ((fun (x : α) ↦ b • x) '' A n)

Tactic:
exact fun g ↦ MeasurableSet.const_smul (hA_meas n) g

Premises used: MeasurableSet.const_smul
-- 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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
⊢ MeasurableSet (Quotient.mk α_mod_G '' A n)

Tactic:
have measπAn : MeasurableSet (π '' A n) := by
      let _ : Setoid α := α_mod_G
      rw [measurableSet_quotient, Quotient.mk''_eq_mk, this]
      apply MeasurableSet.iUnion
      exact fun g ↦ MeasurableSet.const_smul (hA_meas n) 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 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
refine_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) ((fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [fund_dom_s.projection_respects_measure_apply (μ := μ) measπAn, this, iUnion_inter]

Premises used: Set.iUnion_inter, MeasureTheory.IsFundamentalDomain.projection_respects_measure_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 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
lt_of_le_of_lt ?_ (hA n)

Premises used: lt_of_le_of_lt
-- 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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
refine_1 :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (A n) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine lt_of_le_of_lt ?_ (hA n)

Premises used: lt_of_le_of_lt
-- 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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
refine_1 :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞)
    (∑' (g : G), (ν : (a : Set α) → ℝ≥0∞) (g • A n ∩ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (A n) : ℝ≥0∞)

Tactic:
rw [fund_dom_s.measure_eq_tsum (A n)]

Premises used: MeasureTheory.IsFundamentalDomain.measure_eq_tsum
-- 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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞)
    (∑' (g : G), (ν : (a : Set α) → ℝ≥0∞) (g • A n ∩ s) : ℝ≥0∞)

Tactic:
measure_iUnion_le _

Premises used: MeasureTheory.measure_iUnion_le
-- 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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞)
    (∑' (g : G), (ν : (a : Set α) → ℝ≥0∞) (g • A n ∩ s) : ℝ≥0∞)

Tactic:
exact measure_iUnion_le _

Premises used: MeasureTheory.measure_iUnion_le
-- 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 α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
refine_2 : Quotient.mk α_mod_G '' univ = univ
⊢ Eq.{u_3 + 1} (α := Set (Quotient α_mod_G)) (⋃ (i : ℕ), (fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) i) univ

Tactic:
rw [← image_iUnion, hA']

Premises used: Set.image_iUnion
-- 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 α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
⊢ Surjective.{u_3 + 1, u_3 + 1} (α := α) (β := Quotient α_mod_G) Quotient.mk'

Tactic:
Quotient.mk'_surjective

Premises used: Quotient.mk'_surjective
-- 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 α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
⊢ Surjective (Quotient.mk α_mod_G)

Tactic:
convert! Quotient.mk'_surjective

Premises used: Quotient.mk'_surjective
-- 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 α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
⊢ Quotient.mk α_mod_G '' univ = univ

Tactic:
refine image_univ_of_surjective (by convert! Quotient.mk'_surjective)

Premises used: Set.image_univ_of_surjective
-- 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)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
obtain : ∀ (𝓕 : Set α) (h𝓕 : IsFundamentalDomain G 𝓕 ν), IsFiniteMeasure μ
⊢ IsFiniteMeasure μ

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 α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
rw : IsFiniteMeasure (m0 := Quotient.instMeasurableSpace) (Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕))
⊢ IsFiniteMeasure μ

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

Premises used: MeasureTheory.IsFundamentalDomain.projection_respects_measure