-- Mathlib/Analysis/Convolution.lean
theorem hasFDerivAt_convolution_right_with_param {g : P → G → E'} {s : Set P} {k : Set G}
    (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0)
    (hf : LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)) (q₀ : P × G)
    (hq₀ : q₀.1 ∈ s) :
    HasFDerivAt (fun q : P × G => (f ⋆[L, μ] g q.1) q.2)
      ((f ⋆[L.precompR (P × G), μ] fun x : G => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀

Proof state:
𝕜 : 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 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 (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
A : IsCompact ({q₀.1} ×ˢ k)
⊢ ∃ ε C, 0 < ε ∧ ball q₀.1 ε ⊆ s ∧ ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C

Tactic:
obtain ⟨t, kt, t_open, ht⟩ : ∃ t, {q₀.1} ×ˢ k ⊆ t ∧ IsOpen t ∧ IsBounded (g' '' t) := by
  have B : ContinuousOn g' (s ×ˢ univ) :=
    hg.continuousOn_fderiv_of_isOpen (hs.prod isOpen_univ) le_rfl
  apply exists_isOpen_isBounded_image_of_isCompact_of_continuousOn A (hs.prod isOpen_univ) _ B
  simp only [prod_subset_prod_iff, hq₀, singleton_subset_iff, subset_univ, and_self_iff,
    true_or]

Result:
case intro.intro.intro
𝕜 : 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 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 (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
A : IsCompact ({q₀.1} ×ˢ k)
t : Set (P × G)
kt : {q₀.1} ×ˢ k ⊆ t
t_open : IsOpen t
ht : Bornology.IsBounded (g' '' t)
⊢ ∃ ε C, 0 < ε ∧ ball q₀.1 ε ⊆ s ∧ ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C

Proof state:
case a.a
𝕜 : 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 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 (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)).comp (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 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 μ
a : G
x : P × G
hx : dist x q₀ < δ
⊢ (x.1, x.2 - a).1 ∈ ball q₀.1 ε

Tactic:
rw [Prod.dist_eq] at hx

Result:
case a.a
𝕜 : 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 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 (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)).comp (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 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 μ
a : G
x : P × G
hx : dist x.1 q₀.1 ⊔ dist x.2 q₀.2 < δ
⊢ (x.1, x.2 - a).1 ∈ ball q₀.1 ε