awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
inst_4 : MulAction H β
inst_5 : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm : (a : β) → α) ν μ
e : H ≃ G
hef :
  ∀ (g : H),
    Semiconj (⇑f : (a : α) → β) (fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) g : G) x)
      fun (x : β) ↦ g • x
g : G
x : α
⊢ Eq.{u_3 + 1} (α := α)
    ((f.symm : (a : β) → α)
        ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_4, u_4} (α := H) ((e.symm : (a : G) → H) g : H) x) ((f : (a : α) → β) x)) :
      α)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)) : α)
have rw : Eq.{u_3 + 1} (α := α)
  ((f.symm : (a : β) → α)
      ((f : (a : α) → β)
          ((fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) ((e.symm : (a : G) → H) g : H) : G) x)
            x) :
        β) :
    α)
  ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)) : α)
Tactic: rw [← hef _ _, f.symm_apply_apply, f.symm_apply_apply, e.apply_symm_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
inst_4 : MulAction H β
inst_5 : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm : (a : β) → α) ν μ
e : H ≃ G
hef :
  ∀ (g : H),
    Semiconj (⇑f : (a : α) → β) (fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) g : G) x)
      fun (x : β) ↦ g • x
g : G
x : α
rw :
  Eq.{u_3 + 1} (α := α)
    ((f.symm : (a : β) → α)
        ((f : (a : α) → β)
            ((fun (x : α) ↦
                HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) ((e.symm : (a : G) → H) g : H) : G) x)
              x) :
          β) :
      α)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)) : α)
⊢ Eq.{u_3 + 1} (α := α)
    ((f.symm : (a : β) → α)
        ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_4, u_4} (α := H) ((e.symm : (a : G) → H) g : H) x) ((f : (a : α) → β) x)) :
      α)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)) : α)
have rw₁ : Eq.{u_3 + 1} (α := α)
  ((fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) ((e.symm : (a : G) → H) g : H) : G) x) x)
  ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)))
Tactic: rw [← hef _ _, f.symm_apply_apply, f.symm_apply_apply, e.apply_symm_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
inst_4 : MulAction H β
inst_5 : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm : (a : β) → α) ν μ
e : H ≃ G
hef :
  ∀ (g : H),
    Semiconj (⇑f : (a : α) → β) (fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) g : G) x)
      fun (x : β) ↦ g • x
g : G
x : α
rw :
  Eq.{u_3 + 1} (α := α)
    ((f.symm : (a : β) → α)
        ((f : (a : α) → β)
            ((fun (x : α) ↦
                HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) ((e.symm : (a : G) → H) g : H) : G) x)
              x) :
          β) :
      α)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)) : α)
rw₁ :
  Eq.{u_3 + 1} (α := α)
    ((fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) ((e.symm : (a : G) → H) g : H) : G) x) x)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)))
⊢ Eq.{u_3 + 1} (α := α)
    ((f.symm : (a : β) → α)
        ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_4, u_4} (α := H) ((e.symm : (a : G) → H) g : H) x) ((f : (a : α) → β) x)) :
      α)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)) : α)
have rw₂ : Eq.{u_3 + 1} (α := α)
  ((fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) ((e.symm : (a : G) → H) g : H) : G) x) x)
  ((fun (x : α) ↦ g • x) x)
Tactic: rw [← hef _ _, f.symm_apply_apply, f.symm_apply_apply, e.apply_symm_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
inst_4 : MulAction H β
inst_5 : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm : (a : β) → α) ν μ
e : H ≃ G
hef :
  ∀ (g : H),
    Semiconj (⇑f : (a : α) → β) (fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) g : G) x)
      fun (x : β) ↦ g • x
g : G
x : α
rw :
  Eq.{u_3 + 1} (α := α)
    ((f.symm : (a : β) → α)
        ((f : (a : α) → β)
            ((fun (x : α) ↦
                HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) ((e.symm : (a : G) → H) g : H) : G) x)
              x) :
          β) :
      α)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)) : α)
