-- Mathlib/Analysis/Convolution.lean
theorem contDiffOn_convolution_right_with_param {f : G → E} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F)
    {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 𝕜 n (↿g) (s ×ˢ univ)) :
    ContDiffOn 𝕜 n (fun q : P × G => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)

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
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
f : G → E
n : ℕ∞
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 𝕜 (↑n) (↿g) (s ×ˢ univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this✝¹ : MeasurableSpace eG := borel eG
this✝ : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift
isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift
isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift
ef : eG → E := f ∘ ⇑isoG
eμ : Measure eG := Measure.map (⇑isoG.symm) μ
eg : eP → eG → eE' := fun ep ex => isoE'.symm (g (isoP ep) (isoG ex))
eL : E →L[𝕜] eE' →L[𝕜] eF := (↑(isoE'.arrowCongr isoF).symm).comp L
R : eP × eG → eF := fun q => (ef ⋆[eL, eμ] eg q.1) q.2
R_contdiff : ContDiffOn 𝕜 (↑n) R ((⇑isoP ⁻¹' s) ×ˢ univ)
A : ContDiffOn 𝕜 (↑n) (⇑isoF ∘ R ∘ ⇑(isoP.prod isoG).symm) (s ×ˢ univ)
⊢ ⇑isoF ∘ R ∘ ⇑(isoP.prod isoG).symm = fun q => (f ⋆[L, μ] g q.1) q.2

Tactic:
apply funext

Result:
case h
𝕜 : 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
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
f : G → E
n : ℕ∞
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 𝕜 (↑n) (↿g) (s ×ˢ univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this✝¹ : MeasurableSpace eG := borel eG
this✝ : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift
isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift
isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift
ef : eG → E := f ∘ ⇑isoG
eμ : Measure eG := Measure.map (⇑isoG.symm) μ
eg : eP → eG → eE' := fun ep ex => isoE'.symm (g (isoP ep) (isoG ex))
eL : E →L[𝕜] eE' →L[𝕜] eF := (↑(isoE'.arrowCongr isoF).symm).comp L
R : eP × eG → eF := fun q => (ef ⋆[eL, eμ] eg q.1) q.2
R_contdiff : ContDiffOn 𝕜 (↑n) R ((⇑isoP ⁻¹' s) ×ˢ univ)
A : ContDiffOn 𝕜 (↑n) (⇑isoF ∘ R ∘ ⇑(isoP.prod isoG).symm) (s ×ˢ univ)
⊢ ∀ (x : P × G), (⇑isoF ∘ R ∘ ⇑(isoP.prod isoG).symm) x = (f ⋆[L, μ] g x.1) x.2

Proof state:
case refine_1
𝕜 : 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
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
f : G → E
n : ℕ∞
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 𝕜 (↑n) (↿g) (s ×ˢ univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this✝¹ : MeasurableSpace eG := borel eG
this✝ : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift
isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift
isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift
ef : eG → E := f ∘ ⇑isoG
eμ : Measure eG := Measure.map (⇑isoG.symm) μ
eg : eP → eG → eE' := fun ep ex => isoE'.symm (g (isoP ep) (isoG ex))
eL : E →L[𝕜] eE' →L[𝕜] eF := (↑(isoE'.arrowCongr isoF).symm).comp L
R : eP × eG → eF := fun q => (ef ⋆[eL, eμ] eg q.1) q.2
hek : IsCompact (⇑isoG ⁻¹' k)
hes : IsOpen (⇑isoP ⁻¹' s)
⊢ ∀ (p : eP) (x : eG), p ∈ ⇑isoP ⁻¹' s → x ∉ ⇑isoG ⁻¹' k → eg p x = 0

Tactic:
intro p x hp hx

Result:
case refine_1
𝕜 : 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
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
f : G → E
n : ℕ∞
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 𝕜 (↑n) (↿g) (s ×ˢ univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this✝¹ : MeasurableSpace eG := borel eG
this✝ : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift
isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift
isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift
ef : eG → E := f ∘ ⇑isoG
eμ : Measure eG := Measure.map (⇑isoG.symm) μ
eg : eP → eG → eE' := fun ep ex => isoE'.symm (g (isoP ep) (isoG ex))
eL : E →L[𝕜] eE' →L[𝕜] eF := (↑(isoE'.arrowCongr isoF).symm).comp L
R : eP × eG → eF := fun q => (ef ⋆[eL, eμ] eg q.1) q.2
hek : IsCompact (⇑isoG ⁻¹' k)
hes : IsOpen (⇑isoP ⁻¹' s)
p : eP
x : eG
hp : p ∈ ⇑isoP ⁻¹' s
hx : x ∉ ⇑isoG ⁻¹' k
⊢ eg p x = 0