Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
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
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : 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) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : 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 → s ×ˢ univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a ↦ (L (f a)) (g x.1 (x.2 - a))) μ
I2 : Integrable (fun a ↦ (L (f a)) (g q₀.1 (q₀.2 - a))) μ
I3 : AEStronglyMeasurable (fun a ↦ L (f a) ∘SL g' (q₀.1, q₀.2 - a)) μ
K' : Set G := -k + {q₀.2}
K'_def : K' = -k + {q₀.2}
hK' : IsCompact K'
U : Set G
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
K'U : K' ⊆ U
hU : IntegrableOn f U μ
δ : ℝ
δpos : 0 < δ
δε : δ ≤ ε
hδ : K' + ball 0 δ ⊆ U
this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) := hasOpNorm
bound : G → ℝ := U.indicator fun t ↦ ‖precompR (P × G) L‖ * ‖f t‖ * C
I4 : ∀ᵐ (a : G) ∂μ, ∀ (x : P × G), dist x q₀ < δ → ‖((precompR (P × G) L) (f a)) (g' (x.1, x.2 - a))‖ ≤ bound a
I5 : Integrable bound μ
⊢ HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 ↿g (q₀.1, x)) q₀.2) q₀

Tactic:
have I6 : ∀ᵐ a : G ∂μ, ∀ x : P × G, dist x q₀ < δ →
      HasFDerivAt (fun x : P × G => L (f a) (g x.1 (x.2 - a)))
        ((L (f a)).comp (g' (x.fst, x.snd - a))) x := by
    filter_upwards with a x hx
    apply (L _).hasFDerivAt.comp x
    have N : s ×ˢ univ ∈ 𝓝 (x.1, x.2 - a) := by
      apply A'
      apply h₀ε
      rw [Prod.dist_eq] at hx
      exact lt_of_lt_of_le (lt_of_le_of_lt (le_max_left _ _) hx) δε
    have Z := ((hg.differentiableOn one_ne_zero).differentiableAt N).hasFDerivAt
    have Z' :
        HasFDerivAt (fun x : P × G => (x.1, x.2 - a)) (ContinuousLinearMap.id 𝕜 (P × G)) x := by
      have : (fun x : P × G => (x.1, x.2 - a)) = _root_.id - fun x => (0, a) := by
        ext x <;> simp only [Pi.sub_apply, _root_.id, Prod.fst_sub, sub_zero, Prod.snd_sub]
      rw [this]
      exact (hasFDerivAt_id x).sub_const (0, a)
    exact Z.comp x Z'

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
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
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : 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) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : 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 → s ×ˢ univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a ↦ (L (f a)) (g x.1 (x.2 - a))) μ
I2 : Integrable (fun a ↦ (L (f a)) (g q₀.1 (q₀.2 - a))) μ
I3 : AEStronglyMeasurable (fun a ↦ L (f a) ∘SL g' (q₀.1, q₀.2 - a)) μ
K' : Set G := -k + {q₀.2}
K'_def : K' = -k + {q₀.2}
hK' : IsCompact K'
U : Set G
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
K'U : K' ⊆ U
hU : IntegrableOn f U μ
δ : ℝ
δpos : 0 < δ
δε : δ ≤ ε
hδ : K' + ball 0 δ ⊆ U
this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) := hasOpNorm
bound : G → ℝ := U.indicator fun t ↦ ‖precompR (P × G) L‖ * ‖f t‖ * C
I4 : ∀ᵐ (a : G) ∂μ, ∀ (x : P × G), dist x q₀ < δ → ‖((precompR (P × G) L) (f a)) (g' (x.1, x.2 - a))‖ ≤ bound a
I5 : Integrable bound μ
I6 :
  ∀ᵐ (a : G) ∂μ,
    ∀ (x : P × G), dist x q₀ < δ → HasFDerivAt (fun x ↦ (L (f a)) (g x.1 (x.2 - a))) (L (f a) ∘SL g' (x.1, x.2 - a)) x
⊢ HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 ↿g (q₀.1, x)) q₀.2) q₀