awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : Eq (α := ℝ≥0∞) (((map π (μ.restrict 𝓕) : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  ∀ (hs : Eq (α := ℝ≥0∞) ((μ.restrict 𝓕 : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map π μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [map_apply meas_π s_meas] at hs ⊢

Premises used: MeasureTheory.Measure.map_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : Eq (α := ℝ≥0∞) ((μ.restrict 𝓕 : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ : MeasurableSet (π ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply] at hs

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
apply : ∀ (g : ↥Γ.op), g • π ⁻¹' s = π ⁻¹' s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply h𝓕.measure_zero_of_invariant _ _ hs

Premises used: MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
γ : ↥Γ.op
h : ∀ (g : G), g ∈ γ • π ⁻¹' s ↔ g ∈ π ⁻¹' s
⊢ γ • π ⁻¹' s = π ⁻¹' s

Tactic:
ext g
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
γ : ↥Γ.op
g : G
h : π (γ⁻¹ • g) ∈ s ↔ π g ∈ s
⊢ g ∈ γ • π ⁻¹' s ↔ g ∈ π ⁻¹' s

Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem, mem_preimage, mem_preimage]

Premises used: Set.mem_smul_set_iff_inv_smul_mem, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
γ : ↥Γ.op
g : G
h : π (γ⁻¹ • g) = π g
⊢ π (γ⁻¹ • g) ∈ s ↔ π g ∈ s

Tactic:
congr! 1
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
γ : ↥Γ.op
g : G
⊢ Eq (α := G ⧸ Γ) (↑(g * MulOpposite.unop (↑γ⁻¹ : Gᵐᵒᵖ)) : G ⧸ Γ) (↑g : G ⧸ Γ)

Tactic:
QuotientGroup.mk_mul_of_mem g (γ⁻¹).2

Premises used: QuotientGroup.mk_mul_of_mem, Inv.inv, Subtype.property
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)
γ : ↥Γ.op
g : G
⊢ π (γ⁻¹ • g) = π g

Tactic:
convert! QuotientGroup.mk_mul_of_mem g (γ⁻¹).2 using 1

Premises used: QuotientGroup.mk_mul_of_mem, Inv.inv, Subtype.property
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : Eq (α := ℝ≥0∞) ((μ.restrict 𝓕 : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ MeasurableSet (π ⁻¹' s)

Tactic:
MeasurableSet.preimage s_meas meas_π

Premises used: MeasurableSet.preimage
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
hs : Eq (α := ℝ≥0∞) ((μ.restrict 𝓕 : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ MeasurableSet (π ⁻¹' s)

Tactic:
exact MeasurableSet.preimage s_meas meas_π

Premises used: MeasurableSet.preimage
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
E : Type u_2
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
inst_10 : μ.IsMulRightInvariant
f : G → E
hf₁ : Integrable f μ
hf₂ : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : G), f x ∂μ) (∑' (γ : ↥Γ.op), ∫ (x : G) in 𝓕, f (γ • x) ∂μ)

Tactic:
h𝓕.integral_eq_tsum'' f hf₁

Premises used: MeasureTheory.IsFundamentalDomain.integral_eq_tsum''
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
E : Type u_2
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
inst_10 : μ.IsMulRightInvariant
f : G → E
hf₁ : Integrable f μ
hf₂ : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
⊢ Eq.{u_2 + 1} (α := E) (∑' (γ : ↥Γ.op), ∫ (x : G) in 𝓕, f (γ • x) ∂μ) (∫ (x : G) in 𝓕, ∑' (γ : ↥Γ.op), f (γ • x) ∂μ)

Tactic:
?_
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
E : Type u_2
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
inst_10 : μ.IsMulRightInvariant
f : G → E
hf₁ : Integrable f μ
hf₂ : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : G) in 𝓕, ∑' (γ : ↥Γ.op), f (γ • x) ∂μ)
    (@integral _ _ _ _ inst_6 (Measure.map mk (μ.restrict 𝓕)) fun (x : G ⧸ Γ) ↦ automorphize f x)

Tactic:
(integral_map continuous_quotient_mk'.aemeasurable hf₂).symm

Premises used: MeasureTheory.integral_map, continuous_quotient_mk', MulAction.automorphize, Continuous.aemeasurable, Quotient.mk', QuotientGroup.automorphize, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
E : Type u_2
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
inst_10 : μ.IsMulRightInvariant
f : G → E
hf₁ : Integrable f μ
hf₂ : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
calc :
  Eq.{u_2 + 1} (α := E) (∑' (γ : ↥Γ.op), ∫ (x : G) in 𝓕, f (γ • x) ∂μ) (∫ (x : G) in 𝓕, ∑' (γ : ↥Γ.op), f (γ • x) ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : G), f x ∂μ)
    (@integral _ _ _ _ inst_6 (Measure.map mk (μ.restrict 𝓕)) fun (x : G ⧸ Γ) ↦ automorphize f x)

Tactic:
calc ∫ x : G, f x ∂μ = ∑' γ : Γ.op, ∫ x in 𝓕, f (γ • x) ∂μ :=
    h𝓕.integral_eq_tsum'' f hf₁
    _ = ∫ x in 𝓕, ∑' γ : Γ.op, f (γ • x) ∂μ := ?_
    _ = ∫ x : G ⧸ Γ, automorphize f x ∂μ_𝓕 :=
      (integral_map continuous_quotient_mk'.aemeasurable hf₂).symm

Premises used: MeasureTheory.integral_map, continuous_quotient_mk', MeasureTheory.IsFundamentalDomain.integral_eq_tsum'', Subgroup.op, Continuous.aemeasurable, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
E : Type u_2
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
inst_10 : μ.IsMulRightInvariant
f : G → E
hf₁ : Integrable f μ
hf₂ : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
hf : ∀ (i : ↥Γ.op), AEStronglyMeasurable.{u_1, u_2} (β := E) (fun (x : G) ↦ f (i • x)) (μ.restrict 𝓕)
hf' : Ne (α := ℝ≥0∞) (∑' (i : ↥Γ.op), ∫⁻ (a : G) in 𝓕, ‖f (i • a)‖ₑ ∂μ) ∞
⊢ Eq.{u_2 + 1} (α := E) (∑' (γ : ↥Γ.op), ∫ (x : G) in 𝓕, f (γ • x) ∂μ) (∫ (x : G) in 𝓕, ∑' (γ : ↥Γ.op), f (γ • x) ∂μ)

Tactic:
rw [integral_tsum]

Premises used: MeasureTheory.integral_tsum
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
E : Type u_2
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
inst_10 : μ.IsMulRightInvariant
f : G → E
hf₁ : Integrable f μ
hf₂ : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
⊢ ∀ (i : ↥Γ.op), AEStronglyMeasurable.{u_1, u_2} (β := E) (fun (x : G) ↦ f (i • x)) (μ.restrict 𝓕)

Tactic:
fun i ↦ (hf₁.1.comp_quasiMeasurePreserving
      (measurePreserving_smul i μ).quasiMeasurePreserving).restrict

Premises used: MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving, MeasureTheory.AEStronglyMeasurable.restrict, And.left, MeasureTheory.measurePreserving_smul, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
E : Type u_2
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
inst_10 : μ.IsMulRightInvariant
f : G → E
hf₁ : Integrable f μ
hf₂ : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
⊢ ∀ (i : ↥Γ.op), AEStronglyMeasurable.{u_1, u_2} (β := E) (fun (x : G) ↦ f (i • x)) (μ.restrict 𝓕)

Tactic:
exact fun i ↦ (hf₁.1.comp_quasiMeasurePreserving
      (measurePreserving_smul i μ).quasiMeasurePreserving).restrict

Premises used: MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving, MeasureTheory.AEStronglyMeasurable.restrict, And.left, MeasureTheory.measurePreserving_smul, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
E : Type u_2
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
inst_10 : μ.IsMulRightInvariant
f : G → E
hf₁ : Integrable f μ
hf₂ : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
hf' : ∫⁻ (x : G), ‖f x‖ₑ ∂μ ≠ ∞
⊢ Ne (α := ℝ≥0∞) (∑' (i : ↥Γ.op), ∫⁻ (a : G) in 𝓕, ‖f (i • a)‖ₑ ∂μ) ∞

Tactic:
rw [← h𝓕.lintegral_eq_tsum'' (‖f ·‖ₑ)]

Premises used: MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum'', ENorm.enorm
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
E : Type u_2
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
inst_10 : μ.IsMulRightInvariant
f : G → E
hf₁ : Integrable f μ
hf₂ : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
⊢ ∫⁻ (x : G), ‖f x‖ₑ ∂μ ≠ ∞

Tactic:
ne_of_lt hf₁.2

Premises used: And.right, ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
E : Type u_2
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
inst_10 : μ.IsMulRightInvariant
f : G → E
hf₁ : Integrable f μ
hf₂ : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
⊢ ∫⁻ (x : G), ‖f x‖ₑ ∂μ ≠ ∞

Tactic:
exact ne_of_lt hf₁.2

Premises used: And.right, ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
K : Type u_2
inst_8 : NormedField K
inst_9 : NormedSpace ℝ K
inst_10 : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable (m₀ := inst_6) g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : Ne (α := ℝ≥0∞) (@essSup _ _ _ inst_6 (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))) ∞
F_ae_measurable : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
π : G → G ⧸ Γ := mk
⊢ Measurable π

Tactic:
have meas_π : Measurable π := continuous_quotient_mk'.measurable
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
K : Type u_2
inst_8 : NormedField K
inst_9 : NormedSpace ℝ K
inst_10 : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable (m₀ := inst_6) g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : Ne (α := ℝ≥0∞) (@essSup _ _ _ inst_6 (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))) ∞
F_ae_measurable : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
π : G → G ⧸ Γ := mk
meas_π : Measurable π
⊢ automorphize (g ∘ π * f) = g * automorphize f

Tactic:
QuotientGroup.automorphize_smul_left f g

Premises used: Quotient.mk', QuotientGroup.automorphize_smul_left
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
K : Type u_2
inst_8 : NormedField K
inst_9 : NormedSpace ℝ K
inst_10 : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable (m₀ := inst_6) g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : Ne (α := ℝ≥0∞) (@essSup _ _ _ inst_6 (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))) ∞
F_ae_measurable : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
π : G → G ⧸ Γ := mk
meas_π : Measurable π
⊢ automorphize (g ∘ π * f) = g * automorphize f

Tactic:
exact QuotientGroup.automorphize_smul_left f g

Premises used: QuotientGroup.automorphize_smul_left
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
K : Type u_2
inst_8 : NormedField K
inst_9 : NormedSpace ℝ K
inst_10 : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable (m₀ := inst_6) g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : Ne (α := ℝ≥0∞) (@essSup _ _ _ inst_6 (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))) ∞
F_ae_measurable : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
π : G → G ⧸ Γ := mk
meas_π : Measurable π
⊢ automorphize (g ∘ π * f) = g * automorphize f

Tactic:
have H₀ : QuotientGroup.automorphize ((g ∘ π) * f) = g * (QuotientGroup.automorphize f) := by
    exact QuotientGroup.automorphize_smul_left f g
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
K : Type u_2
inst_8 : NormedField K
inst_9 : NormedSpace ℝ K
inst_10 : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable (m₀ := inst_6) g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : Ne (α := ℝ≥0∞) (@essSup _ _ _ inst_6 (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))) ∞
F_ae_measurable : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
π : G → G ⧸ Γ := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
⊢ Eq.{u_2 + 1} (α := K) (∫ (x : G), g (π x) * f x ∂μ)
    (@integral _ _ _ _ inst_6 (Measure.map mk (μ.restrict 𝓕)) fun (x : G ⧸ Γ) ↦ automorphize (g ∘ π * f) x)

Tactic:
?_
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst_5 : Countable.{u_1 + 1} ↥Γ
inst_6 : MeasurableSpace (G ⧸ Γ)
inst_7 : BorelSpace.{u_1} (G ⧸ Γ)
K : Type u_2
inst_8 : NormedField K
inst_9 : NormedSpace ℝ K
inst_10 : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable (m₀ := inst_6) g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : Ne (α := ℝ≥0∞) (@essSup _ _ _ inst_6 (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))) ∞
F_ae_measurable : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize f) (Measure.map mk (μ.restrict 𝓕))
π : G → G ⧸ Γ := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
⊢ Eq.{u_2 + 1} (α := K)
    (@integral _ _ _ _ inst_6 (Measure.map mk (μ.restrict 𝓕)) fun (x : G ⧸ Γ) ↦ automorphize (g ∘ π * f) x)
    (@integral _ _ _ _ inst_6 (Measure.map mk (μ.restrict 𝓕)) fun (x : G ⧸ Γ) ↦ g x * automorphize f x)

Tactic:
simp [H₀]