awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : 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
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‖
⊢ ContinuousAt (f ⋆[L, μ] g) x₀
have refine_1 : ∀ᶠ (x : G) in 𝓝 x₀,
  AEStronglyMeasurable.{uG, uF} (β := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a))) μ
Tactic: refine continuousAt_of_dominated ?_ this (by fun_prop) ?_
-- 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
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‖
refine_1 :
  ∀ᶠ (x : G) in 𝓝 x₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a))) μ
⊢ ContinuousAt (f ⋆[L, μ] g) x₀
have refine_2 : ∀ᵐ (a : G) ∂μ,
  ContinuousAt.{uG, uF} (Y := F)
    (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a))) x₀
Tactic: refine continuousAt_of_dominated ?_ this (by fun_prop) ?_
-- 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
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‖
⊢ ∀ᵐ (a : G) ∂μ,
    ContinuousAt.{uG, uF} (Y := F)
      (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a))) x₀
have refine_2 : ∀ (t : G),
  ContinuousAt.{uG, uF} (Y := F)
    (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) x₀
Tactic: filter_upwards with t
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
⊢ g ⋆[L.flip, μ] f = f ⋆[L, μ] g
have h : ∀ (x : G), (g ⋆[L.flip, μ] f) x = (f ⋆[L, μ] g) x
Tactic: ext1 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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
x : G
⊢ (g ⋆[L.flip, μ] f) x = (f ⋆[L, μ] g) x
have h : Eq.{uF + 1} (α := F) (∫ (t : G), (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t)) ∂μ)
  (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)
Tactic: simp_rw [convolution_def]
-- 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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
x : G
⊢ Eq.{uF + 1} (α := F) (∫ (t : G), (((L.flip : (a : E') → E →L[𝕜] F) (g t) : E →L[𝕜] F) : (a : E) → F) (f (x - t)) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)
have h : Eq.{uF + 1} (α := F)
  (∫ (x_1 : G), (((L.flip : (a : E') → E →L[𝕜] F) (g (x - x_1)) : E →L[𝕜] F) : (a : E) → F) (f (x - (x - x_1))) ∂μ)
  (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)
Tactic: rw [← integral_sub_left_eq_self _ μ 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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
x : G
⊢ Eq.{uF + 1} (α := F)
    (∫ (x_1 : G), (((L.flip : (a : E') → E →L[𝕜] F) (g (x - x_1)) : E →L[𝕜] F) : (a : E) → F) (f (x - (x - x_1))) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)
have h : Eq.{uF + 1} (α := F)
  (∫ (x_1 : G), (((L.flip : (a : E') → E →L[𝕜] F) (g (x - x_1)) : E →L[𝕜] F) : (a : E) → F) (f x_1) ∂μ)
  (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)
Tactic: simp_rw [sub_sub_self, flip_apply]
-- 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'
x : G
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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
⊢ (f ⋆[L, μ] g) x = ∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t) ∂μ
have rw : (g ⋆[L.flip, μ] f) x = ∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f (x - t)) : E' →L[𝕜] F) : (a : E') → F) (g t) ∂μ
Tactic: rw [← convolution_flip]
-- 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'
x : G
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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
⊢ Eq.{uF + 1} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-x - t)) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f (-t)) : E' →L[𝕜] F) : (a : E') → F) (g (x + t)) ∂μ)
have h : EventuallyEq.{uG, uF} (β := F) (ae μ)
  (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (-x - a))) fun (a : G) ↦
  (((L : (a : E) → E' →L[𝕜] F) (f (-a)) : E' →L[𝕜] F) : (a : E') → F) (g (x + a))
Tactic: apply integral_congr_ae
-- 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'
x : G
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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
⊢ EventuallyEq.{uG, uF} (β := F) (ae μ)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (-x - a))) fun (a : G) ↦
    (((L : (a : E) → E' →L[𝕜] F) (f (-a)) : E' →L[𝕜] F) : (a : E') → F) (g (x + a))
have h : ∀ (t : G) (ht : f (-t) = f t) (h't : g (-(x + t)) = g (x + t)),
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-x - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f (-t)) : E' →L[𝕜] F) : (a : E') → F) (g (x + t)) : F)
Tactic: filter_upwards [h1, (eventually_add_left_iff μ x).2 h2] with t ht h't
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
t : G
ht : f (-t) = f t
h't : g (-(x + t)) = g (x + t)
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-x - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f (-t)) : E' →L[𝕜] F) : (a : E') → F) (g (x + t)) : F)
have h : Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-x - t)) : F)
  ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x + t)) : F)
Tactic: simp_rw [ht, ← h't, neg_add']
-- 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'
x : G
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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
t : G
ht : f (-t) = f t
h't : g (-(x + t)) = g (x + t)
h :
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-x - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x + t)) : F)
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-x - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f (-t)) : E' →L[𝕜] F) : (a : E') → F) (g (x + t)) : F)
have h₁ : Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-x - t)) : F)
  ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (-(x + t))) : F)
