awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
inst_13 : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas :
  AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)
h2_meas :
  AEStronglyMeasurable (β := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
    ν
⊢ Integrable.{uF, uG} (ε := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)
have simp_rw : (∀ᵐ (y : G) ∂ν,
    Integrable.{uF, uG} (ε := F)
      (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y))) μ) ∧
  Integrable (ε := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
    ν
Tactic: simp_rw [integrable_prod_iff' h_meas]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
inst_13 : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas :
  AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)
h2_meas :
  AEStronglyMeasurable (β := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
    ν
⊢ (∀ᵐ (y : G) ∂ν,
      Integrable.{uF, uG} (ε := F)
        (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y))) μ) ∧
    Integrable (ε := ℝ)
      (fun (y : G) ↦
        ∫ (x : G),
          Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
      ν
have refine : Integrable (ε := ℝ)
  (fun (y : G) ↦
    ∫ (x : G),
      Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
  ν
Tactic: refine ⟨Eventually.of_forall fun t => (L (f t)).integrable_comp (hg.comp_sub_right t), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
inst_13 : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas :
  AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)
h2_meas :
  AEStronglyMeasurable (β := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
    ν
⊢ Integrable (ε := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
    ν
have refine_1 : Integrable (ε := ℝ) (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ) ν
Tactic: refine Integrable.mono' ?_ h2_meas
      (Eventually.of_forall fun t => (?_ : _ ≤ ‖L‖ * ‖f t‖ * ∫ x, ‖g (x - t)‖ ∂μ))
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
inst_13 : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas :
  AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)
h2_meas :
  AEStronglyMeasurable (β := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
    ν
refine_1 : Integrable (ε := ℝ) (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ) ν
⊢ Integrable (ε := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
    ν
have refine_2 : ∀ (t : G),
  Norm.norm (E := ℝ)
      (∫ (x : G),
        Norm.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‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ
Tactic: refine Integrable.mono' ?_ h2_meas
      (Eventually.of_forall fun t => (?_ : _ ≤ ‖L‖ * ‖f t‖ * ∫ x, ‖g (x - t)‖ ∂μ))
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
inst_13 : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas :
  AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)
h2_meas :
  AEStronglyMeasurable (β := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
    ν
⊢ Integrable (ε := ℝ) (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ) ν
have refine_1 : Integrable (ε := ℝ) (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g x‖ ∂μ) ν
Tactic: simp only [integral_sub_right_eq_self (‖g ·‖)]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
inst_13 : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas :
  AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)
h2_meas :
  AEStronglyMeasurable (β := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
    ν
t : G
⊢ Norm.norm (E := ℝ)
      (∫ (x : G),
        Norm.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‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ
have refine_2 : Norm.norm (E := ℝ)
    (∫ (x : G),
      Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ∂μ) ≤
  ∫ (a : G), ‖L‖ * ‖f t‖ * ‖g (a - t)‖ ∂μ
Tactic: simp_rw [← integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
inst_13 : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas :
  AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (p : G × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f p.2) : E' →L[𝕜] F) : (a : E') → F) (g (p.1 - p.2))) (μ.prod ν)
h2_meas :
  AEStronglyMeasurable (β := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) : F) ∂μ)
    ν
t : G
⊢ Norm.norm (E := ℝ)
      (∫ (x : G),
        Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ∂μ) ≤
    ∫ (a : G), ‖L‖ * ‖f t‖ * ‖g (a - t)‖ ∂μ
have refine_2 : LE.le (α := ℝ)
  (∫ (x : G),
    Norm.norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ∂μ)
  (∫ (a : G), ‖L‖ * ‖f t‖ * ‖g (a - t)‖ ∂μ)
Tactic: rw [Real.norm_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
x₀ : G
h :
  HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
u : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addRight x₀)
v : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addLeft x₀)
⊢ ConvolutionExistsAt f g x₀ L μ
have apply : AEStronglyMeasurable (m₀ := inst_7) g
  (Measure.map (fun (t : G) ↦ (↑((toAddUnits : (a : G) → AddUnits G) x₀) : G) - t)
    (μ.restrict
      (tsupport.{uG, uF} (α := F) fun (t : G) ↦
        (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)))))
Tactic: apply ((u.isCompact_preimage.mpr h).bddAbove_image hg.norm.continuousOn).convolutionExistsAt' L
    isClosed_closure.measurableSet subset_closure (hf.integrableOn_isCompact h)
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
x₀ : G
h :
  HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
u : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addRight x₀)
v : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addLeft x₀)
⊢ AEStronglyMeasurable (g ∘ (⇑v : (a : G) → G))
    (μ.restrict
      (tsupport.{uG, uF} (α := F) fun (t : G) ↦
        (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))))
have apply : MeasurableSet.{uG} (α := G)
  (tsupport.{uG, uF} (α := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)))
