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
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
⊢ ContinuousWithinAt (Y := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (SProd.sprod (β := Set G) s univ) (q₀, x₀)
have neg : ∀ (t : Set G) (t_comp : IsCompact t) (ht : t ∈ 𝓝 x₀),
  ContinuousWithinAt (Y := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (SProd.sprod (β := Set G) s univ) (q₀, x₀)
Tactic: obtain ⟨t, t_comp, ht⟩ : ∃ t, IsCompact t ∧ t ∈ 𝓝 x₀ := exists_compact_mem_nhds x₀
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
⊢ ContinuousWithinAt (Y := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (SProd.sprod (β := Set G) s univ) (q₀, x₀)
have k'_comp : IsCompact k'
Tactic: have k'_comp : IsCompact k' := IsCompact.vadd_set hk.neg t_comp
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
⊢ uncurry g' = uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)
have h : ∀ (y : (P × G) × G), uncurry g' y = (uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
⊢ ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
have this₁ : uncurry g' = uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)
Tactic: have : g'.uncurry = g.uncurry ∘ (fun w ↦ (w.1.1, w.1.2 - w.2)) := by ext y; 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
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0
this_1 : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
this : uncurry g' = uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)
⊢ ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
have rw : ContinuousOn (uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)) (SProd.sprod (β := Set G) s' univ)
Tactic: rw [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
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0
this_1 : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
this : uncurry g' = uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)
⊢ ContinuousOn (uncurry g ∘ fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)) (SProd.sprod (β := Set G) s' univ)
have refine : MapsTo (fun (w : (P × G) × G) ↦ (w.1.1, w.1.2 - w.2)) (SProd.sprod (β := Set G) s' univ)
  (SProd.sprod (β := Set G) s univ)
Tactic: refine hg.comp (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
⊢ ContinuousWithinAt (Y := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (SProd.sprod (β := Set G) s univ) (q₀, x₀)
have A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
Tactic: have A : ContinuousOn g'.uncurry (s' ×ˢ univ) := by
    have : g'.uncurry = g.uncurry ∘ (fun w ↦ (w.1.1, w.1.2 - w.2)) := by ext y; rfl
    rw [this]
    refine hg.comp (by fun_prop) ?_
    simp +contextual [s', MapsTo]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
⊢ ContinuousOn (Y := F)
    (fun (a : P × G) ↦ ∫ (x : G), (((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g' a x) ∂μ) s'
have apply : ∀ (p : P × G) (x : G), p ∈ s' → x ∉ k' → g' p x = 0
Tactic: apply continuousOn_integral_bilinear_of_locally_integrable_of_compact_support L k'_comp A _
      (hf.integrableOn_isCompact k'_comp)
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
p : P
x y : G
hp : (p, x).1 ∈ s
hx : (p, x).2 ∈ t
hy : y ∉ k'
⊢ g' (p, x) y = 0
have apply : (p, x).2 - y ∉ k
Tactic: apply hgs p _ hp
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
p : P
x y : G
hp : (p, x).1 ∈ s
hx : (p, x).2 ∈ t
hy : y ∉ k'
⊢ (p, x).2 - y ∉ k
have contrapose : ∀ (hy : (p, x).2 - y ∈ k), y ∈ k'
Tactic: contrapose hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
⊢ ContinuousWithinAt (Y := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (SProd.sprod (β := Set G) s univ) (q₀, x₀)
have B : ContinuousOn (Y := F)
  (fun (a : P × G) ↦ ∫ (x : G), (((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g' a x) ∂μ) s'
Tactic: have B : ContinuousOn (fun a ↦ ∫ x, L (f x) (g' a x) ∂μ) s' := by
    apply continuousOn_integral_bilinear_of_locally_integrable_of_compact_support L k'_comp A _
      (hf.integrableOn_isCompact k'_comp)
    rintro ⟨p, x⟩ y ⟨hp, hx⟩ hy
    apply hgs p _ hp
    contrapose hy
    exact ⟨y - x, by simpa using hy, x, hx, by simp⟩
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
H : ∃ p ∈ s, ∃ (x : G), g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun (p : P × G) (x : G) ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (SProd.sprod (β := Set G) s' univ)
B :
  ContinuousOn (Y := F)
    (fun (a : P × G) ↦ ∫ (x : G), (((L : (a : E) → E' →L[𝕜] F) (f x) : E' →L[𝕜] F) : (a : E') → F) (g' a x) ∂μ) s'
⊢ ContinuousWithinAt (Y := F) (fun (q : P × G) ↦ (f ⋆[L, μ] g q.1) q.2) (SProd.sprod (β := Set G) s univ) (q₀, x₀)
have neg : s' ∈ 𝓝[SProd.sprod (β := Set G) s univ] (q₀, x₀)
Tactic: apply ContinuousWithinAt.mono_of_mem_nhdsWithin (B (q₀, x₀) ⟨hq₀, mem_of_mem_nhds 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
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : TopologicalSpace P
s : Set P
v : P → G
hv : ContinuousOn v s
g : P → G → E'
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (SProd.sprod (β := Set G) s univ)
⊢ ContinuousOn.{uP, uF} (Y := F) (fun (x : P) ↦ (f ⋆[L, μ] g x) (v x)) s
have L₁ : MapsTo (fun (x : P) ↦ (id x, v x)) s (SProd.sprod (β := Set G) s univ)
Tactic: apply
    (continuousOn_convolution_right_with_param L hk hgs hf hg).comp (continuousOn_id.prodMk hv)
-- 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 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
⊢ Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ⋆[L, μ] g)
have rw : ContinuousOn (f ⋆[L, μ] g) univ
Tactic: rw [← continuousOn_univ]
-- 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 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g' : G → G → E' := fun (x q : G) ↦ g q
⊢ ContinuousOn (f ⋆[L, μ] g) univ
have this : ContinuousOn (↿g') (SProd.sprod (α := Set G) (β := Set G) univ univ)
Tactic: have : ContinuousOn ↿g' (univ ×ˢ univ) := (hg.comp continuous_snd).continuousOn
-- 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 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
⊢ Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ⋆[L, μ] g)
have refine : ∀ (x₀ : G), ContinuousAt (f ⋆[L, μ] g) x₀
Tactic: refine continuous_iff_continuousAt.mpr 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 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
⊢ ∀ᶠ (x : G) in 𝓝 x₀,
    ∀ᵐ (t : G) ∂μ,
      norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
        ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
have h : ∀ (x : G),
  ∀ᵐ (t : G) ∂μ,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
      ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
Tactic: filter_upwards with 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 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ x : G
⊢ ∀ᵐ (t : G) ∂μ,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
      ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
have h : ∀ (t : G),
  norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
    ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
Tactic: filter_upwards with t
-- 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 : NormedSpace ℝ F
inst_9 : AddGroup G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : BorelSpace G
inst_13 : FirstCountableTopology G
inst_14 : SecondCountableTopologyEither G E'
hbg : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
⊢ ContinuousAt (f ⋆[L, μ] g) x₀
have this : ∀ᶠ (x : G) in 𝓝 x₀,
  ∀ᵐ (t : G) ∂μ,
    norm.{uF} (E := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) : F) ≤
      ‖L‖ * ‖f t‖ * ⨆ (i : G), ‖g i‖
Tactic: have : ∀ᶠ x in 𝓝 x₀, ∀ᵐ t : G ∂μ, ‖L (f t) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖ := by
    filter_upwards with x; filter_upwards with t
    apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl, le_ciSup hbg (x - t)]