rw₁ :
  Eq.{u_3 + 1} (α := α)
    ((fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) ((e.symm : (a : G) → H) g : H) : G) x) x)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)))
rw₂ :
  Eq.{u_3 + 1} (α := α)
    ((fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) ((e.symm : (a : G) → H) g : H) : G) x) x)
    ((fun (x : α) ↦ g • x) x)
⊢ Eq.{u_3 + 1} (α := α)
    ((f.symm : (a : β) → α)
        ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_4, u_4} (α := H) ((e.symm : (a : G) → H) g : H) x) ((f : (a : α) → β) x)) :
      α)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)) : α)
have rw₃ : Eq.{u_3 + 1} (α := α) ((fun (x : α) ↦ g • x) x) ((fun (x : α) ↦ g • x) x)
Tactic: rw [← hef _ _, f.symm_apply_apply, f.symm_apply_apply, e.apply_symm_apply]
-- 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
⊢ (sum fun (g : G) ↦ ν.restrict (g • s)) = ν
have rw : ν.restrict (⋃ (i : G), i • s) = ν
Tactic: rw [← restrict_iUnion_ae (h.aedisjoint.mono fun i j h => hν h) fun g =>
      (h.nullMeasurableSet_smul g).mono_ac hν,
    restrict_congr_set (hν h.iUnion_smul_ae_eq), restrict_univ]
-- 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
rw : ν.restrict (⋃ (i : G), i • s) = ν
⊢ (sum fun (g : G) ↦ ν.restrict (g • s)) = ν
have rw₁ : ν.restrict univ = ν
Tactic: rw [← restrict_iUnion_ae (h.aedisjoint.mono fun i j h => hν h) fun g =>
      (h.nullMeasurableSet_smul g).mono_ac hν,
    restrict_congr_set (hν h.iUnion_smul_ae_eq), restrict_univ]
-- 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
rw : ν.restrict (⋃ (i : G), i • s) = ν
rw₁ : ν.restrict univ = ν
⊢ (sum fun (g : G) ↦ ν.restrict (g • s)) = ν
have rw₂ : ν = ν
Tactic: rw [← restrict_iUnion_ae (h.aedisjoint.mono fun i j h => hν h) fun g =>
      (h.nullMeasurableSet_smul g).mono_ac hν,
    restrict_congr_set (hν h.iUnion_smul_ae_eq), restrict_univ]
-- 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν
have rw : ∫⁻ (x : α), f x ∂ν = ∫⁻ (a : α), f a ∂sum fun (g : G) ↦ ν.restrict (g • s)
Tactic: rw [← lintegral_sum_measure, h.sum_restrict_of_ac 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → ℝ≥0∞
rw : ∫⁻ (x : α), f x ∂ν = ∫⁻ (a : α), f a ∂sum fun (g : G) ↦ ν.restrict (g • s)
⊢ ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν
have rw₁ : ∫⁻ (x : α), f x ∂ν = ∫⁻ (a : α), f a ∂ν
Tactic: rw [← lintegral_sum_measure, h.sum_restrict_of_ac hν]
-- 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
t : Set α
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∑' (g : G), (ν : (a : Set α) → ℝ≥0∞) (t ∩ g • s) : ℝ≥0∞)
have H : ν.restrict t ≪ μ
Tactic: have H : ν.restrict t ≪ μ := Measure.restrict_le_self.absolutelyContinuous.trans 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
h : IsFundamentalDomain G s μ
t : Set α
ht : ∀ (g : G), g • t = t
hts : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • t ∩ s)) 0
Tactic: rw [measure_eq_tsum 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
inst_6 : Finite G
h : IsFundamentalDomain G s μ
t : Set α
ht : ∀ (g : G), g • t =ᶠ[ae μ] t
⊢ (μ : (a : Set α) → ℝ≥0∞) t = HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have haveI : ∀ (this : Fintype G),
  (μ : (a : Set α) → ℝ≥0∞) t = HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: haveI : Fintype G := Fintype.ofFinite 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
inst_6 : Finite G
h : IsFundamentalDomain G s μ
t : Set α
ht : ∀ (g : G), g • t =ᶠ[ae μ] t
this : Fintype G
⊢ (μ : (a : Set α) → ℝ≥0∞) t = HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw : ∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • t ∩ s) =
  HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [h.measure_eq_tsum]