Tactic: apply (hg.comp v.continuous).continuousOn.aestronglyMeasurable_of_isCompact h
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
x₀ : G
h :
  HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
u : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addRight x₀)
v : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addLeft x₀)
⊢ AEStronglyMeasurable (m₀ := inst_7) g
    (Measure.map (fun (t : G) ↦ (↑((toAddUnits : (a : G) → AddUnits G) x₀) : G) - t)
      (μ.restrict
        (tsupport.{uG, uF} (α := F) fun (t : G) ↦
          (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)))))
have A : AEStronglyMeasurable (g ∘ (⇑v : (a : G) → G))
  (μ.restrict
    (tsupport.{uG, uF} (α := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))))
Tactic: have A : AEStronglyMeasurable (g ∘ v)
      (μ.restrict (tsupport fun t : G => L (f t) (g (x₀ - t)))) := by
    apply (hg.comp v.continuous).continuousOn.aestronglyMeasurable_of_isCompact h
    exact (isClosed_tsupport _).measurableSet
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
x₀ : G
h :
  HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
u : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addRight x₀)
v : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addLeft x₀)
A :
  AEStronglyMeasurable (g ∘ (⇑v : (a : G) → G))
    (μ.restrict
      (tsupport.{uG, uF} (α := F) fun (t : G) ↦
        (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))))
⊢ AEStronglyMeasurable (m₀ := inst_7) g
    (Measure.map (fun (t : G) ↦ (↑((toAddUnits : (a : G) → AddUnits G) x₀) : G) - t)
      (μ.restrict
        (tsupport.{uG, uF} (α := F) fun (t : G) ↦
          (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)))))
have h₁ : ∀ (x : G), Eq (α := G → G) (HSub.hSub (α := G) (↑((toAddUnits : (a : G) → AddUnits G) x₀) : G)) (⇑v : (a : G) → G)
Tactic: convert!
    ((v.continuous.measurable.measurePreserving
              (μ.restrict (tsupport fun t => L (f t) (g (x₀ - t))))).aestronglyMeasurable_comp_iff
          v.measurableEmbedding).1
      A
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
x₀ : G
h :
  HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
u : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addRight x₀)
v : G ≃ₜ G := Homeomorph.trans (Homeomorph.neg G) (Homeomorph.addLeft x₀)
A :
  AEStronglyMeasurable (g ∘ (⇑v : (a : G) → G))
    (μ.restrict
      (tsupport.{uG, uF} (α := F) fun (t : G) ↦
        (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))))
x : G
⊢ Eq (α := G → G) (HSub.hSub (α := G) (↑((toAddUnits : (a : G) → AddUnits G) x₀) : G)) (⇑v : (a : G) → G)
have h₁ : ∀ (x : G), (↑((toAddUnits : (a : G) → AddUnits G) x₀) : G) - x = (v : (a : G) → G) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
⊢ ConvolutionExistsAt f g x₀ L μ
have refine : HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
  (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
Tactic: refine HasCompactSupport.convolutionExistsAt L ?_ hf hg
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
⊢ HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
have refine : Subset (α := Set G)
  (support.{uG, uF} (M := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)))
  (support (g ∘ (⇑(Homeomorph.subLeft x₀) : (a : G) → G)))
Tactic: refine (hcg.comp_homeomorph (Homeomorph.subLeft x₀)).mono ?_
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
⊢ Subset (α := Set G)
    (support.{uG, uF} (M := F) fun (t : G) ↦
      (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)))
    (support (g ∘ (⇑(Homeomorph.subLeft x₀) : (a : G) → G)))
have refine : ∀ (t : G) (ht : g (x₀ - t) = 0),
  Eq.{uF + 1} (α := F)
    ((fun (t : G) ↦ ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)) t) 0
Tactic: refine fun t => mt fun ht : g (x₀ - t) = 0 => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ t : G
ht : g (x₀ - t) = 0
simp_rw simp_rw₁ :
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) (0 : F)
⊢ Eq.{uF + 1} (α := F)
    ((fun (t : G) ↦ ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)) t) 0
have simp_rw₂ : Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) 0 : F) (0 : F)
Tactic: simp_rw [ht, (L _).map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
hcf : HasCompactSupport f
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
⊢ ConvolutionExistsAt f g x₀ L μ
have refine : HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
  (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
Tactic: refine HasCompactSupport.convolutionExistsAt L ?_ hf hg
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
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 : AddGroup G
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup G
inst_11 : BorelSpace G
hcf : HasCompactSupport f
hf : LocallyIntegrable f μ
hg : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
⊢ HasCompactSupport.{uG, uF} (β := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))
have refine : (support.{uG, uF} (M := F) fun (t : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) ⊆
  support f
Tactic: refine hcf.mono ?_