awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 : 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
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 : 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
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 : 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
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_quotientAddGroup_mk h𝓕 hg'.aemeasurable]

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, essSup_comp_quotientAddGroup_mk
-- 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
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 : 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
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 : 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
⊢ 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_quotientAddGroup_mk h𝓕 hg'.aemeasurable]
    exact g_ℒ_infinity
-- 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
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 : 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
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 : 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
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 : 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
H₁ : Integrable (g ∘ π * f) μ'
⊢ AEStronglyMeasurable (α := G' ⧸ Γ') (m₀ := inst_6) (automorphize (g ∘ π * f)) (Measure.map mk (μ'.restrict 𝓕'))

Tactic:
have H₂ : AEStronglyMeasurable (QuotientAddGroup.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 : 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
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 QuotientAddGroup.integral_eq_integral_automorphize h𝓕 H₁ H₂

Premises used: QuotientAddGroup.integral_eq_integral_automorphize
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
⊢ IsCompact k

Tactic:
have k_comp : IsCompact k := h'g
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
apply : ∀ (x₀ : G), ContinuousAt.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀
⊢ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ

Tactic:
apply continuous_iff_continuousAt.2 (fun x₀ ↦ ?_)

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
⊢ ∃ (t : Set G), IsCompact t ∧ t ∈ 𝓝 x₀

Tactic:
exists_compact_mem_nhds x₀

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
obtain :
  ∀ (t : Set G) (t_comp : IsCompact t) (ht : t ∈ 𝓝 x₀),
    ContinuousAt.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀
⊢ ContinuousAt.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀

Tactic:
obtain ⟨t, t_comp, ht⟩ : ∃ t, IsCompact t ∧ t ∈ 𝓝 x₀ := exists_compact_mem_nhds x₀

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, nhds
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
⊢ IsCompact k'

Tactic:
have k'_comp : IsCompact k' := t_comp.smul_set k_comp.inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
hf : ContinuousOn.{u_1, u_2} (Y := E) (uncurry fun (x y : G) ↦ g (y⁻¹ * x)) (SProd.sprod (β := Set G) t univ)
hfs : ∀ (p x : G), p ∈ t → x ∉ k' → g (x⁻¹ * p) = 0
⊢ ContinuousOn.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) t

Tactic:
apply continuousOn_integral_of_compact_support k'_comp

Premises used: continuousOn_integral_of_compact_support
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
⊢ ContinuousOn.{u_1, u_2} (Y := E) (uncurry fun (x y : G) ↦ g (y⁻¹ * x)) (SProd.sprod (β := Set G) t univ)

Tactic:
(hg.comp (continuous_snd.inv.mul continuous_fst)).continuousOn

Premises used: Continuous.continuousOn, Continuous.comp, continuous_snd, continuous_fst, Continuous.mul, Continuous.inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
⊢ ContinuousOn.{u_1, u_2} (Y := E) (uncurry fun (x y : G) ↦ g (y⁻¹ * x)) (SProd.sprod (β := Set G) t univ)

Tactic:
exact (hg.comp (continuous_snd.inv.mul continuous_fst)).continuousOn

Premises used: Continuous.continuousOn, Continuous.comp, continuous_snd, continuous_fst, Continuous.mul, Continuous.inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
p x : G
hp : p ∈ t
hx : x ∉ k'
hfs : ∀ (hx : g (x⁻¹ * p) ≠ 0), x ∈ k'
⊢ g (x⁻¹ * p) = 0

Tactic:
contrapose! hx
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
p x : G
hp : p ∈ t
hx : g (x⁻¹ * p) ≠ 0
⊢ (fun (x1 x2 : G) ↦ x1 * x2) p (p⁻¹ * x) = x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.Unique
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : LocallyCompactSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace ℝ E
g : G → E
hg : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
p x : G
hp : p ∈ t
hx : g (x⁻¹ * p) ≠ 0
hfs : p⁻¹ * x ∈ k⁻¹
⊢ x ∈ k'

Tactic:
refine ⟨p, hp, p⁻¹ * x, ?_, by simp⟩