awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
funProp₂ : map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : G) ↦ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ) μ
have funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
funProp₂ : map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : G) ↦ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ) μ
have funProp₅ : map (fun (a : G × G) ↦ a.1⁻¹ * a.2) (μ.prod μ) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
⊢ f ⋆ₘₗ[μ] g ⋆ₘₗ[μ] k = (f ⋆ₘₗ[μ] g) ⋆ₘₗ[μ] k
have h : ∀ (x : G), (f ⋆ₘₗ[μ] g ⋆ₘₗ[μ] k) x = ((f ⋆ₘₗ[μ] g) ⋆ₘₗ[μ] k) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y_1 : G) ↦ g y_1 * k (y_1⁻¹ * (y⁻¹ * x))) μ
have funProp : mG ≤ mG
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
funProp : mG ≤ mG
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y_1 : G) ↦ g y_1 * k (y_1⁻¹ * (y⁻¹ * x))) μ
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ k a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ k a0
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y_1 : G) ↦ g y_1 * k (y_1⁻¹ * (y⁻¹ * x))) μ
have funProp₂ : map (fun (a : G) ↦ a⁻¹ * (y⁻¹ * x)) μ ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
| f y * ∫⁻ (y_1 : G), g y_1 * k (y_1⁻¹ * (y⁻¹ * x)) ∂μ
have rw : ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ
Tactic: rw [← lintegral_const_mul'' _ (by fun_prop), ← lintegral_mul_left_eq_self _ y⁻¹]
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ ∫⁻ (y : G), f y * ∫⁻ (y_1 : G), g y_1 * k (y_1⁻¹ * (y⁻¹ * x)) ∂μ ∂μ =
    ∫⁻ (y : G), (∫⁻ (y_1 : G), f y_1 * g (y_1⁻¹ * y) ∂μ) * k (y⁻¹ * x) ∂μ
have h : ∫⁻ (y : G), ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ ∂μ =
  ∫⁻ (y : G), (∫⁻ (y_1 : G), f y_1 * g (y_1⁻¹ * y) ∂μ) * k (y⁻¹ * x) ∂μ
Tactic: conv in f _ * (∫⁻ _, _ ∂μ) =>
    rw [← lintegral_const_mul'' _ (by fun_prop), ← lintegral_mul_left_eq_self _ y⁻¹]
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y_1 : G) ↦ f y_1 * g (y_1⁻¹ * y)) μ
have funProp : mG ≤ mG
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
funProp : mG ≤ mG
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y_1 : G) ↦ f y_1 * g (y_1⁻¹ * y)) μ
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y_1 : G) ↦ f y_1 * g (y_1⁻¹ * y)) μ
have funProp₂ : map (fun (a : G) ↦ a⁻¹ * y) μ ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
| (∫⁻ (y_1 : G), f y_1 * g (y_1⁻¹ * y) ∂μ) * k (y⁻¹ * x)
have rw : ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ
Tactic: rw [← lintegral_mul_const'' _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ ∫⁻ (y : G), ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), (∫⁻ (y_1 : G), f y_1 * g (y_1⁻¹ * y) ∂μ) * k (y⁻¹ * x) ∂μ
have h : ∫⁻ (y : G), ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ ∂μ =
  ∫⁻ (y : G), ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ ∂μ
Tactic: conv in (∫⁻ _, _ ∂μ) * k _ =>
    rw [← lintegral_mul_const'' _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ ∫⁻ (y : G), ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ ∂μ
have h : ∫⁻ (y : G), ∫⁻ (x_1 : G), f x_1 * (g (x_1⁻¹ * y) * k ((x_1⁻¹ * y)⁻¹ * (x_1⁻¹ * x))) ∂μ ∂μ =
  ∫⁻ (y : G), ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ ∂μ
Tactic: rw [lintegral_lintegral_swap]
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
h :
  ∫⁻ (y : G), ∫⁻ (x_1 : G), f x_1 * (g (x_1⁻¹ * y) * k ((x_1⁻¹ * y)⁻¹ * (x_1⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ ∂μ
⊢ ∫⁻ (y : G), ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ ∂μ
have h₁ : AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))))
  (μ.prod μ)
