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 : 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 (⇑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:
((v.continuous.measurable.measurePreserving
              (μ.restrict (tsupport fun t => L (f t) (g (x₀ - t))))).aestronglyMeasurable_comp_iff
          v.measurableEmbedding).1
      A

Premises used: Homeomorph.continuous, Homeomorph.measurableEmbedding, Measurable.measurePreserving, HSub.hSub, MeasureTheory.Measure.restrict, tsupport, MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff, Continuous.measurable, Iff.mp, DFunLike.coe
-- 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 : 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))))
h₁ : ∀ (x : G), Eq (α := G → G) (HSub.hSub (α := G) (↑((toAddUnits : (a : G) → AddUnits G) x₀) : G)) (⇑v : (a : G) → G)
⊢ 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:
convert!
    ((v.continuous.measurable.measurePreserving
              (μ.restrict (tsupport fun t => L (f t) (g (x₀ - t))))).aestronglyMeasurable_comp_iff
          v.measurableEmbedding).1
      A

Premises used: Homeomorph.continuous, Homeomorph.measurableEmbedding, Measurable.measurePreserving, HSub.hSub, MeasureTheory.Measure.restrict, tsupport, MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff, Continuous.measurable, Iff.mp, DFunLike.coe
-- 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 : 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
h₁ : ∀ (x : G), (↑((toAddUnits : (a : G) → AddUnits G) x₀) : G) - x = (v : (a : G) → G) x
⊢ Eq (α := G → G) (HSub.hSub (α := G) (↑((toAddUnits : (a : G) → AddUnits G) x₀) : G)) (⇑v : (a : G) → G)

Tactic:
ext 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 : 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_1 x : G
⊢ (↑((toAddUnits : (a : G) → AddUnits G) x₀) : G) - x = (v : (a : G) → G) x

Tactic:
simp only [v, Homeomorph.neg, sub_eq_add_neg, val_toAddUnits_apply, Homeomorph.trans_apply,
    Equiv.neg_apply, Homeomorph.homeomorph_mk_coe, Homeomorph.coe_addLeft]

Premises used: val_toAddUnits_apply, Homeomorph.homeomorph_mk_coe, Homeomorph.coe_addLeft, sub_eq_add_neg, Homeomorph.neg, Homeomorph.trans_apply, Equiv.neg_apply
-- 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 : 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 μ

Tactic:
HasCompactSupport.convolutionExistsAt L ?_ hf hg

Premises used: HasCompactSupport.convolutionExistsAt
-- 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 : 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
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))
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
refine HasCompactSupport.convolutionExistsAt L ?_ hf hg

Premises used: HasCompactSupport.convolutionExistsAt
-- 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 : 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))

Tactic:
(hcg.comp_homeomorph (Homeomorph.subLeft x₀)).mono ?_

Premises used: HasCompactSupport.comp_homeomorph, HasCompactSupport.mono, Homeomorph.subLeft
-- 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 : 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
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)))
⊢ 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 (hcg.comp_homeomorph (Homeomorph.subLeft x₀)).mono ?_

Premises used: HasCompactSupport.comp_homeomorph, HasCompactSupport.mono, Homeomorph.subLeft
-- 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 : 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)))

Tactic:
fun t => mt fun ht : g (x₀ - t) = 0 => ?_

Premises used: Set.Mem, setOf, mt, Set.Subset, Function.support, Not
-- 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 : 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
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
⊢ 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 fun t => mt fun ht : g (x₀ - t) = 0 => ?_

Premises used: mt
-- 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 : 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)
simp_rw₂ : Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) 0 : 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

Tactic:
simp_rw [ht, (L _).map_zero]

Premises used: ContinuousLinearMap.map_zero, DFunLike.coe
-- 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 : 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 μ

Tactic:
HasCompactSupport.convolutionExistsAt L ?_ hf hg

Premises used: HasCompactSupport.convolutionExistsAt
-- 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 : 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
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))
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
refine HasCompactSupport.convolutionExistsAt L ?_ hf hg

Premises used: HasCompactSupport.convolutionExistsAt
-- 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 : 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))

Tactic:
hcf.mono ?_

Premises used: HasCompactSupport.mono
-- 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 : 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
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
⊢ 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 hcf.mono ?_

Premises used: HasCompactSupport.mono
-- 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 : 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
⊢ (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:
fun t => mt fun ht : f t = 0 => ?_

Premises used: Set.Mem, setOf, mt, Set.Subset, Function.support, Not
-- 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 : 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
refine :
  ∀ (t : G) (ht : f 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
⊢ (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 fun t => mt fun ht : f t = 0 => ?_

Premises used: mt
-- 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 : 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₀ t : G
ht : f 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)
simp_rw₂ : Eq.{uF + 1} (α := F) (((L : (a : E) → E' →L[𝕜] F) 0 : (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

Tactic:
simp_rw [ht, L.map_zero₂]

Premises used: ContinuousLinearMap.map_zero₂
-- 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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd₂ G
inst_12 : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ x₀ - t) ⁻¹' s)
hs : MeasurableSet s
h2s :
  (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))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g μ
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
BddAbove.convolutionExistsAt' L ?_ hs h2s hf ?_

Premises used: BddAbove.convolutionExistsAt'
-- 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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd₂ G
inst_12 : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ x₀ - t) ⁻¹' s)
hs : MeasurableSet s
h2s :
  (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))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g μ
refine_1 : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ -t + x₀) ⁻¹' s)
refine_2 : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
refine BddAbove.convolutionExistsAt' L ?_ hs h2s hf ?_

Premises used: BddAbove.convolutionExistsAt'
-- 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 : AddCommGroup G
inst_9 : MeasurableNeg G
inst_10 : μ.IsAddLeftInvariant
inst_11 : MeasurableAdd₂ G
inst_12 : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ x₀ - t) ⁻¹' s)
hs : MeasurableSet s
h2s :
  (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))) ⊆
    s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g μ
refine_1 : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ x₀ - t) ⁻¹' s)
⊢ BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ -t + x₀) ⁻¹' s)

Tactic:
simp_rw [← sub_eq_neg_add, hbg]

Premises used: sub_eq_neg_add