awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
refine : ∀ (x₀ : G), ContinuousAt (f ⋆[L, μ] g) x₀
⊢ Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ⋆[L, μ] g)

Tactic:
refine continuous_iff_continuousAt.mpr fun x₀ => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
h :
  ∀ (x : G),
    ∀ᵐ (t : G) ∂μ,
      norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
        ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
⊢ ∀ᶠ (x : G) in 𝓝 x₀,
    ∀ᵐ (t : G) ∂μ,
      norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
        ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖

Tactic:
filter_upwards with x
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ x : G
h :
  ∀ (t : G),
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
      ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
⊢ ∀ᵐ (t : G) ∂μ,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
      ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖

Tactic:
filter_upwards with t
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ x t : G
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
    ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖

Tactic:
apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl, le_ciSup hbg (x - t)]

Premises used: le_rfl, HSub.hSub, le_ciSup, ContinuousLinearMap.le_of_opNorm₂_le_of_le
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
⊢ ∀ᶠ (x : G) in 𝓝 x₀,
    ∀ᵐ (t : G) ∂μ,
      norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
        ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖

Tactic:
have : ∀ᶠ x in 𝓝 x₀, ∀ᵐ t : G ∂μ, ‖L (f t) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖ := by
    filter_upwards with x; filter_upwards with t
    apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl, le_ciSup hbg (x - t)]
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
this :
  ∀ᶠ (x : G) in 𝓝 x₀,
    ∀ᵐ (t : G) ∂μ,
      norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
        ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
⊢ Integrable (ε := ℝ) (fun (a : G) ↦ ‖L‖ * ‖f a‖ * ⨆ (i : G), ‖g i‖) μ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
this :
  ∀ᶠ (x : G) in 𝓝 x₀,
    ∀ᵐ (t : G) ∂μ,
      norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
        ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
refine_1 :
  ∀ᶠ (x : G) in 𝓝 x₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a))) μ
refine_2 :
  ∀ᵐ (a : G) ∂μ,
    ContinuousAt.{uG, uF} (Y := F)
      (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a))) x₀
⊢ ContinuousAt (f ⋆[L, μ] g) x₀

Tactic:
refine continuousAt_of_dominated ?_ this (by fun_prop) ?_

Premises used: MeasureTheory.continuousAt_of_dominated
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
this :
  ∀ᶠ (x : G) in 𝓝 x₀,
    ∀ᵐ (t : G) ∂μ,
      norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
        ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
⊢ ∀ᶠ (x : G) in 𝓝 x₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a))) μ

Tactic:
Eventually.of_forall fun x =>
      hf.aestronglyMeasurable.convolution_integrand_snd' L hg.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd', Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
this :
  ∀ᶠ (x : G) in 𝓝 x₀,
    ∀ᵐ (t : G) ∂μ,
      norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
        ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
⊢ ∀ᶠ (x : G) in 𝓝 x₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a))) μ

Tactic:
exact Eventually.of_forall fun x =>
      hf.aestronglyMeasurable.convolution_integrand_snd' L hg.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd', Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
this :
  ∀ᶠ (x : G) in 𝓝 x₀,
    ∀ᵐ (t : G) ∂μ,
      norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
        ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
refine_2 :
  ∀ (t : G),
    ContinuousAt.{uG, uF} (Y := F)
      (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) x₀
⊢ ∀ᵐ (a : G) ∂μ,
    ContinuousAt.{uG, uF} (Y := F)
      (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a))) x₀

Tactic:
filter_upwards with t
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
this :
  ∀ᶠ (x : G) in 𝓝 x₀,
    ∀ᵐ (t : G) ∂μ,
      norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
        ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
t : G
⊢ ContinuousAt.{uG, uF} (Y := F)
    (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) x₀

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddCommGroup G
⊢ support (f ⋆[L, μ] g) ⊆ support f + support g

Tactic:
(support_convolution_subset_swap L).trans (add_comm _ _).subset

Premises used: HasSubset.Subset.trans, add_comm, Eq.subset, MeasureTheory.support_convolution_subset_swap
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
h : ∀ (x : G), (g ⋆[L.flip, μ] f) x = (f ⋆[L, μ] g) x
⊢ g ⋆[L.flip, μ] f = f ⋆[L, μ] g

Tactic:
ext1 x
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
x : G
h :
  Eq.{uF + 1} (α := F) (∫ (t : G), (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t)) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)
⊢ (g ⋆[L.flip, μ] f) x = (f ⋆[L, μ] g) x