Tactic: simp_rw [ht, ← h't, neg_add']
-- 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'
x : G
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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : MeasurableNeg G
inst_13 : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
⊢ Eq.{uF + 1} (α := F) (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f (-t)) : E' →L[𝕜] F) : (a : E') → F) (g (x + t)) ∂μ)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)
have rw : Eq.{uF + 1} (α := F)
  (∫ (x_1 : G), (((L : (a : E) → E' →L[𝕜] F) (f (- -x_1)) : E' →L[𝕜] F) : (a : E') → F) (g (x + -x_1)) ∂μ)
  (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t)) ∂μ)
Tactic: rw [← integral_neg_eq_self]
-- 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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : BorelSpace G
hcf : HasCompactSupport f
hf : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : LocallyIntegrable g μ
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ⋆[L, μ] g)
have rw : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g ⋆[L.flip, μ] f)
Tactic: rw [← convolution_flip]
-- 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 : AddCommGroup G
inst_10 : μ.IsAddLeftInvariant
inst_11 : μ.IsNegInvariant
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : BorelSpace G
inst_15 : FirstCountableTopology G
inst_16 : SecondCountableTopologyEither G E
hbf : BddAbove (α := ℝ) (range fun (x : G) ↦ ‖f x‖)
hf : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Integrable g μ
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ⋆[L, μ] g)
have rw : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g ⋆[L.flip, μ] f)
Tactic: rw [← convolution_flip]
-- 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 : SeminormedAddCommGroup G
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
t : G
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
have pos : ∀ (ht : t ∈ support f),
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
Tactic: by_cases ht : t ∈ support f
-- 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 : SeminormedAddCommGroup G
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
t : G
pos :
  ∀ (ht : t ∈ support f),
    Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
      ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
have neg : ∀ (ht : t ∉ support f),
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
Tactic: by_cases ht : t ∈ support f
-- 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 : SeminormedAddCommGroup G
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
t : G
ht : t ∈ support f
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
have h2t : Membership.mem (γ := Set G) (ball 0 R) t
Tactic: have h2t := hf ht
-- 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 : SeminormedAddCommGroup G
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
t : G
ht : t ∈ support f
h2t : Membership.mem (γ := Set G) (ball 0 R) t
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
have h2t₁ : ‖t‖ < R
Tactic: rw [mem_ball_zero_iff] at h2t
Cleared hypotheses: h2t
-- 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 : SeminormedAddCommGroup G
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
have hg₁ : x₀ - t ∈ ball x₀ R → g (x₀ - t) = g x₀
Tactic: specialize hg (x₀ - t)
Cleared hypotheses: hg
-- 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 : SeminormedAddCommGroup G
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
hg : x₀ - t ∈ ball x₀ R → g (x₀ - t) = g x₀
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
have hg₁ : ‖t‖ < R → g (x₀ - t) = g x₀
Tactic: rw [sub_eq_add_neg, add_mem_ball_iff_norm, norm_neg, ← sub_eq_add_neg] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst_7 : MeasurableSpace G
μ : Measure G
inst_8 : NormedSpace ℝ F
inst_9 : SeminormedAddCommGroup G
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
hg : ‖t‖ < R → g (x₀ - t) = g x₀
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
have pos : Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
  ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
Tactic: rw [hg h2t]
-- 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 : SeminormedAddCommGroup G
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
t : G
ht : t ∉ support f
⊢ Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t)) : F)
    ((((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g x₀) : F)
have ht₁ : f t = 0
Tactic: rw [notMem_support] at ht
Cleared hypotheses: ht