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 ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable (_m := inst_6) g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
⊢ @essSup _ _ _ inst_6 g (map QuotientGroup.mk (μ.restrict 𝓕)) = essSup (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ
have rw : essSup (g ∘ QuotientGroup.mk) (μ.restrict 𝓕) = essSup (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ
Tactic: rw [essSup_map_measure g_ae_measurable hπ.aemeasurable]
-- 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 ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable (_m := inst_6) g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
⊢ essSup (g ∘ QuotientGroup.mk) (μ.restrict 𝓕) = essSup (fun (x : G) ↦ g (↑x : G ⧸ Γ)) μ
have refine : ∀ (γ : ↥Γ.op) (x : G), (g ∘ QuotientGroup.mk) (γ • x) = (g ∘ QuotientGroup.mk) x
Tactic: refine h𝓕.essSup_measure_restrict ?_
-- 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 ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable (_m := inst_6) g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
γ : Gᵐᵒᵖ
hγ : γ ∈ Γ.op
x : G
⊢ (g ∘ QuotientGroup.mk) (Subtype.mk (p := fun (x : Gᵐᵒᵖ) ↦ x ∈ Γ.op) γ hγ • x) = (g ∘ QuotientGroup.mk) x
have dsimp : g (↑(x * MulOpposite.unop γ) : G ⧸ Γ) = g (↑x : G ⧸ Γ)
Tactic: dsimp
-- 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 ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable (_m := inst_6) g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
γ : Gᵐᵒᵖ
hγ : γ ∈ Γ.op
x : G
⊢ g (↑(x * MulOpposite.unop γ) : G ⧸ Γ) = g (↑x : G ⧸ Γ)
have e_a : Eq (α := G ⧸ Γ) (↑(x * MulOpposite.unop γ) : G ⧸ Γ) (↑x : G ⧸ Γ)
Tactic: congr 1
-- 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 ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
⊢ AbsolutelyContinuous (_m0 := inst_6) (map π μ) (map π (μ.restrict 𝓕))
have meas_π : Measurable π
Tactic: have meas_π : Measurable π := continuous_quotient_mk'.measurable
-- 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 ⧸ Γ)
inst_8 : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
⊢ AbsolutelyContinuous (_m0 := inst_6) (map π μ) (map π (μ.restrict 𝓕))
have h : ∀ ⦃s : Set (G ⧸ Γ)⦄,
  MeasurableSet s →
    Eq (α := ℝ≥0∞) (((map π (μ.restrict 𝓕) : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) (((map π μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply AbsolutelyContinuous.mk
-- 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 ⧸ Γ)
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∞)
⊢ Eq (α := ℝ≥0∞) (((map π μ : Measure (G ⧸ Γ)) : (a : Set (G ⧸ Γ)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have h : ∀ (hs : Eq (α := ℝ≥0∞) ((μ.restrict 𝓕 : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [map_apply meas_π s_meas] at hs ⊢
Cleared hypotheses: hs
-- 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 ⧸ Γ)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have h : ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s ∩ 𝓕) : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply] at hs
Cleared hypotheses: hs
-- 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 ⧸ Γ)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have h₁ : MeasurableSet (π ⁻¹' s)
Tactic: rw [Measure.restrict_apply] at hs
-- 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 ⧸ Γ)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (π ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have apply : ∀ (g : ↥Γ.op), g • π ⁻¹' s = π ⁻¹' s
Tactic: apply h𝓕.measure_zero_of_invariant _ _ hs
-- 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 ⧸ Γ)
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
⊢ γ • π ⁻¹' s = π ⁻¹' s
have h : ∀ (g : G), g ∈ γ • π ⁻¹' s ↔ g ∈ π ⁻¹' s
Tactic: ext g
-- 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 ⧸ Γ)
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 ∈ γ • π ⁻¹' s ↔ g ∈ π ⁻¹' s
have h : π (γ⁻¹ • g) ∈ s ↔ π g ∈ s
Tactic: rw [Set.mem_smul_set_iff_inv_smul_mem, mem_preimage, mem_preimage]
-- 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 ⧸ Γ)
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) ∈ s ↔ π g ∈ s
have h : π (γ⁻¹ • g) = π g
Tactic: congr! 1
-- 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 ⧸ Γ)
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 ∂μ)
    (@integral _ _ _ _ inst_6 (Measure.map mk (μ.restrict 𝓕)) fun (x : G ⧸ Γ) ↦ automorphize f x)
have calc : Eq.{u_2 + 1} (α := E) (∑' (γ : ↥Γ.op), ∫ (x : G) in 𝓕, f (γ • x) ∂μ) (∫ (x : G) in 𝓕, ∑' (γ : ↥Γ.op), 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
-- 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 ⧸ Γ)
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) ∂μ)
have hf : ∀ (i : ↥Γ.op), AEStronglyMeasurable.{u_1, u_2} (β := E) (fun (x : G) ↦ f (i • x)) (μ.restrict 𝓕)
Tactic: rw [integral_tsum]
-- 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 ⧸ Γ)
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 𝓕)
⊢ Eq.{u_2 + 1} (α := E) (∑' (γ : ↥Γ.op), ∫ (x : G) in 𝓕, f (γ • x) ∂μ) (∫ (x : G) in 𝓕, ∑' (γ : ↥Γ.op), f (γ • x) ∂μ)
have hf' : Ne (α := ℝ≥0∞) (∑' (i : ↥Γ.op), ∫⁻ (a : G) in 𝓕, ‖f (i • a)‖ₑ ∂μ) ∞
Tactic: rw [integral_tsum]
-- 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 ⧸ Γ)
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 𝓕))
⊢ Ne (α := ℝ≥0∞) (∑' (i : ↥Γ.op), ∫⁻ (a : G) in 𝓕, ‖f (i • a)‖ₑ ∂μ) ∞
have hf' : ∫⁻ (x : G), ‖f x‖ₑ ∂μ ≠ ∞
Tactic: rw [← h𝓕.lintegral_eq_tsum'' (‖f ·‖ₑ)]
-- 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
⊢ 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 : 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 π
⊢ 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₀ : QuotientGroup.automorphize ((g ∘ π) * f) = g * (QuotientGroup.automorphize f) := by
    exact QuotientGroup.automorphize_smul_left f g
-- 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
⊢ 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 ⧸ Γ), QuotientGroup.automorphize ((g ∘ π) * f) x ∂μ_𝓕 := ?_
    _ = ∫ (x : G ⧸ Γ), g x * (QuotientGroup.automorphize f x) ∂μ_𝓕 := by simp [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
⊢ 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 : 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) μ
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 : 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 ⧸ Γ)) μ
⊢ 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 : 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)
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_quotientGroup_mk h𝓕 hg'.aemeasurable]
    exact g_ℒ_infinity