Tactic: rw [lintegral_lintegral_swap]
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k (x_1⁻¹ * x))) (μ.prod μ)
have funProp : mG ≤ mG
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
funProp : mG ≤ mG
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k (x_1⁻¹ * x))) (μ.prod μ)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k (x_1⁻¹ * x))) (μ.prod μ)
have funProp₂ : map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
funProp₂ : map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k (x_1⁻¹ * x))) (μ.prod μ)
have funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
funProp₂ : map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k (x_1⁻¹ * x))) (μ.prod μ)
have funProp₅ : map (fun (a : G × G) ↦ a.1⁻¹ * a.2) (μ.prod μ) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
funProp₂ : map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
funProp₅ : map (fun (a : G × G) ↦ a.1⁻¹ * a.2) (μ.prod μ) ≪ μ
funProp₆ : mG ≤ mG
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k (x_1⁻¹ * x))) (μ.prod μ)
have funProp₇ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ k a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
funProp₂ : map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
funProp₅ : map (fun (a : G × G) ↦ a.1⁻¹ * a.2) (μ.prod μ) ≪ μ
funProp₆ : mG ≤ mG
funProp₇ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ k a0
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k (x_1⁻¹ * x))) (μ.prod μ)
have funProp₈ : map (fun (a : G × G) ↦ a.2⁻¹ * x) (μ.prod μ) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))))
    (μ.prod μ)
have simpa : AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (y x_1 : G) ↦ f y * (g (y⁻¹ * x_1) * k (x_1⁻¹ * x))) (μ.prod μ)
Tactic: simpa [mul_assoc] using by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : CommGroup G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : μ.IsInvInvariant
f g : G → ℝ≥0∞
⊢ f ⋆ₘₗ[μ] g = g ⋆ₘₗ[μ] f
have h : ∀ (x : G), (f ⋆ₘₗ[μ] g) x = (g ⋆ₘₗ[μ] f) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : CommGroup G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : μ.IsInvInvariant
f g : G → ℝ≥0∞
x : G
⊢ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ = ∫⁻ (y : G), g y * f (y⁻¹ * x) ∂μ
have h : ∫⁻ (x_1 : G), f (x * x_1⁻¹) * g ((x * x_1⁻¹)⁻¹ * x) ∂μ = ∫⁻ (y : G), g y * f (y⁻¹ * x) ∂μ
Tactic: rw [← lintegral_mul_left_eq_self _ x, ← lintegral_inv_eq_self]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
x : E
⊢ Membership.mem (γ := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) x ↔
    ∀ (t : Set E), s ⊆ t → AbsConvex 𝕜 t → x ∈ t
have simp_rw : Membership.mem (γ := Set E) (⋂ (t : Set E), ⋂ (_ : s ⊆ t), ⋂ (_ : AbsConvex 𝕜 t), t) x ↔
  ∀ (t : Set E), s ⊆ t → AbsConvex 𝕜 t → x ∈ t
Tactic: simp_rw [absConvexHull_eq_iInter, mem_iInter]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
⊢ Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ s = ∅
have mp : Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) → s = ∅
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
mp : Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) → s = ∅
⊢ Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ s = ∅
have mpr : s = ∅ → Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
h : Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E)
⊢ s = ∅
have mp : s ⊆ (absConvexHull 𝕜 : (a : Set E) → Set E) s
Tactic: rw [← Set.subset_empty_iff, ← h]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : AddCommMonoid E
inst_3 : PartialOrder 𝕜
s : Set E
⊢ Set.Nonempty.{u_2} (α := E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s) ↔ s.Nonempty
have rw : ¬Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ ¬s = ∅
Tactic: rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne, Ne]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
⊢ Filter.HasBasis (𝓝 0) (fun (s : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) s ∧ AbsConvex 𝕜 s) id
have 𝕜₁ : ∀ (s : Set E) (hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s),
  ∃ (i' : Set E), (Membership.mem (γ := Filter E) (𝓝 0) i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id s
Tactic: refine
    (LocallyConvexSpace.convex_basis_zero 𝕜 E).to_hasBasis (fun s hs => ?_) fun s hs =>
      ⟨s, ⟨hs.1, hs.2.2⟩, rfl.subset⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s
⊢ ∃ (i' : Set E), (Membership.mem (γ := Filter E) (𝓝 0) i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id s
have refine : Membership.mem (α := Set E) (γ := Filter E) (𝓝 0) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s) : Set E) ∧
  AbsConvex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))
