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 ⧸ Γ)
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
calc :
  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)
⊢ Eq.{u_2 + 1} (α := K) (∫ (x : G), g (↑x : G ⧸ Γ) * f x ∂μ)
    (@integral _ _ _ _ inst_6 (Measure.map mk (μ.restrict 𝓕)) fun (x : G ⧸ Γ) ↦ g x * automorphize f x)

Tactic:
calc ∫ (x : G), g (π x) * (f x) ∂μ =
        ∫ (x : G ⧸ Γ), QuotientGroup.automorphize ((g ∘ π) * f) x ∂μ_𝓕 := ?_
    _ = ∫ (x : G ⧸ Γ), g x * (QuotientGroup.automorphize f x) ∂μ_𝓕 := by simp [H₀]
-- 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
⊢ AEStronglyMeasurable.{u_1, u_2} (β := K) (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ

Tactic:
have : AEStronglyMeasurable (fun (x : G) ↦ g (x : (G ⧸ Γ))) μ :=
      (hg.mono_ac h𝓕.absolutelyContinuous_map).comp_measurable meas_π
-- 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
this : AEStronglyMeasurable.{u_1, u_2} (β := K) (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ
⊢ Integrable (g ∘ π * f) μ

Tactic:
Integrable.essSup_smul f_ℒ_1 this ?_

Premises used: MeasureTheory.Integrable.essSup_smul
-- 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
this : AEStronglyMeasurable.{u_1, u_2} (β := K) (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ
refine : Ne (α := ℝ≥0∞) (essSup (fun (x : G) ↦ ‖g (↑x : G ⧸ Γ)‖ₑ) μ) ∞
⊢ Integrable (g ∘ π * f) μ

Tactic:
refine Integrable.essSup_smul f_ℒ_1 this ?_

Premises used: MeasureTheory.Integrable.essSup_smul
-- 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
this : AEStronglyMeasurable.{u_1, u_2} (β := K) (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ
⊢ AEStronglyMeasurable (β := ℝ≥0∞) (m₀ := inst_6) (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))

Tactic:
have hg' : AEStronglyMeasurable (‖g ·‖ₑ) μ_𝓕 := continuous_enorm.comp_aestronglyMeasurable hg
-- 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
this : AEStronglyMeasurable.{u_1, u_2} (β := K) (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ
hg' : AEStronglyMeasurable (β := ℝ≥0∞) (m₀ := inst_6) (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))
rw : Ne (α := ℝ≥0∞) (@essSup _ _ _ inst_6 (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))) ∞
⊢ Ne (α := ℝ≥0∞) (essSup (fun (x : G) ↦ ‖g (↑x : G ⧸ Γ)‖ₑ) μ) ∞

Tactic:
rw [← essSup_comp_quotientGroup_mk h𝓕 hg'.aemeasurable]

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, essSup_comp_quotientGroup_mk
-- 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
this : AEStronglyMeasurable.{u_1, u_2} (β := K) (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ
hg' : AEStronglyMeasurable (β := ℝ≥0∞) (m₀ := inst_6) (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))
⊢ Ne (α := ℝ≥0∞) (@essSup _ _ _ inst_6 (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))) ∞

Tactic:
g_ℒ_infinity
-- 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
this : AEStronglyMeasurable.{u_1, u_2} (β := K) (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ
hg' : AEStronglyMeasurable (β := ℝ≥0∞) (m₀ := inst_6) (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))
⊢ Ne (α := ℝ≥0∞) (@essSup _ _ _ inst_6 (fun (x : G ⧸ Γ) ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))) ∞

Tactic:
exact g_ℒ_infinity
-- 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
⊢ Integrable (g ∘ π * f) μ

Tactic:
have H₁ : Integrable ((g ∘ π) * f) μ := by
    have : AEStronglyMeasurable (fun (x : G) ↦ g (x : (G ⧸ Γ))) μ :=
      (hg.mono_ac h𝓕.absolutelyContinuous_map).comp_measurable meas_π
    refine Integrable.essSup_smul f_ℒ_1 this ?_
    have hg' : AEStronglyMeasurable (‖g ·‖ₑ) μ_𝓕 := continuous_enorm.comp_aestronglyMeasurable hg
    rw [← essSup_comp_quotientGroup_mk h𝓕 hg'.aemeasurable]
    exact g_ℒ_infinity
-- 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
H₁ : Integrable (g ∘ π * f) μ
simp_rw : AEStronglyMeasurable (m₀ := inst_6) (g * automorphize f) (Measure.map mk (μ.restrict 𝓕))
⊢ AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize (g ∘ π * f)) (Measure.map mk (μ.restrict 𝓕))

Tactic:
simp_rw [H₀]
-- 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
H₁ : Integrable (g ∘ π * f) μ
⊢ AEStronglyMeasurable (m₀ := inst_6) (g * automorphize f) (Measure.map mk (μ.restrict 𝓕))

Tactic:
hg.mul F_ae_measurable

Premises used: MeasureTheory.AEStronglyMeasurable.mul
-- 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
H₁ : Integrable (g ∘ π * f) μ
⊢ AEStronglyMeasurable (m₀ := inst_6) (g * automorphize f) (Measure.map mk (μ.restrict 𝓕))

Tactic:
exact hg.mul F_ae_measurable

Premises used: MeasureTheory.AEStronglyMeasurable.mul
-- 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
H₁ : Integrable (g ∘ π * f) μ
⊢ AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize (g ∘ π * f)) (Measure.map mk (μ.restrict 𝓕))

Tactic:
have H₂ : AEStronglyMeasurable (QuotientGroup.automorphize ((g ∘ π) * f)) μ_𝓕 := by
    simp_rw [H₀]
    exact hg.mul F_ae_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 π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
H₁ : Integrable (g ∘ π * f) μ
H₂ : AEStronglyMeasurable (α := G ⧸ Γ) (m₀ := inst_6) (automorphize (g ∘ π * f)) (Measure.map mk (μ.restrict 𝓕))
⊢ 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:
apply QuotientGroup.integral_eq_integral_automorphize h𝓕 H₁ H₂

Premises used: QuotientGroup.integral_eq_integral_automorphize
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G' : Type u_1
inst : AddGroup G'
inst_1 : MeasurableSpace G'
inst_2 : TopologicalSpace G'
inst_3 : IsTopologicalAddGroup G'
inst_4 : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.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 : μ'.IsAddRightInvariant
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 : AddGroup G'
inst_1 : MeasurableSpace G'
inst_2 : TopologicalSpace G'
inst_3 : IsTopologicalAddGroup G'
inst_4 : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.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 : μ'.IsAddRightInvariant
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₀ : QuotientAddGroup.automorphize ((g ∘ π) * f) = g * (QuotientAddGroup.automorphize f) :=
    QuotientAddGroup.automorphize_smul_left f g
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G' : Type u_1
inst : AddGroup G'
inst_1 : MeasurableSpace G'
inst_2 : TopologicalSpace G'
inst_3 : IsTopologicalAddGroup G'
inst_4 : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.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 : μ'.IsAddRightInvariant
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 : AddGroup G'
inst_1 : MeasurableSpace G'
inst_2 : TopologicalSpace G'
inst_3 : IsTopologicalAddGroup G'
inst_4 : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.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 : μ'.IsAddRightInvariant
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₀]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G' : Type u_1
inst : AddGroup G'
inst_1 : MeasurableSpace G'
inst_2 : TopologicalSpace G'
inst_3 : IsTopologicalAddGroup G'
inst_4 : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.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 : μ'.IsAddRightInvariant
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
calc :
  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)
⊢ Eq.{u_2 + 1} (α := K) (∫ (x : G'), g (↑x : G' ⧸ Γ') * f x ∂μ')
    (@integral _ _ _ _ inst_6 (Measure.map mk (μ'.restrict 𝓕')) fun (x : G' ⧸ Γ') ↦ g x * automorphize f x)

Tactic:
calc ∫ (x : G'), g (π x) * f x ∂μ' =
    ∫ (x : G' ⧸ Γ'), QuotientAddGroup.automorphize ((g ∘ π) * f) x ∂μ_𝓕 := ?_
    _ = ∫ (x : G' ⧸ Γ'), g x * (QuotientAddGroup.automorphize f x) ∂μ_𝓕 := by simp [H₀]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G' : Type u_1
inst : AddGroup G'
inst_1 : MeasurableSpace G'
inst_2 : TopologicalSpace G'
inst_3 : IsTopologicalAddGroup G'
inst_4 : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.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 : μ'.IsAddRightInvariant
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
⊢ AEStronglyMeasurable.{u_1, u_2} (β := K) (fun (x : G') ↦ g (↑x : G' ⧸ Γ')) μ'

Tactic:
have : AEStronglyMeasurable (fun (x : G') ↦ g (x : (G' ⧸ Γ'))) μ' :=
      (hg.mono_ac h𝓕.absolutelyContinuous_map).comp_measurable meas_π