Tactic:
simp_rw [convolution_def]

Premises used: MeasureTheory.convolution_def
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
x : G
h :
  Eq.{uF + 1} (α := F)
    (∫ (x_1 : G), (((L.flip : (a : E') → E →L[𝕜] F) (g (x - x_1)) : E →L[𝕜] F) : (a : E) → F) (f (x - (x - x_1))) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)
⊢ Eq.{uF + 1} (α := F) (∫ (t : G), (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t)) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)

Tactic:
rw [← integral_sub_left_eq_self _ μ x]

Premises used: MeasureTheory.integral_sub_left_eq_self
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
x : G
h :
  Eq.{uF + 1} (α := F)
    (∫ (x_1 : G), (((L.flip : (a : E') → E →L[𝕜] F) (g (x - x_1)) : E →L[𝕜] F) : (a : E) → F) (f x_1) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)
⊢ Eq.{uF + 1} (α := F)
    (∫ (x_1 : G), (((L.flip : (a : E') → E →L[𝕜] F) (g (x - x_1)) : E →L[𝕜] F) : (a : E) → F) (f (x - (x - x_1))) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)

Tactic:
simp_rw [sub_sub_self, flip_apply]

Premises used: ContinuousLinearMap.flip_apply, sub_sub_self
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
rw : (g ⋆[L.flip, μ] f) x = ∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t) ∂μ
⊢ (f ⋆[L, μ] g) x = ∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t) ∂μ

Tactic:
rw [← convolution_flip]

Premises used: MeasureTheory.convolution_flip
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
⊢ (g ⋆[L.flip, μ] f) x = ∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t) ∂μ

Tactic:
rfl
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
F : Type uF
inst : NormedAddCommGroup F
x : G
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 F
inst_3 : MeasurableSpace G
μ : Measure G
inst_4 : NormedSpace ℝ F
inst_5 : AddCommGroup G
inst_6 : μ.IsAddLeftInvariant
inst_7 : μ.IsNegInvariant
inst_8 : MeasurableNeg G
inst_9 : MeasurableAdd G
f : G → 𝕜
g : G → F
⊢ Eq (α := F) (convolution (𝕜 := 𝕜) f g (lsmul 𝕜 𝕜) μ x) (∫ (t : G), f (x - t) • g t ∂μ)

Tactic:
convolution_eq_swap _

Premises used: MeasureTheory.convolution_eq_swap
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
x : G
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : AddCommGroup G
inst_3 : μ.IsAddLeftInvariant
inst_4 : μ.IsNegInvariant
inst_5 : MeasurableNeg G
inst_6 : MeasurableAdd G
inst_7 : NormedSpace ℝ 𝕜
f g : G → 𝕜
⊢ Eq (α := 𝕜) (convolution (𝕜 := 𝕜) f g (mul 𝕜 𝕜) μ x) (∫ (t : G), f (x - t) * g t ∂μ)

Tactic:
convolution_eq_swap _

Premises used: MeasureTheory.convolution_eq_swap
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
h :
  EventuallyEq.{uG, uF} (β := F) (ae μ)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (-x - a))) fun (a : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f (-a)) : E' →L[𝕜] F) : (a : E') → F) (g (x + a))
⊢ Eq.{uF + 1} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-x - t)) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f (-t)) : E' →L[𝕜] F) : (a : E') → F) (g (x + t)) ∂μ)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
h :
  ∀ (t : G) (ht : f (-t) = f t) (h't : g (-(x + t)) = g (x + t)),
    Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-x - t)) : F)
      ((((L : (a : E) → E' →L[𝕜] F) (f (-t)) : E' →L[𝕜] F) : (a : E') → F) (g (x + t)) : F)
⊢ EventuallyEq.{uG, uF} (β := F) (ae μ)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (-x - a))) fun (a : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f (-a)) : E' →L[𝕜] F) : (a : E') → F) (g (x + a))

Tactic:
filter_upwards [h1, (eventually_add_left_iff μ x).2 h2] with t ht h't

Premises used: Iff.mpr, MeasureTheory.eventually_add_left_iff
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
t : G
ht : f (-t) = f t
h't : g (-(x + t)) = g (x + t)
h :
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-x - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x + t)) : F)
h₁ :
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-x - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-(x + t))) : F)
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-x - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f (-t)) : E' →L[𝕜] F) : (a : E') → F) (g (x + t)) : F)

Tactic:
simp_rw [ht, ← h't, neg_add']

Premises used: neg_add'