-- 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
inst_6 : Finite G
h : IsFundamentalDomain G s μ
t : Set α
ht : ∀ (g : G), g • t =ᶠ[ae μ] t
this : Fintype G
⊢ ∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • t ∩ s) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have ht₁ : ∀ (g : G), g • t ∩ s =ᶠ[ae μ] t ∩ s
Tactic: replace ht : ∀ g : G, (g • t ∩ s : Set α) =ᵐ[μ] (t ∩ s : Set α) := fun g =>
    ae_eq_set_inter (ht g) (ae_eq_refl s)
Cleared hypotheses: ht
-- 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
inst_6 : Finite G
h : IsFundamentalDomain G s μ
t : Set α
this : Fintype G
ht : ∀ (g : G), g • t ∩ s =ᶠ[ae μ] t ∩ s
⊢ ∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • t ∩ s) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have simp_rw : ∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (t ∩ s) =
  HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: simp_rw [measure_congr (ht _), tsum_fintype, Finset.sum_const, Nat.card_eq_fintype_card,
    Finset.card_univ]
-- 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
inst_6 : Finite G
h : IsFundamentalDomain G s μ
t : Set α
this : Fintype G
ht : ∀ (g : G), g • t ∩ s =ᶠ[ae μ] t ∩ s
simp_rw :
  ∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (t ∩ s) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ ∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • t ∩ s) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have simp_rw₁ : ∑ g : G, (μ : (a : Set α) → ℝ≥0∞) (t ∩ s) =
  HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: simp_rw [measure_congr (ht _), tsum_fintype, Finset.sum_const, Nat.card_eq_fintype_card,
    Finset.card_univ]
-- 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
inst_6 : Finite G
h : IsFundamentalDomain G s μ
t : Set α
this : Fintype G
ht : ∀ (g : G), g • t ∩ s =ᶠ[ae μ] t ∩ s
simp_rw :
  ∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (t ∩ s) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
simp_rw₁ :
  ∑ g : G, (μ : (a : Set α) → ℝ≥0∞) (t ∩ s) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ ∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • t ∩ s) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have simp_rw₂ : HSMul.hSMul (β := ℝ≥0∞) (Finset.card.{u_1} (α := G) Finset.univ) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: simp_rw [measure_congr (ht _), tsum_fintype, Finset.sum_const, Nat.card_eq_fintype_card,
    Finset.card_univ]
-- 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
inst_6 : Finite G
h : IsFundamentalDomain G s μ
t : Set α
this : Fintype G
ht : ∀ (g : G), g • t ∩ s =ᶠ[ae μ] t ∩ s
simp_rw :
  ∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (t ∩ s) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
simp_rw₁ :
  ∑ g : G, (μ : (a : Set α) → ℝ≥0∞) (t ∩ s) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
