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 : AddGroup G
inst_8 : TopologicalSpace G
hcg : HasCompactSupport g
hg : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x t : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
refine : ∀ (i : G), ‖g i‖ ≤ ⨆ (i : G), ‖g i‖
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
    u.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖) t

Tactic:
refine convolution_integrand_bound_right_of_le_of_subset _ (fun i => ?_) hx hu

Premises used: MeasureTheory.convolution_integrand_bound_right_of_le_of_subset
-- 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 : AddGroup G
inst_8 : TopologicalSpace G
hcg : HasCompactSupport g
hg : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x t : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
i : G
⊢ ‖g i‖ ≤ ⨆ (i : G), ‖g i‖

Tactic:
le_ciSup (hg.norm.bddAbove_range_of_hasCompactSupport hcg.norm) _

Premises used: Continuous.norm, le_ciSup, HasCompactSupport.norm, Continuous.bddAbove_range_of_hasCompactSupport
-- 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 : AddGroup G
inst_8 : TopologicalSpace G
hcg : HasCompactSupport g
hg : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x t : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
i : G
⊢ ‖g i‖ ≤ ⨆ (i : G), ‖g i‖

Tactic:
exact le_ciSup (hg.norm.bddAbove_range_of_hasCompactSupport hcg.norm) _

Premises used: Continuous.norm, le_ciSup, HasCompactSupport.norm, Continuous.bddAbove_range_of_hasCompactSupport
-- 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 : AddGroup G
inst_8 : TopologicalSpace G
hcg : HasCompactSupport g
hg : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x t : G
s : Set G
hx : x ∈ s
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
    (-tsupport g + s).indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖) t

Tactic:
hcg.convolution_integrand_bound_right_of_subset L hg hx Subset.rfl

Premises used: Set.Subset.rfl, HasCompactSupport.convolution_integrand_bound_right_of_subset
-- 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 : AddGroup G
inst_8 : TopologicalSpace G
inst_9 : ContinuousSub G
hg : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
t : G
⊢ Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : G) ↦ g (x - t)

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 : AddGroup G
inst_8 : TopologicalSpace G
hcf : HasCompactSupport f
hf : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
x t : G
s : Set G
hx : x ∈ s
⊢ norm.{uF} (E := F) ((((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t)) : F) ≤
    (-tsupport f + s).indicator (fun (t : G) ↦ ‖L.flip‖ * ‖g t‖ * ⨆ (i : G), ‖f i‖) t

Tactic:
hcf.convolution_integrand_bound_right L.flip hf hx

Premises used: ContinuousLinearMap.flip, HasCompactSupport.convolution_integrand_bound_right
-- 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 : AddGroup G
inst_8 : TopologicalSpace G
hcf : HasCompactSupport f
hf : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
x t : G
s : Set G
hx : x ∈ s
h :
  Eq (α := ℝ) ((-tsupport f + s).indicator (fun (t : G) ↦ (‖L‖ * ⨆ (i : G), ‖f i‖) * ‖g t‖) t)
    ((-tsupport f + s).indicator (fun (t : G) ↦ ‖L.flip‖ * ‖g t‖ * ⨆ (i : G), ‖f i‖) t)
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t) : F) ≤
    (-tsupport f + s).indicator (fun (t : G) ↦ (‖L‖ * ⨆ (i : G), ‖f i‖) * ‖g t‖) t

Tactic:
convert! hcf.convolution_integrand_bound_right L.flip hf hx using 1

Premises used: ContinuousLinearMap.flip, HasCompactSupport.convolution_integrand_bound_right
-- 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 : AddGroup G
inst_8 : TopologicalSpace G
hcf : HasCompactSupport f
hf : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
x t : G
s : Set G
hx : x ∈ s
h :
  Eq (α := ℝ) ((-tsupport f + s).indicator (fun (t : G) ↦ (‖L‖ * ⨆ (i : G), ‖f i‖) * ‖g t‖) t)
    ((-tsupport f + s).indicator (fun (t : G) ↦ ‖L‖ * ‖g t‖ * ⨆ (i : G), ‖f i‖) t)
⊢ Eq (α := ℝ) ((-tsupport f + s).indicator (fun (t : G) ↦ (‖L‖ * ⨆ (i : G), ‖f i‖) * ‖g t‖) t)
    ((-tsupport f + s).indicator (fun (t : G) ↦ ‖L.flip‖ * ‖g t‖ * ⨆ (i : G), ‖f i‖) t)

Tactic:
simp_rw [L.opNorm_flip, mul_right_comm]

Premises used: mul_right_comm, ContinuousLinearMap.opNorm_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'
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 : Sub G
x : G
h : ConvolutionExistsAt f g x L μ
⊢ Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ

Tactic:
h

Premises used: MeasureTheory.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 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
hf : AEStronglyMeasurable f ν
hg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (p : G × G) ↦ p.1 - p.2) (μ.prod ν))
⊢ 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 ν)

