awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
k : ℕ
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hk : (↑k : ℕ∞ω) ≤ n
hx : x ∈ s
⊢ HAdd.hAdd (α := ℕ∞ω) 0 (↑k : ℕ∞ω) ≤ n

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
k : ℕ
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hk : (↑k : ℕ∞ω) ≤ n
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    (iteratedFDerivWithin 𝕜 k f s) s

Tactic:
fun _x hx ↦ hf.contDiffWithinAt hx |>.continuousWithinAt_iteratedFDerivWithin hs hk hx

Premises used: ContDiffWithinAt.continuousWithinAt_iteratedFDerivWithin, ContinuousOn, ContDiffOn.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
k : ℕ
hf : ContDiffAt 𝕜 n f x
hk : (↑k : ℕ∞ω) ≤ n
⊢ HAdd.hAdd (α := ℕ∞ω) 0 (↑k : ℕ∞ω) ≤ n

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
k : ℕ
hf : ContDiffOn 𝕜 n f s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : (↑k : ℕ∞ω) ≤ n
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k f) s

Tactic:
fun _x hx ↦ hf.contDiffAt (hs.mem_nhds hx) |>.continuousAt_iteratedFDeriv hk |>.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, IsOpen.mem_nhds, ContDiffOn.contDiffAt, ContinuousOn, ContDiffAt.continuousAt_iteratedFDeriv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : 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
inl :
  ∀ (hcg : HasCompactSupport.{uG, uE'} (α := G) (β := E') 0) (hg : ContDiff.{u𝕜, uG, uE'} 𝕜 (E := G) (F := E') 1 0),
    HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (E' := E') f 0 L μ)
      (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 0) (precompR G L) μ x₀) x₀
inr :
  ∀ (fin_dim : FiniteDimensional 𝕜 G),
    HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
      (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) (precompR G L) μ x₀) x₀
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) (precompR G L) μ x₀) x₀

Tactic:
rcases hcg.eq_zero_or_finiteDimensional 𝕜 hg.continuous with (rfl | fin_dim)

Premises used: ContDiff.continuous, HasCompactSupport.eq_zero_or_finiteDimensional, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
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
hf : LocallyIntegrable f μ
x₀ : G
hcg : HasCompactSupport.{uG, uE'} (α := G) (β := E') 0
hg : ContDiff.{u𝕜, uG, uE'} 𝕜 (E := G) (F := E') 1 0
⊢ Eq (α := (x : G) → G →L[𝕜] E') (fderiv 𝕜 0) 0

Tactic:
have : fderiv 𝕜 (0 : G → E') = 0 := fderiv_const (0 : E')
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
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
hf : LocallyIntegrable f μ
x₀ : G
hcg : HasCompactSupport.{uG, uE'} (α := G) (β := E') 0
hg : ContDiff.{u𝕜, uG, uE'} 𝕜 (E := G) (F := E') 1 0
this : Eq (α := (x : G) → G →L[𝕜] E') (fderiv 𝕜 0) 0
inl : HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) 0 0 x₀
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (E' := E') f 0 L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 0) (precompR G L) μ x₀) x₀

Tactic:
simp only [this, convolution_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, MeasureTheory.convolution_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
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
hf : LocallyIntegrable f μ
x₀ : G
hcg : HasCompactSupport.{uG, uE'} (α := G) (β := E') 0
hg : ContDiff.{u𝕜, uG, uE'} 𝕜 (E := G) (F := E') 1 0
this : Eq (α := (x : G) → G →L[𝕜] E') (fderiv 𝕜 0) 0
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) 0 0 x₀

Tactic:
hasFDerivAt_const (0 : F) x₀

Premises used: hasFDerivAt_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
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
hf : LocallyIntegrable f μ
x₀ : G
hcg : HasCompactSupport.{uG, uE'} (α := G) (β := E') 0
hg : ContDiff.{u𝕜, uG, uE'} 𝕜 (E := G) (F := E') 1 0
this : Eq (α := (x : G) → G →L[𝕜] E') (fderiv 𝕜 0) 0
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) 0 0 x₀

Tactic:
exact hasFDerivAt_const (0 : F) x₀

Premises used: hasFDerivAt_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : 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
⊢ ProperSpace G

Tactic:
have : ProperSpace G := FiniteDimensional.proper_rclike 𝕜 G
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : 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
inr :
  let L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L;
  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₀
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) (precompR G L) μ x₀) x₀

Tactic:
set L' := L.precompR G

Premises used: ContinuousLinearMap.precompR
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : 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
⊢ ∀ᶠ (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))) μ

Tactic:
have h1 : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (fun t => L (f t) (g (x - t))) μ :=
    Eventually.of_forall
      (hf.aestronglyMeasurable.convolution_integrand_snd L hg.continuous.aestronglyMeasurable)
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : 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))) μ
⊢ ∀ (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)))
      μ

Tactic:
have h2 : ∀ x, AEStronglyMeasurable (fun t => L' (f t) (fderiv 𝕜 g (x - t))) μ :=
    hf.aestronglyMeasurable.convolution_integrand_snd L'
      (hg.continuous_fderiv one_ne_zero).aestronglyMeasurable
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : 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)))
      μ
x t : G
⊢ HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x

Tactic:
simpa using
      (hg.differentiable one_ne_zero).differentiableAt.hasFDerivAt.comp x
        ((hasFDerivAt_id x).sub (hasFDerivAt_const t x))

Premises used: Differentiable.differentiableAt, HasFDerivAt.sub, hasFDerivAt_id, hasFDerivAt_const, DifferentiableAt.hasFDerivAt, ContDiff.differentiable, one_ne_zero, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : 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)))
      μ
⊢ ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x

Tactic:
have h3 : ∀ x t, HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x := fun x t ↦ by
    simpa using
      (hg.differentiable one_ne_zero).differentiableAt.hasFDerivAt.comp x
        ((hasFDerivAt_id x).sub (hasFDerivAt_const t x))
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : 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
⊢ IsCompact K'

Tactic:
have hK' : IsCompact K' := (hcg.fderiv 𝕜).isCompact.neg.add (isCompact_closedBall x₀ 1)
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : 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 → ℝ
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))) μ
⊢ 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₀

Tactic:
apply hasFDerivAt_integral_of_dominated_of_fderiv_le (ball_mem_nhds _ zero_lt_one) h1 _ (h2 x₀)

Premises used: Metric.ball_mem_nhds, zero_lt_one, hasFDerivAt_integral_of_dominated_of_fderiv_le
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : 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'
t x : G
hx : x ∈ ball x₀ 1
⊢ norm (E := G →L[𝕜] F)
      ((((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)) :
        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)) t

Tactic:
(hcg.fderiv 𝕜).convolution_integrand_bound_right L' (hg.continuous_fderiv one_ne_zero)
        (ball_subset_closedBall hx)

Premises used: Metric.ball_subset_closedBall, HasCompactSupport.fderiv, ContDiff.continuous_fderiv, one_ne_zero, HasCompactSupport.convolution_integrand_bound_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : 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
inr₁ inr₂ :
  ∀ (t x : G) (hx : x ∈ ball x₀ 1),
    norm (E := G →L[𝕜] F)
        ((((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)) :
          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)) t
⊢ ∀ᵐ (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

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)