awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
refine :
  ∀ (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) x) :
        α)
      ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) x) : α)
⊢ IsFundamentalDomain H ((⇑f.symm : (a : β) → α) ⁻¹' s) ν

Tactic:
refine h.preimage_of_equiv hf e.symm.bijective fun g x => ?_

Premises used: Equiv.bijective, MeasureTheory.IsFundamentalDomain.preimage_of_equiv, Equiv.symm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 : β
rcases :
  ∀ (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 : β)) : α)
⊢ 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) x) :
      α)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) x) : α)

Tactic:
rcases f.surjective x with ⟨x, rfl⟩

Premises used: Equiv.surjective, rfl
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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)
rw₃ rw₄ : Eq.{u_3 + 1} (α := α) ((fun (x : α) ↦ 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 : β)) : α)

Tactic:
rw [← hef _ _, f.symm_apply_apply, f.symm_apply_apply, e.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Equiv.symm_apply_apply
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
⊢ Pairwise fun (g₁ g₂ : G) ↦ AEDisjoint ν (g₁ • s) (g₂ • s)

Tactic:
h.aedisjoint.mono fun _ _ H => hν H

Premises used: MeasureTheory.IsFundamentalDomain.aedisjoint, Pairwise.mono
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
G' : Type u_6
inst_3 : Group G'
inst_4 : MulAction G' α
inst_5 : MeasurableConstSMul G' α
inst_6 : SMulInvariantMeasure G' α μ
inst_7 : SMulCommClass G' G α
h : IsFundamentalDomain G s μ
g : G'
⊢ IsFundamentalDomain G (g • s) μ

Tactic:
h.image_of_equiv (MulAction.toPerm g) (measurePreserving_smul _ _).quasiMeasurePreserving
    (Equiv.refl _) <| smul_comm g

Premises used: MulAction.toPerm, MeasureTheory.measurePreserving_smul, MeasureTheory.MeasurePreserving.quasiMeasurePreserving, SMulCommClass.smul_comm, Equiv.refl, MeasureTheory.IsFundamentalDomain.image_of_equiv
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α μ
h : IsFundamentalDomain G s μ
g : G
⊢ NullMeasurableSet (g • s) μ

Tactic:
h.nullMeasurableSet.smul g

Premises used: MeasureTheory.IsFundamentalDomain.nullMeasurableSet, MeasureTheory.NullMeasurableSet.smul
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α μ
h : IsFundamentalDomain G s μ
g : G
t : Set α
⊢ (μ.restrict t).restrict (g • s) = μ.restrict (g • s ∩ t)

Tactic:
restrict_restrict₀ ((h.nullMeasurableSet_smul g).mono restrict_le_self)

Premises used: MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul, MeasureTheory.Measure.restrict_restrict₀, MeasureTheory.Measure.restrict_le_self, MeasureTheory.NullMeasurableSet.mono
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α μ
h : IsFundamentalDomain G s μ
g g' : G
⊢ (fun (g' : G) ↦ g * g' * g⁻¹) ((fun (g' : G) ↦ g⁻¹ * g' * g) g') = g'

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α μ
h : IsFundamentalDomain G s μ
g g' : G
⊢ (fun (g' : G) ↦ g⁻¹ * g' * g) ((fun (g' : G) ↦ g * g' * g⁻¹) g') = g'

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α μ
h : IsFundamentalDomain G s μ
g g' : G
x : α
⊢ Eq.{u_3 + 1} (α := α)
    ((MulAction.toPerm g : (a : α) → α)
        ((fun (x : α) ↦
            HSMul.hSMul (α := G)
              (({ toFun := fun (g' : G) ↦ g⁻¹ * g' * g, invFun := fun (g' : G) ↦ g * g' * g⁻¹, left_inv := ⋯,
                      right_inv := ⋯ } :
                    (a : G) → G)
                  g' :
                G)
              x)
          x) :
      α)
    ((fun (x : α) ↦ g' • x) ((MulAction.toPerm g : (a : α) → α) x) : α)

Tactic:
simp [smul_smul, mul_assoc]

Premises used: mul_assoc, smul_smul
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 = ν
rw₂ rw₃ : ν = ν
⊢ (sum fun (g : G) ↦ ν.restrict (g • 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]

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul, MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq, MeasureTheory.Measure.restrict_iUnion_ae, MeasureTheory.IsFundamentalDomain.aedisjoint, MeasureTheory.NullMeasurableSet.mono_ac, Pairwise.mono, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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)
rw₁ rw₂ : ∫⁻ (x : α), f x ∂ν = ∫⁻ (a : α), f a ∂ν
⊢ ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν

Tactic:
rw [← lintegral_sum_measure, h.sum_restrict_of_ac hν]

Premises used: MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac, MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 μ
⊢ (sum fun (g : G) ↦ μ.restrict (g • s)) = μ

Tactic:
h.sum_restrict_of_ac (refl _)

Premises used: MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac, refl
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 μ
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂μ

Tactic:
h.lintegral_eq_tsum_of_ac (refl _) f

Premises used: MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac, refl
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 μ
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g⁻¹ • x) ∂μ

Tactic:
calc
    ∫⁻ x, f x ∂μ = ∑' g : G, ∫⁻ x in g • s, f x ∂μ := h.lintegral_eq_tsum f
    _ = ∑' g : G, ∫⁻ x in g⁻¹ • s, f x ∂μ := ((Equiv.inv G).tsum_eq _).symm
    _ = ∑' g : G, ∫⁻ x in s, f (g⁻¹ • x) ∂μ := tsum_congr fun g => Eq.symm <|
      (measurePreserving_smul g⁻¹ μ).setLIntegral_comp_emb (measurableEmbedding_const_smul _) _ _

Premises used: MeasureTheory.MeasurePreserving.setLIntegral_comp_emb, Trans.trans, Equiv.inv, tsum_congr, Equiv.tsum_eq, measurableEmbedding_const_smul, MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum, Inv.inv, MeasureTheory.measurePreserving_smul, 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 α
s : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
h : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g • x) ∂μ

Tactic:
(lintegral_eq_tsum' h f).trans ((Equiv.inv G).tsum_eq (fun g ↦ ∫⁻ (x : α) in s, f (g • x) ∂μ))

Premises used: Equiv.inv, MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum', Equiv.tsum_eq, MeasureTheory.Measure.restrict, HSMul.hSMul, MeasureTheory.lintegral, Eq.trans
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 μ
f : α → ℝ≥0∞
t : Set α
⊢ Eq (α := ℝ≥0∞) (∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂μ.restrict t) (∑' (g : G), ∫⁻ (x : α) in t ∩ g • s, f x ∂μ)

Tactic:
simp only [h.restrict_restrict, inter_comm]

Premises used: MeasureTheory.IsFundamentalDomain.restrict_restrict, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 μ
f : α → ℝ≥0∞
t : Set α
⊢ Eq (α := ℝ≥0∞) (∑' (g : G), ∫⁻ (x : α) in t ∩ g⁻¹ • s, f x ∂μ) (∑' (g : G), ∫⁻ (x : α) in g⁻¹ • (g • t ∩ s), f x ∂μ)

Tactic:
simp only [smul_set_inter, inv_smul_smul]

Premises used: Set.smul_set_inter, inv_smul_smul
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α
⊢ ν.restrict t ≪ μ

Tactic:
have H : ν.restrict t ≪ μ := Measure.restrict_le_self.absolutelyContinuous.trans hν
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α
H : ν.restrict t ≪ μ
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∑' (g : G), (ν : (a : Set α) → ℝ≥0∞) (t ∩ g • s) : ℝ≥0∞)

Tactic:
simpa only [setLIntegral_one, Pi.one_def,
    Measure.restrict_apply₀ ((h.nullMeasurableSet_smul _).mono_ac H), inter_comm] using
    h.lintegral_eq_tsum_of_ac H 1

Premises used: MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul, MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac, MeasureTheory.setLIntegral_one, Set.inter_comm, Pi.one_def, MeasureTheory.Measure.restrict_apply₀, MeasureTheory.NullMeasurableSet.mono_ac, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (t ∩ g • s) : ℝ≥0∞)

Tactic:
h.measure_eq_tsum_of_ac AbsolutelyContinuous.rfl t

Premises used: MeasureTheory.IsFundamentalDomain.measure_eq_tsum_of_ac, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • t ∩ s) : ℝ≥0∞)

Tactic:
simpa only [setLIntegral_one] using h.setLIntegral_eq_tsum' (fun _ => 1) t

Premises used: MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum', MeasureTheory.setLIntegral_one, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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∞)
rw : Eq (α := ℝ≥0∞) (∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • t ∩ s)) 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [measure_eq_tsum h]

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 α
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∞) (∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • t ∩ s)) 0

Tactic:
simp [ht, hts]
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
haveI :
  ∀ (this : Fintype G),
    (μ : (a : Set α) → ℝ≥0∞) t = HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) t = HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
haveI : Fintype G := Fintype.ofFinite G
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
rw :
  ∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • t ∩ s) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) t = HSMul.hSMul (β := ℝ≥0∞) (Nat.card G) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
rw [h.measure_eq_tsum]

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 α
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), 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)
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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∞)
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∞)
⊢ ∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • 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]

