awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
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 α μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : G), i⁻¹ • fundamentalInterior G s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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∞)
have refine : μ.measureOf ((⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s)ᶜ = ⊥
Tactic: refine eq_bot_mono (μ.mono <| compl_subset_compl.2 this) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s)ᶜ = ⊥
have simp : μ.measureOf ((⋃ (g : G), g • fundamentalFrontier G s) ∪ {a : α | ∃ (g : G), g • a ∈ s}ᶜ) = 0
Tactic: simp only [iUnion_inv_smul, compl_sdiff, ENNReal.bot_eq_zero, himp_eq, sup_eq_union,
      @iUnion_smul_eq_setOf_exists _ _ _ _ s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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
⊢ 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∞)
have rw : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' 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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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∞)
⊢ 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∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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 μ
⊢ Eq (α := Measure (Quotient α_mod_G)) (Measure.map (Quotient.mk α_mod_G) (μ.restrict s))
    (Measure.map (Quotient.mk α_mod_G) (μ.restrict t))
have 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∞)
Tactic: ext U meas_U
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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
⊢ 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∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ t) : ℝ≥0∞)
Tactic: rw [measure_map_restrict_apply (meas_U := meas_U), measure_map_restrict_apply (meas_U := meas_U)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ t) : ℝ≥0∞)
have h : MeasurableSet (Quotient.mk α_mod_G ⁻¹' U)
Tactic: apply MeasureTheory.IsFundamentalDomain.measure_set_eq fund_dom_s fund_dom_t
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ t) : ℝ≥0∞)
have h₁ : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' Quotient.mk α_mod_G ⁻¹' U = Quotient.mk α_mod_G ⁻¹' U
Tactic: apply MeasureTheory.IsFundamentalDomain.measure_set_eq fund_dom_s fund_dom_t
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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
⊢ (fun (x : α) ↦ g • x) ⁻¹' Quotient.mk α_mod_G ⁻¹' U = Quotient.mk α_mod_G ⁻¹' U
have h : ∀ (x : α),
  Membership.mem (γ := Set α) ((fun (x : α) ↦ g • x) ⁻¹' Quotient.mk α_mod_G ⁻¹' U) x ↔ x ∈ Quotient.mk α_mod_G ⁻¹' U
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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⟧
have a : g • x ≈ x
Tactic: apply Quotient.sound
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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
⊢ g • x ≈ x
have h : (fun (m : G) ↦ m • x) g = g • x
Tactic: use g
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
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 : α
⊢ Membership.mem (γ := Set α) ((fun (x : α) ↦ g • x) ⁻¹' Quotient.mk α_mod_G ⁻¹' U) x ↔ x ∈ Quotient.mk α_mod_G ⁻¹' U
have this : ⟦g • x⟧ = ⟦x⟧
Tactic: have : Quotient.mk α_mod_G (g • x) = Quotient.mk α_mod_G x := by
      apply Quotient.sound
      use g
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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 ν
⊢ 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∞)
have simp : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Exists.choose (p := fun (s : Set α) ↦ IsFundamentalDomain G s ν) sorry) : ℝ≥0∞)
  ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp only [(fund_dom_s.hasFundamentalDomain ν), ↓reduceDIte]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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 ν
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Exists.choose (p := fun (s : Set α) ↦ IsFundamentalDomain G s ν) ⋯) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : IsFundamentalDomain G (Exists.choose (p := fun (s : Set α) ↦ IsFundamentalDomain G s ν) sorry) ν
Tactic: rw [fund_dom_s.measure_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) U : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ t) : ℝ≥0∞)
have 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∞)
Tactic: rw [fund_dom_t.projection_respects_measure (μ := μ), measure_map_restrict_apply ν t meas_U]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) U : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ t) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ t) : ℝ≥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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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 ν μ'
⊢ μ = μ'
have obtain : ∀ (𝓕 : Set α) (h𝓕 : IsFundamentalDomain G 𝓕 ν), μ = μ'
Tactic: obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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 𝓕 ν
⊢ μ = μ'
have rw : Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕) = μ'
Tactic: rw [h𝓕.projection_respects_measure (μ := μ), h𝓕.projection_respects_measure (μ := μ')]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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 𝓕) = μ'
⊢ μ = μ'
have 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 (μ := μ')]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
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 ν μ
⊢ Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕) = μ
have this : HasFundamentalDomain G α ν
Tactic: haveI : HasFundamentalDomain G α ν := ⟨𝓕, h𝓕⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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 α ν
⊢ Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕) = μ
have 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 (μ := μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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 ν
⊢ Eq (α := Measure (Quotient α_mod_G)) (Measure.map (Quotient.mk α_mod_G) (ν.restrict s))
    (Measure.map (Quotient.mk α_mod_G) (ν.restrict t))
have rw : Eq (α := Measure (Quotient α_mod_G)) (Measure.map (Quotient.mk α_mod_G) (ν.restrict t))
  (Measure.map (Quotient.mk α_mod_G) (ν.restrict t))
Tactic: rw [fund_dom_s.quotientMeasure_eq _ fund_dom_t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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∞)
⊢ QuotientMeasureEqMeasurePreimage.{u_1, u_3} (G := G) ν 0
have apply : Eq (α := Measure (Quotient α_mod_G)) 0 (Measure.map (Quotient.mk α_mod_G) (ν.restrict s))
Tactic: apply fund_dom_s.quotientMeasureEqMeasurePreimage
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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∞)
⊢ Eq (α := Measure (Quotient α_mod_G)) 0 (Measure.map (Quotient.mk α_mod_G) (ν.restrict s))
have 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∞)
Tactic: ext U meas_U
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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∞)
    (((Measure.map (Quotient.mk α_mod_G) (ν.restrict s) : Measure (Quotient α_mod_G)) :
          (a : Set (Quotient α_mod_G)) → ℝ≥0∞)
        U :
      ℝ≥0∞)
have 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∞)
Tactic: convert! (measure_inter_null_of_null_right (h := vol_s) (Quotient.mk α_mod_G ⁻¹' U)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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∞)
    (((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∞)
have h : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥0∞)
  ((ν : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' U ∩ s) : ℝ≥0∞)
Tactic: rw [measure_map_restrict_apply (meas_U := meas_U)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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 ν μ
⊢ SigmaFinite μ
have rw : Nonempty.{u_3 + 1} (μ.FiniteSpanningSetsIn univ)
Tactic: rw [sigmaFinite_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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 ν μ
⊢ Nonempty.{u_3 + 1} (μ.FiniteSpanningSetsIn univ)
have 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)
Tactic: obtain ⟨A, hA_meas, hA, hA'⟩ := Measure.toFiniteSpanningSetsIn (h := i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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
⊢ Nonempty.{u_3 + 1} (μ.FiniteSpanningSetsIn univ)
have refine_1 : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) ((fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: refine ⟨⟨fun n ↦ π '' (A n), by simp, fun n ↦ ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
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∞)
⊢ Nonempty.{u_3 + 1} (μ.FiniteSpanningSetsIn univ)
have refine_2 : Eq.{u_3 + 1} (α := Set (Quotient α_mod_G)) (⋃ (i : ℕ), (fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) i) univ
Tactic: refine ⟨⟨fun n ↦ π '' (A n), by simp, fun n ↦ ?_, ?_⟩⟩