Tactic: refine ⟨convexHull 𝕜 (balancedCore 𝕜 s), ?_, convexHull_min (balancedCore_subset s) hs.2⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s
⊢ Membership.mem (α := Set E) (γ := Filter E) (𝓝 0) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s) : Set E) ∧
    AbsConvex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))
have refine : AbsConvex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))
Tactic: refine ⟨Filter.mem_of_superset (balancedCore_mem_nhds_zero hs.1) (subset_convexHull 𝕜 _), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s
⊢ AbsConvex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))
have refine : Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))
Tactic: refine ⟨(balancedCore_balanced s).convexHull, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ZeroLEOneClass 𝕜
⊢ Filter.HasBasis (𝓝 0) (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_4] s ∧ AbsConvex 𝕜 s) id
have refine_1 : ∀ (i : Set E),
  Membership.mem (γ := Filter E) (𝓝 0) i ∧ AbsConvex 𝕜 i →
    ∃ (i' : Set E), (0 ∈ i' ∧ IsOpen[inst_4] i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id i
Tactic: refine (nhds_hasBasis_absConvex 𝕜 E).to_hasBasis ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ZeroLEOneClass 𝕜
refine_1 :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i ∧ AbsConvex 𝕜 i →
      ∃ (i' : Set E), (0 ∈ i' ∧ IsOpen[inst_4] i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id i
⊢ Filter.HasBasis (𝓝 0) (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_4] s ∧ AbsConvex 𝕜 s) id
have refine_2 : ∀ (i' : Set E),
  0 ∈ i' ∧ IsOpen[inst_4] i' ∧ AbsConvex 𝕜 i' →
    ∃ (i : Set E), (Membership.mem (γ := Filter E) (𝓝 0) i ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id i'
Tactic: refine (nhds_hasBasis_absConvex 𝕜 E).to_hasBasis ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ZeroLEOneClass 𝕜
s : Set E
hs_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
hs_balanced : Balanced 𝕜 s
hs_convex : Convex 𝕜 s
⊢ ∃ (i' : Set E), (0 ∈ i' ∧ IsOpen[inst_4] i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id s
have refine_1 : 0 ∈ interior s ∧ IsOpen[inst_4] (interior s) ∧ AbsConvex 𝕜 (interior s)
Tactic: refine ⟨interior s, ?_, interior_subset⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : E
ha : a ∈ balancedHull ℝ s
⊢ Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E) a
have obtain : ∀ (r : ℝ) (hr : ‖r‖ ≤ 1) (y : E) (hy : y ∈ s) (ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s),
  Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E) ((fun (x : E) ↦ r • x) y)
Tactic: obtain ⟨r, hr, y, hy, rfl⟩ := mem_balancedHull_iff.1 ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s
⊢ Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E) ((fun (x : E) ↦ r • x) y)
have a : (fun (x : E) ↦ r • x) y ∈ segment ℝ y (-y)
Tactic: apply segment_subset_convexHull (mem_union_left (-s) hy) (mem_union_right _ (neg_mem_neg.mpr hy))
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s
⊢ (fun (x : E) ↦ r • x) y ∈ segment ℝ y (-y)
have this : 0 ≤ 1 + r
Tactic: have : 0 ≤ 1 + r := neg_le_iff_add_nonneg'.mp (neg_le_of_abs_le hr)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s
this : 0 ≤ 1 + r
⊢ (fun (x : E) ↦ r • x) y ∈ segment ℝ y (-y)
have this₁ : 0 ≤ 1 - r
Tactic: have : 0 ≤ 1 - r := sub_nonneg.2 (le_of_abs_le hr)