Premises used: Finset.card_univ, MeasureTheory.measure_congr, tsum_fintype, Nat.card_eq_fintype_card, Finset.sum_const
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 μ
f : α → ℝ≥0∞
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ Eq (α := ℝ≥0∞) (∑' (g : G), ∫⁻ (x : α) in s ∩ g • t, f x ∂μ) (∑' (g : G), ∫⁻ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ)

Tactic:
simp only [hf, inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 ∂μ

Tactic:
hs.setLIntegral_eq ht (Set.indicator A fun _ => 1) fun g x ↦ ?_

Premises used: Set.indicator, MeasureTheory.IsFundamentalDomain.setLIntegral_eq, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
refine : ∀ (g : G) (x : α), Eq (α := ℝ≥0∞) (A.indicator (fun (x : α) ↦ 1) (g • x)) (A.indicator (fun (x : α) ↦ 1) x)
⊢ ∫⁻ (x : α) in s, A.indicator 1 x ∂μ = ∫⁻ (x : α) in t, A.indicator 1 x ∂μ

Tactic:
refine hs.setLIntegral_eq ht (Set.indicator A fun _ => 1) fun g x ↦ ?_

Premises used: Set.indicator, MeasureTheory.IsFundamentalDomain.setLIntegral_eq, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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))
    (indicator ((fun (x : α) ↦ g • x) ⁻¹' A) ((fun (x : α) ↦ 1) ∘ fun (x : α) ↦ g • x) x)

Tactic:
(Set.indicator_comp_right (g • · : α → α) (g := fun _ ↦ (1 : ℝ≥0∞))).symm

Premises used: Set.indicator_comp_right, HSMul.hSMul, 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 α
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 : α
h : A = (fun (x : α) ↦ g • x) ⁻¹' A
⊢ Eq (α := ℝ≥0∞) (A.indicator (fun (x : α) ↦ 1) (g • x)) (A.indicator (fun (x : α) ↦ 1) x)

Tactic:
convert! (Set.indicator_comp_right (g • · : α → α) (g := fun _ ↦ (1 : ℝ≥0∞))).symm

Premises used: Set.indicator_comp_right, HSMul.hSMul, 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 α
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 : α
h h₁ : A = A
⊢ A = (fun (x : α) ↦ g • x) ⁻¹' A

Tactic:
rw [hA g]