awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding (β := G) fun (x : G) ↦ x * g
rw : Eq.{u_5 + 1} (α := E) (@integral _ _ _ _ inst (map (fun (x : G) ↦ x * g) μ) fun (y : G) ↦ f y) (∫ (x : G), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x * g) ∂μ) (∫ (x : G), f x ∂μ)
have rw₁ : Eq.{u_5 + 1} (α := E) (∫ (y : G), f y ∂μ) (∫ (x : G), f x ∂μ)
Tactic: rw [← h_mul.integral_map, map_mul_right_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
f : G → E
g : G
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x / g) ∂μ) (∫ (x : G), f x ∂μ)
have simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x * g⁻¹) ∂μ) (∫ (x : G), f x ∂μ)
Tactic: simp_rw [div_eq_mul_inv, integral_mul_right_eq_self f g⁻¹]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (hypothesis)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) 0
have this : IsAddTorsionFree E
Tactic: have : IsAddTorsionFree E := .of_isTorsionFree ℝ E
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
this : IsAddTorsionFree E
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) 0
have simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (-∫ (x : G), f x ∂μ)
Tactic: simp_rw [← self_eq_neg, ← integral_neg, ← hf', integral_mul_left_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
this : IsAddTorsionFree E
simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (-∫ (x : G), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) 0
have simp_rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (∫ (a : G), -f a ∂μ)
Tactic: simp_rw [← self_eq_neg, ← integral_neg, ← hf', integral_mul_left_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
this : IsAddTorsionFree E
simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (-∫ (x : G), f x ∂μ)
simp_rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (∫ (a : G), -f a ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) 0
have simp_rw₂ : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (∫ (a : G), f (g * a) ∂μ)
Tactic: simp_rw [← self_eq_neg, ← integral_neg, ← hf', integral_mul_left_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (hypothesis)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
hf' : ∀ (x : G), f (x * g) = -f x
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) 0
have this : IsAddTorsionFree E
Tactic: have : IsAddTorsionFree E := .of_isTorsionFree ℝ E
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
hf' : ∀ (x : G), f (x * g) = -f x
this : IsAddTorsionFree E
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) 0
have simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (-∫ (x : G), f x ∂μ)
Tactic: simp_rw [← self_eq_neg, ← integral_neg, ← hf', integral_mul_right_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
hf' : ∀ (x : G), f (x * g) = -f x
this : IsAddTorsionFree E
simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (-∫ (x : G), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) 0
have simp_rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (∫ (a : G), -f a ∂μ)
Tactic: simp_rw [← self_eq_neg, ← integral_neg, ← hf', integral_mul_right_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
hf' : ∀ (x : G), f (x * g) = -f x
this : IsAddTorsionFree E
simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (-∫ (x : G), f x ∂μ)
simp_rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (∫ (a : G), -f a ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) 0
have simp_rw₂ : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (∫ (a : G), f (a * g) ∂μ)
Tactic: simp_rw [← self_eq_neg, ← integral_neg, ← hf', integral_mul_right_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
f : G → F
inst_4 : μ.IsMulRightInvariant
hf : Integrable f μ
g : G
⊢ Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (t / g)) μ
have simp_rw : Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (t * g⁻¹)) μ
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
f : G → F
inst_5 : μ.IsInvInvariant
inst_6 : μ.IsMulLeftInvariant
g : G
⊢ Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g / t)) μ ↔ Integrable f μ
have refine : ∀ (h : Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g / t)) μ), Integrable f μ
Tactic: refine ⟨fun h => ?_, fun h => h.comp_div_left g⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
f : G → F
inst_5 : μ.IsInvInvariant
inst_6 : μ.IsMulLeftInvariant
g : G
h : Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g / t)) μ
⊢ Integrable f μ
have h₁ : ∀ (x : G), x = g / (g⁻¹ * x)⁻¹
Tactic: convert! h.comp_inv.comp_mul_left g⁻¹
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
f : G → F
inst_5 : μ.IsInvInvariant
inst_6 : μ.IsMulLeftInvariant
g : G
h : Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g / t)) μ
x : G
⊢ x = g / (g⁻¹ * x)⁻¹
have h₁ : x = g * (g⁻¹ * x)
Tactic: simp_rw [div_inv_eq_mul, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : MeasurableInv G
f : G → E
μ : Measure G
inst_6 : μ.IsInvInvariant
inst_7 : μ.IsMulLeftInvariant
x' : G
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x' / x) ∂μ) (∫ (x : G), f x ∂μ)
have simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x' * x⁻¹) ∂μ) (∫ (x : G), f x ∂μ)
Tactic: simp_rw [div_eq_mul_inv, integral_inv_eq_self (fun x => f (x' * x)) μ,
    integral_mul_left_eq_self f x']
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : MeasurableInv G
f : G → E
μ : Measure G
inst_6 : μ.IsInvInvariant
inst_7 : μ.IsMulLeftInvariant
x' : G
simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x' * x⁻¹) ∂μ) (∫ (x : G), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x' / x) ∂μ) (∫ (x : G), f x ∂μ)
have simp_rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x' * x) ∂μ) (∫ (x : G), f x ∂μ)
Tactic: simp_rw [div_eq_mul_inv, integral_inv_eq_self (fun x => f (x' * x)) μ,
    integral_mul_left_eq_self f x']
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (hypothesis)
Goal:
α : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
G : Type u_7
inst_2 : Group G
inst_3 : MeasurableSpace α
inst_4 : MulAction G α
inst_5 : MeasurableConstSMul G α
μ : Measure α
inst_6 : SMulInvariantMeasure G α μ
f : α → E
g : G
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α), f (g • x) ∂μ) (∫ (x : α), f x ∂μ)
have h : MeasurableEmbedding (β := α) fun (x : α) ↦ g • x
Tactic: have h : MeasurableEmbedding fun x : α => g • x := (MeasurableEquiv.smul g).measurableEmbedding
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
α : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
G : Type u_7
inst_2 : Group G
inst_3 : MeasurableSpace α
inst_4 : MulAction G α
inst_5 : MeasurableConstSMul G α
μ : Measure α
inst_6 : SMulInvariantMeasure G α μ
f : α → E
g : G
h : MeasurableEmbedding (β := α) fun (x : α) ↦ g • x
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α), f (g • x) ∂μ) (∫ (x : α), f x ∂μ)
have rw : Eq.{u_5 + 1} (α := E) (@integral _ _ _ _ inst_3 (map (fun (x : α) ↦ g • x) μ) fun (y : α) ↦ f y) (∫ (x : α), f x ∂μ)
Tactic: rw [← h.integral_map, MeasureTheory.map_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
α : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
G : Type u_7
inst_2 : Group G
inst_3 : MeasurableSpace α
inst_4 : MulAction G α
inst_5 : MeasurableConstSMul G α
μ : Measure α
inst_6 : SMulInvariantMeasure G α μ
f : α → E
g : G
h : MeasurableEmbedding (β := α) fun (x : α) ↦ g • x
rw :
  Eq.{u_5 + 1} (α := E) (@integral _ _ _ _ inst_3 (map (fun (x : α) ↦ g • x) μ) fun (y : α) ↦ f y) (∫ (x : α), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α), f (g • x) ∂μ) (∫ (x : α), f x ∂μ)
have rw₁ : Eq.{u_5 + 1} (α := E) (∫ (y : α), f y ∂μ) (∫ (x : α), f x ∂μ)
Tactic: rw [← h.integral_map, MeasureTheory.map_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.IntegralConvolution (goal)
Goal:
M : Type u_1
F : Type u_2
inst : Monoid M
mM : MeasurableSpace M
inst_1 : MeasurableMul₂ M
inst_2 : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst_3 : NormedSpace ℝ F
inst_4 : SFinite μ
inst_5 : SFinite ν
hf : Integrable f (μ ∗ₘ ν)
⊢ Eq.{u_2 + 1} (α := F) (@integral _ _ _ _ mM (Measure.map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν)) fun (x : M) ↦ f x)
    (∫ (x : M), ∫ (y : M), f (x * y) ∂ν ∂μ)
have hf₁ : Integrable.{u_2, u_1} (ε := F) (fun (x : M × M) ↦ f (x.1 * x.2)) (μ.prod ν)
Tactic: rw [integral_map (by fun_prop) hf.1, integral_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.LIntegral (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulLeftInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ
have h : μ = map (⇑(MeasurableEquiv.mulLeft g) : (a : G) → G) μ
Tactic: convert! (lintegral_map_equiv f <| MeasurableEquiv.mulLeft g).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.LIntegral (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x * g) ∂μ = ∫⁻ (x : G), f x ∂μ
have h : ∫⁻ (x : G), f x ∂μ = ∫⁻ (a : G), f a ∂map (⇑(MeasurableEquiv.mulRight g) : (a : G) → G) μ
Tactic: convert! (lintegral_map_equiv f <| MeasurableEquiv.mulRight g).symm using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.LIntegral (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ
have simp_rw : ∫⁻ (x : G), f (x * g⁻¹) ∂μ = ∫⁻ (x : G), f x ∂μ
Tactic: simp_rw [div_eq_mul_inv, lintegral_mul_right_eq_self f g⁻¹]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.LIntegral (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulLeftInvariant
inst_4 : MeasurableInv G
inst_5 : μ.IsInvInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (g / x) ∂μ = ∫⁻ (x : G), f x ∂μ
have simp_rw : ∫⁻ (x : G), f (g * x⁻¹) ∂μ = ∫⁻ (x : G), f x ∂μ
Tactic: simp_rw [div_eq_mul_inv, lintegral_inv_eq_self (f <| g * ·), lintegral_mul_left_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.LIntegral (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulLeftInvariant
inst_4 : MeasurableInv G
inst_5 : μ.IsInvInvariant
f : G → ℝ≥0∞
g : G
simp_rw : ∫⁻ (x : G), f (g * x⁻¹) ∂μ = ∫⁻ (x : G), f x ∂μ
⊢ ∫⁻ (x : G), f (g / x) ∂μ = ∫⁻ (x : G), f x ∂μ
have simp_rw₁ : ∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ
Tactic: simp_rw [div_eq_mul_inv, lintegral_inv_eq_self (f <| g * ·), lintegral_mul_left_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.LIntegral (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : TopologicalSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : μ.IsMulLeftInvariant
inst_6 : μ.Regular
inst_7 : NeZero μ
f : G → ℝ≥0∞
hf : Continuous f
⊢ ∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0
have rw : f =ᶠ[ae μ] 0 ↔ f = 0
Tactic: rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.LIntegral (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : TopologicalSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : μ.IsMulLeftInvariant
inst_6 : μ.Regular
inst_7 : NeZero μ
f : G → ℝ≥0∞
hf : Continuous f
rw : f =ᶠ[ae μ] 0 ↔ f = 0
⊢ ∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0
have rw₁ : f = 0 ↔ f = 0
Tactic: rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Mul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
c : ℝ≥0∞
g : G
⊢ Measure.map (fun (x : G) ↦ g * x) (c • μ) = c • μ
have rw : HSMul.hSMul (β := Measure G) c (Measure.map (fun (x : G) ↦ g * x) μ) = c • μ
Tactic: rw [Measure.map_smul, map_mul_left_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Mul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
c : ℝ≥0∞
g : G
rw : HSMul.hSMul (β := Measure G) c (Measure.map (fun (x : G) ↦ g * x) μ) = c • μ
⊢ Measure.map (fun (x : G) ↦ g * x) (c • μ) = c • μ
have rw₁ : c • μ = c • μ
Tactic: rw [Measure.map_smul, map_mul_left_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Mul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
c : ℝ≥0∞
g : G
⊢ Measure.map (fun (x : G) ↦ x * g) (c • μ) = c • μ
have rw : HSMul.hSMul (β := Measure G) c (Measure.map (fun (x : G) ↦ x * g) μ) = c • μ
Tactic: rw [Measure.map_smul, map_mul_right_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Mul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
c : ℝ≥0∞
g : G
rw : HSMul.hSMul (β := Measure G) c (Measure.map (fun (x : G) ↦ x * g) μ) = c • μ
⊢ Measure.map (fun (x : G) ↦ x * g) (c • μ) = c • μ
have rw₁ : c • μ = c • μ
Tactic: rw [Measure.map_smul, map_mul_right_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    μ.IsMulLeftInvariant
have trans : (∀ (g : G) (A : Set G),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
        ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
  ∀ (g : G), Measure.map (fun (x : G) ↦ g * x) μ = μ
Tactic: trans ∀ g, map (g * ·) μ = μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
trans :
  (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G), Measure.map (fun (x : G) ↦ g * x) μ = μ
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    μ.IsMulLeftInvariant
have trans₁ : (∀ (g : G), Measure.map (fun (x : G) ↦ g * x) μ = μ) ↔ μ.IsMulLeftInvariant
Tactic: trans ∀ g, map (g * ·) μ = μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G), Measure.map (fun (x : G) ↦ g * x) μ = μ
have simp_rw : (∀ (g : G) (A : Set G),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
        ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
  ∀ (g : G) (s : Set G),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ g * x) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
        ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [Measure.ext_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G) (s : Set G),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ g * x) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have refine : ∀ (g : G) (A : Set G) (hA : MeasurableSet A),
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ g * x) μ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
      ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: refine forall_congr' fun g => forall_congr' fun A => forall_congr' fun hA => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
g : G
A : Set G
hA : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ g * x) μ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
      ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [map_apply (measurable_const_mul g) hA]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    μ.IsMulRightInvariant
have trans : (∀ (g : G) (A : Set G),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
        ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
  ∀ (g : G), Measure.map (fun (x : G) ↦ x * g) μ = μ
Tactic: trans ∀ g, map (· * g) μ = μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
trans :
  (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G), Measure.map (fun (x : G) ↦ x * g) μ = μ
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    μ.IsMulRightInvariant
have trans₁ : (∀ (g : G), Measure.map (fun (x : G) ↦ x * g) μ = μ) ↔ μ.IsMulRightInvariant
Tactic: trans ∀ g, map (· * g) μ = μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G), Measure.map (fun (x : G) ↦ x * g) μ = μ
have simp_rw : (∀ (g : G) (A : Set G),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
        ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
  ∀ (g : G) (s : Set G),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
        ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [Measure.ext_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G) (s : Set G),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have refine : ∀ (g : G) (A : Set G) (hA : MeasurableSet A),
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
      ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: refine forall_congr' fun g => forall_congr' fun A => forall_congr' fun hA => ?_