awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.IsAddLeftInvariant
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 1 g
x₀ : G
fin_dim : FiniteDimensional 𝕜 G
this : ProperSpace G
L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L
h1 :
  ∀ᶠ (x : G) in 𝓝 x₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
h2 :
  ∀ (x : G),
    AEStronglyMeasurable (β := G →L[𝕜] F)
      (fun (t : G) ↦
        (((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f t) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - t)))
      μ
h3 : ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
inr :
  ∀ᵐ (a : G) ∂μ,
    ∀ x ∈ ball x₀ 1,
      norm (E := G →L[𝕜] F)
          ((((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f a) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
                (a : G →L[𝕜] E') → G →L[𝕜] F)
              (fderiv 𝕜 g (x - a)) :
            G →L[𝕜] F) ≤
        (-tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1).indicator
          (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) a
inr₁ :
  Integrable (ε := ℝ)
    (fun (t : G) ↦
      (-tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1).indicator
        (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) t)
    μ
inr₂ :
  ∀ᵐ (a : G) ∂μ,
    ∀ x ∈ ball x₀ 1,
      HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F)
        (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a)))
        ((((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f a) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - a)))
        x
apply : G → ℝ
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) L' μ x₀) x₀
have apply₁ : 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: apply hasFDerivAt_integral_of_dominated_of_fderiv_le (ball_mem_nhds _ zero_lt_one) h1 _ (h2 x₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.IsAddLeftInvariant
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 1 g
x₀ : G
fin_dim : FiniteDimensional 𝕜 G
this : ProperSpace G
L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L
h1 :
  ∀ᶠ (x : G) in 𝓝 x₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
h2 :
  ∀ (x : G),
    AEStronglyMeasurable (β := G →L[𝕜] F)
      (fun (t : G) ↦
        (((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f t) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - t)))
      μ
h3 : ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
⊢ ∀ᵐ (a : G) ∂μ,
    ∀ x ∈ ball x₀ 1,
      norm (E := G →L[𝕜] F)
          ((((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f a) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
                (a : G →L[𝕜] E') → G →L[𝕜] F)
              (fderiv 𝕜 g (x - a)) :
            G →L[𝕜] F) ≤
        (-tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1).indicator
          (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) a
have inr : ∀ (a : G),
  Membership.mem (γ := Set G)
    {x : G |
      (fun (a : G) ↦
          ∀ x ∈ ball x₀ 1,
            norm (E := G →L[𝕜] F)
                ((((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f a) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
                      (a : G →L[𝕜] E') → G →L[𝕜] F)
                    (fderiv 𝕜 g (x - a)) :
                  G →L[𝕜] F) ≤
              (-tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1).indicator
                (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) a)
        x}
    a
Tactic: filter_upwards with t x hx using
      (hcg.fderiv 𝕜).convolution_integrand_bound_right L' (hg.continuous_fderiv one_ne_zero)
        (ball_subset_closedBall hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.IsAddLeftInvariant
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 1 g
x₀ : G
fin_dim : FiniteDimensional 𝕜 G
this : ProperSpace G
L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L
h1 :
  ∀ᶠ (x : G) in 𝓝 x₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
h2 :
  ∀ (x : G),
    AEStronglyMeasurable (β := G →L[𝕜] F)
      (fun (t : G) ↦
        (((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f t) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - t)))
      μ
h3 : ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
inr :
  ∀ (a : G),
    Membership.mem (γ := Set G)
      {x : G |
        (fun (a : G) ↦
            ∀ x ∈ ball x₀ 1,
              norm (E := G →L[𝕜] F)
                  ((((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f a) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
                        (a : G →L[𝕜] E') → G →L[𝕜] F)
                      (fderiv 𝕜 g (x - a)) :
                    G →L[𝕜] F) ≤
                (-tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1).indicator
                  (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) a)
          x}
      a
⊢ ∀ᵐ (a : G) ∂μ,
    ∀ x ∈ ball x₀ 1,
      norm (E := G →L[𝕜] F)
          ((((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f a) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
                (a : G →L[𝕜] E') → G →L[𝕜] F)
              (fderiv 𝕜 g (x - a)) :
            G →L[𝕜] F) ≤
        (-tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1).indicator
          (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) a
have inr₁ : ∀ (a x : G),
  x ∈ ball x₀ 1 →
    norm (E := G →L[𝕜] F)
        ((((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f a) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
              (a : G →L[𝕜] E') → G →L[𝕜] F)
            (fderiv 𝕜 g (x - a)) :
          G →L[𝕜] F) ≤
      (-tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1).indicator
        (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) a
Tactic: filter_upwards with t x hx using
      (hcg.fderiv 𝕜).convolution_integrand_bound_right L' (hg.continuous_fderiv one_ne_zero)
        (ball_subset_closedBall hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.IsAddLeftInvariant
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 1 g
x₀ : G
fin_dim : FiniteDimensional 𝕜 G
this : ProperSpace G
L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L
h1 :
  ∀ᶠ (x : G) in 𝓝 x₀,
    AEStronglyMeasurable.{uG, uF} (β := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
h2 :
  ∀ (x : G),
    AEStronglyMeasurable (β := G →L[𝕜] F)
      (fun (t : G) ↦
        (((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f t) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - t)))
      μ
h3 : ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
⊢ Integrable (ε := ℝ)
    (fun (t : G) ↦
      (-tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1).indicator
        (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) t)
    μ
have inr : IntegrableOn (ε := ℝ) (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) K' μ
Tactic: rw [integrable_indicator_iff hK'.measurableSet]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.IsAddLeftInvariant
inst_14 : μ.IsNegInvariant
hcf : HasCompactSupport f
hf : ContDiff 𝕜 1 f
hg : LocallyIntegrable g μ
x₀ : G
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E := G →L[𝕜] E) (fderiv 𝕜 f) g (precompL G L) μ x₀) x₀
have simp : HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE', uE, uF} (𝕜 := 𝕜) g f L.flip μ)
  (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E) g (fderiv 𝕜 f) (ContinuousLinearMap.flip (precompL G L)) μ x₀) x₀
Tactic: simp +singlePass only [← convolution_flip]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
Goal:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst_8 : μ.IsAddLeftInvariant
inst_9 : SFinite μ
hf : LocallyIntegrable f₀ μ
hcg : HasCompactSupport g₀
hg : ContDiff 𝕜 1 g₀
x₀ : 𝕜
⊢ HasDerivAt.{u𝕜, uF} (F := F) (convolution (𝕜 := 𝕜) f₀ g₀ L μ) (convolution (𝕜 := 𝕜) f₀ (deriv g₀) L μ x₀) x₀
have h : Eq.{uF + 1} (α := F) (convolution (𝕜 := 𝕜) f₀ (deriv g₀) L μ x₀ : F)
  ((convolution (𝕜 := 𝕜) (E' := 𝕜 →L[𝕜] E') f₀ (fderiv 𝕜 g₀) (precompR 𝕜 L) μ x₀ : (a : 𝕜) → F) 1 : F)
Tactic: convert! (hcg.hasFDerivAt_convolution_right L hf hg x₀).hasDerivAt using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
Goal:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst_8 : μ.IsAddLeftInvariant
inst_9 : SFinite μ
hf : LocallyIntegrable f₀ μ
hcg : HasCompactSupport g₀
hg : ContDiff 𝕜 1 g₀
x₀ : 𝕜
⊢ Eq.{uF + 1} (α := F) (convolution (𝕜 := 𝕜) f₀ (deriv g₀) L μ x₀ : F)
    ((convolution (𝕜 := 𝕜) (E' := 𝕜 →L[𝕜] E') f₀ (fderiv 𝕜 g₀) (precompR 𝕜 L) μ x₀ : (a : 𝕜) → F) 1 : F)
have h : Eq.{uF + 1} (α := F) (convolution (𝕜 := 𝕜) f₀ (deriv g₀) L μ x₀)
  (convolution.{u𝕜, u𝕜, uE, uE', uF} (𝕜 := 𝕜) (E' := E') f₀
    (fun (a : 𝕜) ↦ ((fderiv 𝕜 g₀ a : 𝕜 →L[𝕜] E') : (a : 𝕜) → E') 1) L μ x₀)
Tactic: rw [convolution_precompR_apply L hf (hcg.fderiv 𝕜) (hg.continuous_fderiv one_ne_zero)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
Goal:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst_8 : μ.IsAddLeftInvariant
inst_9 : SFinite μ
inst_10 : μ.IsNegInvariant
hcf : HasCompactSupport f₀
hf : ContDiff 𝕜 1 f₀
hg : LocallyIntegrable g₀ μ
x₀ : 𝕜
⊢ HasDerivAt.{u𝕜, uF} (F := F) (convolution (𝕜 := 𝕜) f₀ g₀ L μ) (convolution (𝕜 := 𝕜) (deriv f₀) g₀ L μ x₀) x₀
have simp : HasDerivAt.{u𝕜, uF} (F := F) (convolution (𝕜 := 𝕜) g₀ f₀ L.flip μ) (convolution (𝕜 := 𝕜) g₀ (deriv f₀) L.flip μ x₀) x₀
Tactic: simp +singlePass only [← convolution_flip]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
p : P
hp : p ∈ s
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (g p)
have refine : ∀ (x : G), (p, x) ∈ SProd.sprod (β := Set G) s univ
Tactic: refine hg.continuousOn.comp_continuous (.prodMk_right _) fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
⊢ HasFDerivAt (𝕜 := 𝕜) (F := F) (fun (q : P × G) ↦ convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f (g q.1) L μ q.2)
    (convolution (𝕜 := 𝕜) (E' := P × G →L[𝕜] E') f (fun (x : G) ↦ fderiv 𝕜 ↿g (q₀.1, x)) (precompR (P × G) L) μ q₀.2) q₀
have A : ∀ p ∈ s,
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (g p)
Tactic: have A : ∀ p ∈ s, Continuous (g p) := fun p hp ↦ by
    refine hg.continuousOn.comp_continuous (.prodMk_right _) fun x => ?_
    simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using hp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
q : P × G
hq : q.1 ∈ s
⊢ SProd.sprod (β := Set G) s univ ∈ 𝓝 q
have apply : q ∈ SProd.sprod (β := Set G) s univ
Tactic: apply (hs.prod isOpen_univ).mem_nhds
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
⊢ HasFDerivAt (𝕜 := 𝕜) (F := F) (fun (q : P × G) ↦ convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f (g q.1) L μ q.2)
    (convolution (𝕜 := 𝕜) (E' := P × G →L[𝕜] E') f (fun (x : G) ↦ fderiv 𝕜 ↿g (q₀.1, x)) (precompR (P × G) L) μ q₀.2) q₀
have A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
Tactic: have A' : ∀ q : P × G, q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q := fun q hq ↦ by
    apply (hs.prod isOpen_univ).mem_nhds
    simpa only [mem_prod, mem_univ, and_true] using hq
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
p : P
x : G
hp : p ∈ s
hx : x ∉ k
⊢ g' (p, x) = 0
have refine : ↿g =ᶠ[𝓝 (p, x)] fun (x : P × G) ↦ 0
Tactic: refine (hasFDerivAt_zero_of_eventually_const 0 ?_).fderiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
p : P
x : G
hp : p ∈ s
hx : x ∉ k
⊢ ↿g =ᶠ[𝓝 (p, x)] fun (x : P × G) ↦ 0
have M2 : kᶜ ∈ 𝓝 x
Tactic: have M2 : kᶜ ∈ 𝓝 x := hk.isClosed.isOpen_compl.mem_nhds hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.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 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) s univ ∈ 𝓝 q
p : P
x : G
hp : p ∈ s
hx : x ∉ k
M2 : kᶜ ∈ 𝓝 x
⊢ ↿g =ᶠ[𝓝 (p, x)] fun (x : P × G) ↦ 0
have M1 : s ∈ 𝓝 p
Tactic: have M1 : s ∈ 𝓝 p := hs.mem_nhds hp