awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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 𝓕))
have simp_rw : AEStronglyMeasurable (m₀ := inst_6) (g * automorphize f) (Measure.map mk (μ.restrict 𝓕))
Tactic: simp_rw [H₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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) μ
⊢ 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)
have H₂ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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
⊢ 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)
have meas_π : Measurable π
Tactic: have meas_π : Measurable π := continuous_quotient_mk'.measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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 π
⊢ 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)
have H₀ : automorphize (g ∘ π * f) = g * automorphize f
Tactic: have H₀ : QuotientAddGroup.automorphize ((g ∘ π) * f) = g * (QuotientAddGroup.automorphize f) :=
    QuotientAddGroup.automorphize_smul_left f g
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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 : G' ⧸ Γ') * f x ∂μ')
    (@integral _ _ _ _ inst_6 (Measure.map mk (μ'.restrict 𝓕')) fun (x : G' ⧸ Γ') ↦ g x * automorphize f x)
have 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)
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₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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) μ'
have this : 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_π
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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) μ'
have refine : Ne (α := ℝ≥0∞) (essSup (fun (x : G') ↦ ‖g (↑x : G' ⧸ Γ')‖ₑ) μ') ∞
Tactic: refine Integrable.essSup_smul f_ℒ_1 this ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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' ⧸ Γ')) μ'
⊢ Ne (α := ℝ≥0∞) (essSup (fun (x : G') ↦ ‖g (↑x : G' ⧸ Γ')‖ₑ) μ') ∞
have hg' : AEStronglyMeasurable (β := ℝ≥0∞) (m₀ := inst_6) (fun (x : G' ⧸ Γ') ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕'))
Tactic: have hg' : AEStronglyMeasurable (‖g ·‖ₑ) μ_𝓕 := continuous_enorm.comp_aestronglyMeasurable hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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)
have H₁ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
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 𝓕'))
have simp_rw : AEStronglyMeasurable (m₀ := inst_6) (g * automorphize f) (Measure.map mk (μ'.restrict 𝓕'))
Tactic: simp_rw [H₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
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) μ'
⊢ 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)
have H₂ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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
⊢ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ
have k_comp : IsCompact k
Tactic: have k_comp : IsCompact k := h'g
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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
⊢ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ
have apply : ∀ (x₀ : G), ContinuousAt.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀
Tactic: apply continuous_iff_continuousAt.2 (fun x₀ ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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
⊢ ContinuousAt.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀
have 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₀
Tactic: obtain ⟨t, t_comp, ht⟩ : ∃ t, IsCompact t ∧ t ∈ 𝓝 x₀ := exists_compact_mem_nhds x₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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⁻¹
⊢ ContinuousAt.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀
have k'_comp : IsCompact k'
Tactic: have k'_comp : IsCompact k' := t_comp.smul_set k_comp.inv
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) t
have hf : ContinuousOn.{u_1, u_2} (Y := E) (uncurry fun (x y : G) ↦ g (y⁻¹ * x)) (SProd.sprod (β := Set G) t univ)
Tactic: apply continuousOn_integral_of_compact_support k'_comp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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)
⊢ ContinuousOn.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) t
have hfs : ∀ (p x : G), p ∈ t → x ∉ k' → g (x⁻¹ * p) = 0
Tactic: apply continuousOn_integral_of_compact_support k'_comp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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'
⊢ g (x⁻¹ * p) = 0
have hfs : ∀ (hx : g (x⁻¹ * p) ≠ 0), x ∈ k'
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
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
⊢ x ∈ k'
have hfs : p⁻¹ * x ∈ k⁻¹
Tactic: refine ⟨p, hp, p⁻¹ * x, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
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'
⊢ ContinuousAt.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀
have A : ContinuousOn.{u_1, u_2} (Y := E) (fun (x : G) ↦ ∫ (y : G), g (y⁻¹ * x) ∂μ) t
Tactic: have A : ContinuousOn (fun (x : G) ↦ ∫ y, g (y⁻¹ * x) ∂μ) t := by
    apply continuousOn_integral_of_compact_support k'_comp
    · exact (hg.comp (continuous_snd.inv.mul continuous_fst)).continuousOn
    · intro p x hp hx
      contrapose! hx
      refine ⟨p, hp, p⁻¹ * x, ?_, by simp⟩
      simpa only [Set.mem_inv, mul_inv_rev, inv_inv] using subset_tsupport _ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ ν : Measure G
inst_5 : IsFiniteMeasureOnCompacts μ
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : μ.IsMulLeftInvariant
inst_8 : ν.IsMulRightInvariant
inst_9 : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
hg : Continuous[inst, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
⊢ ∫ (x : G), f x ∂μ = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ)
have inl : ∀ (Hf : f = 0),
  ∫ (x : G), f x ∂μ = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ)
Tactic: rcases h'f.eq_zero_or_locallyCompactSpace_of_group hf with Hf | Hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ ν : Measure G
inst_5 : IsFiniteMeasureOnCompacts μ
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : μ.IsMulLeftInvariant
inst_8 : ν.IsMulRightInvariant
inst_9 : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
hg : Continuous[inst, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
inl :
  ∀ (Hf : f = 0),
    ∫ (x : G), f x ∂μ = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ)
⊢ ∫ (x : G), f x ∂μ = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ)
have inr : ∀ (Hf : LocallyCompactSpace G),
  ∫ (x : G), f x ∂μ = HMul.hMul (α := ℝ) (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) (∫ (x : G), g x ∂μ)
Tactic: rcases h'f.eq_zero_or_locallyCompactSpace_of_group hf with Hf | Hf