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 : 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
⊢ 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)
have 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)
Tactic: simp_rw [L.opNorm_flip, mul_right_comm]
-- 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
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))
⊢ Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) μ
have 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 μ
Tactic: rw [← integrableOn_iff_integrable_of_support_subset h2s]
-- 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
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) ∂μ.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
have 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
Tactic: filter_upwards
-- 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
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
have 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)‖
Tactic: refine le_indicator (fun t ht => ?_) fun t ht => ?_
-- 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
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)‖
⊢ ∀ (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
have 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
Tactic: refine le_indicator (fun t ht => ?_) fun t ht => ?_
-- 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
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
⊢ 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)‖
have h : ‖g (x₀ - t)‖ ≤ ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖
Tactic: apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl]
-- 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
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)‖
have h : -(x₀ - t) + x₀ ∈ s
Tactic: refine (le_ciSup_set hbg <| mem_preimage.mpr ?_)
-- 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
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
⊢ -(x₀ - t) + x₀ ∈ s
have h : t - x₀ + x₀ ∈ s
Tactic: rwa [neg_sub, sub_add_cancel]
-- 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 : 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
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤ 0
have 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))
Tactic: have : t ∉ support fun t => L (f t) (g (x₀ - t)) := mt (fun h => h2s h) ht
-- 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
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))
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤ 0
have h : norm.{uF} (E := F) 0 ≤ 0
Tactic: rw [notMem_support.mp this, norm_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 : 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
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F) ≤ 0
have h₁ : LE.le (α := ℝ) 0 0
Tactic: rw [notMem_support.mp this, norm_zero]
-- 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 : 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')
⊢ 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 μ
have this : ∀ᵐ (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: have : ∀ᵐ t : G ∂μ.restrict s,
      ‖L (f t) (g (x₀ - t))‖ ≤ s.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i : s', ‖g i‖) t := by
    filter_upwards
    refine le_indicator (fun t ht => ?_) fun t ht => ?_
    · apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl]
      refine (le_ciSup_set hbg <| mem_preimage.mpr ?_)
      rwa [neg_sub, sub_add_cancel]
    · have : t ∉ support fun t => L (f t) (g (x₀ - t)) := mt (fun h => h2s h) ht
      rw [notMem_support.mp this, norm_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 : 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')
this :
  ∀ᵐ (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
⊢ 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 μ
have refine_1 : Integrable (ε := ℝ) (s.indicator fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) (μ.restrict s)
Tactic: refine Integrable.mono' ?_ ?_ this
-- 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
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')
this :
  ∀ᵐ (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
refine_1 :
  Integrable (ε := ℝ) (s.indicator fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) (μ.restrict s)
⊢ 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 μ
have refine_2 : AEStronglyMeasurable.{uG, uF} (β := F)
  (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) (μ.restrict s)
Tactic: refine Integrable.mono' ?_ ?_ this
-- 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
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')
this :
  ∀ᵐ (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
⊢ Integrable (ε := ℝ) (s.indicator fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) (μ.restrict s)
have refine_1 : IntegrableOn (ε := ℝ) (fun (t : G) ↦ ‖L‖ * ‖f t‖ * ⨆ (i : (↑s' : Type uG)), ‖g (↑i : G)‖) s (μ.restrict s)
Tactic: rw [integrable_indicator_iff hs]
-- 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
x₀ : G
h : ConvolutionExistsAt (fun (x : G) ↦ ‖f x‖) (fun (x : G) ↦ ‖g x‖) x₀ (mul ℝ ℝ) μ
hmf : AEStronglyMeasurable f μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) μ)
⊢ ConvolutionExistsAt f g x₀ L μ
have refine : ∀ (x : G),
  norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - x)) : F) ≤
    HMul.hMul (β := ℝ) ‖L‖
      (((mul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) ((fun (x : G) ↦ ‖f x‖) x) : (a : ℝ) → ℝ) ((fun (x : G) ↦ ‖g x‖) (x₀ - x)) : ℝ)
Tactic: refine (h.const_mul ‖L‖).mono'
    (hmf.convolution_integrand_snd' L hmg) (Eventually.of_forall fun 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 : MeasurableAdd G
inst_10 : MeasurableNeg G
x₀ : G
h : ConvolutionExistsAt (fun (x : G) ↦ ‖f x‖) (fun (x : G) ↦ ‖g x‖) x₀ (mul ℝ ℝ) μ
hmf : AEStronglyMeasurable f μ
hmg : AEStronglyMeasurable (m₀ := inst_7) g (Measure.map (fun (t : G) ↦ x₀ - t) μ)
x : G
⊢ norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - x)) : F) ≤
    HMul.hMul (β := ℝ) ‖L‖
      (((mul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) ((fun (x : G) ↦ ‖f x‖) x) : (a : ℝ) → ℝ) ((fun (x : G) ↦ ‖g x‖) (x₀ - x)) : ℝ)
have rw : norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - x)) : F) ≤
  ‖L‖ * (fun (x : G) ↦ ‖f x‖) x * (fun (x : G) ↦ ‖g x‖) (x₀ - x)
Tactic: rw [mul_apply', ← mul_assoc]
-- 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 : MeasurableAdd₂ G
inst_10 : MeasurableNeg G
inst_11 : SFinite μ
inst_12 : μ.IsAddRightInvariant
inst_13 : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
⊢ 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 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 ν)
Tactic: have h_meas : AEStronglyMeasurable (fun p : G × G => L (f p.2) (g (p.1 - p.2))) (μ.prod ν) :=
    hf.aestronglyMeasurable.convolution_integrand L hg.aestronglyMeasurable
-- 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 : 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 ν)
⊢ 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 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) ∂μ)
  ν
Tactic: have h2_meas : AEStronglyMeasurable (fun y : G => ∫ x : G, ‖L (f y) (g (x - y))‖ ∂μ) ν :=
    h_meas.prod_swap.norm.integral_prod_right'