-- Mathlib/Analysis/Convolution.lean
theorem _root_.HasCompactSupport.hasFDerivAt_convolution_right (hcg : HasCompactSupport g)
    (hf : LocallyIntegrable f μ) (hg : ContDiff 𝕜 1 g) (x₀ : G) :
    HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[L.precompR G, μ] fderiv 𝕜 g) x₀) x₀

Proof state:
case inl
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hf : LocallyIntegrable f μ
x₀ : G
hcg : HasCompactSupport 0
hg : ContDiff 𝕜 1 0
⊢ HasFDerivAt (f ⋆[L, μ] 0) ((f ⋆[precompR G L, μ] fderiv 𝕜 0) x₀) x₀

Tactic:
have : fderiv 𝕜 (0 : G → E') = 0 := fderiv_const (0 : E')

Result:
case inl
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hf : LocallyIntegrable f μ
x₀ : G
hcg : HasCompactSupport 0
hg : ContDiff 𝕜 1 0
this : fderiv 𝕜 0 = 0
⊢ HasFDerivAt (f ⋆[L, μ] 0) ((f ⋆[precompR G L, μ] fderiv 𝕜 0) x₀) x₀

Proof state:
case inr.bound_integrable
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.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 (fun t => (L (f t)) (g (x - t))) μ
h2 : ∀ (x : G), AEStronglyMeasurable (fun t => (L' (f t)) (fderiv 𝕜 g (x - t))) μ
h3 : ∀ (x t : G), HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
⊢ Integrable
    (fun t => (-tsupport (fderiv 𝕜 g) + closedBall x₀ 1).indicator (fun t => ‖L'‖ * ‖f t‖ * ⨆ i, ‖fderiv 𝕜 g i‖) t) μ

Tactic:
rw [integrable_indicator_iff hK'.measurableSet]

Result:
case inr.bound_integrable
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.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 (fun t => (L (f t)) (g (x - t))) μ
h2 : ∀ (x : G), AEStronglyMeasurable (fun t => (L' (f t)) (fderiv 𝕜 g (x - t))) μ
h3 : ∀ (x t : G), HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
⊢ IntegrableOn (fun t => ‖L'‖ * ‖f t‖ * ⨆ i, ‖fderiv 𝕜 g i‖) K' μ

Proof state:
case inr.h_diff
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.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 (fun t => (L (f t)) (g (x - t))) μ
h2 : ∀ (x : G), AEStronglyMeasurable (fun t => (L' (f t)) (fderiv 𝕜 g (x - t))) μ
h3 : ∀ (x t : G), HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
⊢ ∀ᵐ (a : G) ∂μ, ∀ x ∈ ball x₀ 1, HasFDerivAt (fun x => (L (f a)) (g (x - a))) ((L' (f a)) (fderiv 𝕜 g (x - a))) x

Tactic:
exact Eventually.of_forall fun t x _ => (L _).hasFDerivAt.comp x (h3 x t)

Result:
no goals

Proof state:
case inl
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hf : LocallyIntegrable f μ
x₀ : G
hcg : HasCompactSupport 0
hg : ContDiff 𝕜 1 0
this : fderiv 𝕜 0 = 0
⊢ HasFDerivAt 0 0 x₀

Tactic:
exact hasFDerivAt_const (0 : F) x₀

Result:
no goals

Proof state:
case inl
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hf : LocallyIntegrable f μ
x₀ : G
hcg : HasCompactSupport 0
hg : ContDiff 𝕜 1 0
this : fderiv 𝕜 0 = 0
⊢ HasFDerivAt (f ⋆[L, μ] 0) ((f ⋆[precompR G L, μ] fderiv 𝕜 0) x₀) x₀

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

Result:
case inl
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hf : LocallyIntegrable f μ
x₀ : G
hcg : HasCompactSupport 0
hg : ContDiff 𝕜 1 0
this : fderiv 𝕜 0 = 0
⊢ HasFDerivAt 0 0 x₀