simp_rw₂ :
  HSMul.hSMul (β := ℝ≥0∞) (Finset.card.{u_1} (α := G) Finset.univ) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ ∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • t ∩ s) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have simp_rw₃ : HSMul.hSMul (β := ℝ≥0∞) (Finset.card.{u_1} (α := G) Finset.univ) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) (Fintype.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: simp_rw [measure_congr (ht _), tsum_fintype, Finset.sum_const, Nat.card_eq_fintype_card,
    Finset.card_univ]
-- 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 α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' A = A
⊢ ∫⁻ (x : α) in s, A.indicator 1 x ∂μ = ∫⁻ (x : α) in t, A.indicator 1 x ∂μ
have refine : ∀ (g : G) (x : α), Eq (α := ℝ≥0∞) (A.indicator (fun (x : α) ↦ 1) (g • x)) (A.indicator (fun (x : α) ↦ 1) x)
Tactic: refine hs.setLIntegral_eq ht (Set.indicator A fun _ => 1) fun g 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 α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' A = A
g : G
x : α
⊢ Eq (α := ℝ≥0∞) (A.indicator (fun (x : α) ↦ 1) (g • x)) (A.indicator (fun (x : α) ↦ 1) x)
have h : A = (fun (x : α) ↦ g • x) ⁻¹' A
Tactic: convert! (Set.indicator_comp_right (g • · : α → α) (g := fun _ ↦ (1 : ℝ≥0∞))).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 α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' A = A
g : G
x : α
⊢ A = (fun (x : α) ↦ g • x) ⁻¹' A
have h : A = A
Tactic: rw [hA 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 α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' A = A
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A ∩ t) : ℝ≥0∞)
have this : ∫⁻ (x : α) in s, A.indicator 1 x ∂μ = ∫⁻ (x : α) in t, A.indicator 1 x ∂μ
Tactic: have : ∫⁻ x in s, A.indicator 1 x ∂μ = ∫⁻ x in t, A.indicator 1 x ∂μ := by
    refine hs.setLIntegral_eq ht (Set.indicator A fun _ => 1) fun g x ↦ ?_
    convert! (Set.indicator_comp_right (g • · : α → α) (g := fun _ ↦ (1 : ℝ≥0∞))).symm
    rw [hA 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 α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
β : Type u_6
inst_6 : TopologicalSpace β
inst_7 : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ (∀ (g : G), AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t)))) ↔
    ∀ (g : G), AEStronglyMeasurable f (μ.restrict (g • s ∩ t))
have refine : ∀ (g : G), AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t))) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))
Tactic: refine forall_congr' fun 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 α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
β : Type u_6
inst_6 : TopologicalSpace β
inst_7 : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
⊢ AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t))) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))
have he : MeasurableEmbedding (β := α) fun (x : α) ↦ g⁻¹ • x
Tactic: have he : MeasurableEmbedding (g⁻¹ • · : α → α) := measurableEmbedding_const_smul _
-- 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 α
s t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
β : Type u_6
inst_6 : TopologicalSpace β
inst_7 : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
he : MeasurableEmbedding (β := α) fun (x : α) ↦ g⁻¹ • x
⊢ AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t))) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))
have rw : AEStronglyMeasurable (f ∘ fun (x : α) ↦ g⁻¹ • x) (μ.restrict (g • s ∩ t)) ↔
  AEStronglyMeasurable f (μ.restrict (g • s ∩ t))
Tactic: rw [← image_smul, ← ((measurePreserving_smul g⁻¹ μ).restrict_image_emb he
        _).aestronglyMeasurable_comp_iff he]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ < ∞ ↔ ∫⁻ (a : α) in t, ‖f a‖ₑ ∂μ < ∞
have hf₁ : ∀ (g : G) (x : α), ‖f (g • x)‖ₑ = ‖f x‖ₑ
Tactic: rw [hs.setLIntegral_eq ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
x : α
⊢ ‖f (g • x)‖ₑ = ‖f x‖ₑ
have hf₁ : ‖f x‖ₑ = ‖f x‖ₑ
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
ν : Measure α
inst_7 : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → E
hf : Integrable f ν
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α), f x ∂ν) (∑' (g : G), ∫ (x : α) in g • s, f x ∂ν)
have rw : @Integrable _ _ _ _ inst_2 f (sum fun (g : G) ↦ ν.restrict (g • s))
Tactic: rw [← MeasureTheory.integral_sum_measure, h.sum_restrict_of_ac hν]