Tactic:
L.aestronglyMeasurable_comp₂ hf.comp_snd <| hg.comp_measurable measurable_sub

Premises used: MeasureTheory.AEStronglyMeasurable.comp_measurable, MeasurableSub₂.measurable_sub, ContinuousLinearMap.aestronglyMeasurable_comp₂, MeasureTheory.AEStronglyMeasurable.comp_snd
-- 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
hf : AEStronglyMeasurable f μ
x : G
hg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x - t) μ)
⊢ AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ

Tactic:
L.aestronglyMeasurable_comp₂ hf <| hg.comp_measurable <| measurable_id.const_sub x

Premises used: MeasureTheory.AEStronglyMeasurable.comp_measurable, measurable_id, Measurable.const_sub, ContinuousLinearMap.aestronglyMeasurable_comp₂
-- 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
x : G
hf : AEStronglyMeasurable (m₀ := inst_7) f (Measure.map (fun (t : G) ↦ x - t) μ)
hg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t)) μ

Tactic:
L.aestronglyMeasurable_comp₂ (hf.comp_measurable <| measurable_id.const_sub x) hg

Premises used: MeasureTheory.AEStronglyMeasurable.comp_measurable, measurable_id, Measurable.const_sub, ContinuousLinearMap.aestronglyMeasurable_comp₂
-- 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ -t + x₀) ⁻¹' 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 (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
rw :
  IntegrableOn.{uG, uF} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) s μ
⊢ Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) μ

Tactic:
rw [← integrableOn_iff_integrable_of_support_subset h2s]

Premises used: MeasureTheory.integrableOn_iff_integrable_of_support_subset
-- 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' (fun (t : G) ↦ -t + x₀) ⁻¹' 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 (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
⊢ let s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s;
  BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')

Tactic:
set s' := (fun t => -t + x₀) ⁻¹' s

Premises used: HAdd.hAdd, Neg.neg
-- 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
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 (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
h :
  ∀ (a : G),
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - a)) : F) ≤
      s.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) a
⊢ ∀ᵐ (t : G) ∂μ.restrict s,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤
      s.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) t

Tactic:
filter_upwards
-- 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
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 (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
⊢ ∀ (a : G),
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - a)) : F) ≤
      s.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) a

Tactic:
le_indicator (fun t ht => ?_) fun t ht => ?_

Premises used: Set.le_indicator
-- 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
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 (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
h :
  ∀ (t : G) (ht : t ∈ s),
    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 : (↑s' : Type uG)), ‖g (↑i : G)‖
h₁ :
  ∀ (t : G) (ht : t ∉ s),
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤ 0
⊢ ∀ (a : G),
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - a)) : F) ≤
      s.indicator (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) a

Tactic:
refine le_indicator (fun t ht => ?_) fun t ht => ?_

Premises used: Set.le_indicator
-- 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
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 (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
t : G
ht : t ∈ s
h : ‖g (x₀ - t)‖ ≤ ⨆ (i : (↑s' : Type uG)), ‖g (↑i : 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 : (↑s' : Type uG)), ‖g (↑i : G)‖

Tactic:
apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl]

Premises used: le_rfl, 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 : AddGroup G
inst_9 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
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 (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
t : G
ht : t ∈ s
⊢ ‖g (x₀ - t)‖ ≤ ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖

Tactic:
(le_ciSup_set hbg <| mem_preimage.mpr ?_)

Premises used: Iff.mpr, le_ciSup_set, Set.mem_preimage
-- 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
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 (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
t : G
ht : t ∈ s
h : -(x₀ - t) + x₀ ∈ s
⊢ ‖g (x₀ - t)‖ ≤ ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖

Tactic:
refine (le_ciSup_set hbg <| mem_preimage.mpr ?_)

Premises used: Iff.mpr, le_ciSup_set, Set.mem_preimage
-- 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
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 (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
t : G
ht : t ∈ s
h : t - x₀ + x₀ ∈ s
h₁ h₂ h₃ h₄ : t ∈ s
⊢ -(x₀ - t) + x₀ ∈ s

Tactic:
rwa [neg_sub, sub_add_cancel]

Premises used: neg_sub, sub_add_cancel
-- 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
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 (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
t : G
ht : t ∉ s
⊢ t ∉
    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))

Tactic:
have : t ∉ support fun t => L (f t) (g (x₀ - t)) := mt (fun h => h2s h) ht
-- 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
s : Set G
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 (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun (t : G) ↦ -t + x₀) ⁻¹' s
hbg : BddAbove (α := ℝ) ((fun (i : G) ↦ ‖g i‖) '' s')
t : G
ht : t ∉ s
this :
  t ∉
    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))
h : norm.{uF} (E := F) 0 ≤ 0
h₁ h₂ : LE.le (α := ℝ) 0 0
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤ 0

Tactic:
rw [notMem_support.mp this, norm_zero]

Premises used: norm_zero, Function.notMem_support, Iff.mp