awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : 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[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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : 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 : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] ((⇑isoP : (a : eP) → P) ⁻¹' s)
refine_1 :
  ∀ (p : eP) (x : eG),
    Membership.mem (γ := Set eP) ((⇑isoP : (a : eP) → P) ⁻¹' s) p → x ∉ (⇑isoG : (a : eG) → G) ⁻¹' k → eg p x = 0
refine_2 : LocallyIntegrable ef eμ
refine_3 :
  ContDiffOn 𝕜 (↑n : WithTop ℕ∞) (↿eg) (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)
⊢ ContDiffOn 𝕜 (↑n : WithTop ℕ∞) R (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)

Tactic:
refine contDiffOn_convolution_right_with_param_aux eL hes hek ?_ ?_ ?_

Premises used: MeasureTheory.contDiffOn_convolution_right_with_param_aux
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : 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[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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : 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 : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] ((⇑isoP : (a : eP) → P) ⁻¹' s)
p : eP
x : eG
hp : Membership.mem (γ := Set eP) ((⇑isoP : (a : eP) → P) ⁻¹' s) p
hx : x ∉ (⇑isoG : (a : eG) → G) ⁻¹' k
refine_1 : g ((isoP : (a : eP) → P) p) ((isoG : (a : eG) → G) x) = 0
⊢ eg p x = 0

Tactic:
simp only [eg,
        ContinuousLinearEquiv.map_eq_zero_iff]

Premises used: ContinuousLinearEquiv.map_eq_zero_iff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : 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[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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : 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 : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] ((⇑isoP : (a : eP) → P) ⁻¹' s)
p : eP
x : eG
hp : Membership.mem (γ := Set eP) ((⇑isoP : (a : eP) → P) ⁻¹' s) p
hx : x ∉ (⇑isoG : (a : eG) → G) ⁻¹' k
⊢ g ((isoP : (a : eP) → P) p) ((isoG : (a : eG) → G) x) = 0

Tactic:
hgs _ _ hp hx
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : 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[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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : 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 : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] ((⇑isoP : (a : eP) → P) ⁻¹' s)
p : eP
x : eG
hp : Membership.mem (γ := Set eP) ((⇑isoP : (a : eP) → P) ⁻¹' s) p
hx : x ∉ (⇑isoG : (a : eG) → G) ⁻¹' k
⊢ g ((isoP : (a : eP) → P) p) ((isoG : (a : eG) → G) x) = 0

Tactic:
exact hgs _ _ hp hx
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : 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[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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : 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 : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] ((⇑isoP : (a : eP) → P) ⁻¹' s)
⊢ LocallyIntegrable ef eμ

Tactic:
(locallyIntegrable_map_homeomorph isoG.symm.toHomeomorph).2 hf

Premises used: Iff.mpr, ContinuousLinearEquiv.symm, MeasureTheory.locallyIntegrable_map_homeomorph, ContinuousLinearEquiv.toHomeomorph
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : 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[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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : 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 : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] ((⇑isoP : (a : eP) → P) ⁻¹' s)
⊢ LocallyIntegrable ef eμ

Tactic:
exact (locallyIntegrable_map_homeomorph isoG.symm.toHomeomorph).2 hf
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : 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[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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : 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 : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] ((⇑isoP : (a : eP) → P) ⁻¹' s)
refine_3 :
  ContDiffOn 𝕜 (F := E') (↑n : WithTop ℕ∞)
    (fun (x : eP × eG) ↦ g ((isoP : (a : eP) → P) x.1) ((isoG : (a : eG) → G) x.2))
    (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)
⊢ ContDiffOn 𝕜 (↑n : WithTop ℕ∞) (↿eg) (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)

Tactic:
apply isoE'.symm.contDiff.comp_contDiffOn

Premises used: ContDiff.comp_contDiffOn, ContinuousLinearEquiv.symm, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : 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[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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : 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 : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] ((⇑isoP : (a : eP) → P) ⁻¹' s)
refine_3 :
  MapsTo (⇑(isoP.prodCongr isoG) : (a : eP × eG) → P × G)
    (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ) (SProd.sprod (β := Set G) s univ)
⊢ ContDiffOn 𝕜 (F := E') (↑n : WithTop ℕ∞)
    (fun (x : eP × eG) ↦ g ((isoP : (a : eP) → P) x.1) ((isoG : (a : eG) → G) x.2))
    (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)

Tactic:
apply hg.comp (isoP.prodCongr isoG).contDiff.contDiffOn

Premises used: ContDiff.contDiffOn, ContDiffOn.comp, ContinuousLinearEquiv.prodCongr, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : 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[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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : 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 : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
hek : IsCompact (X := eG) ((⇑isoG : (a : eG) → G) ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] ((⇑isoP : (a : eP) → P) ⁻¹' s)
p : eP
x : eG
hp : Membership.mem (γ := Set eP) ((⇑isoP : (a : eP) → P) ⁻¹' s) (p, x).1
⊢ Membership.mem (α := P × G) (SProd.sprod (β := Set G) s univ)
    ((isoP.prodCongr isoG : (a : eP × eG) → P × G) (p, x) : P × G)

Tactic:
simpa only [mem_preimage, ContinuousLinearEquiv.prodCongr_apply, prodMk_mem_set_prod_eq,
        mem_univ, and_true] using hp

Premises used: and_true, Set.prodMk_mem_set_prod_eq, Set.mem_univ, ContinuousLinearEquiv.prodCongr_apply, Set.mem_preimage
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedAddCommGroup P
inst_13 : 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[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 𝕜 (↑n : WithTop ℕ∞) (↿g) (SProd.sprod (β := Set G) s univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this : MeasurableSpace eG := borel eG
this_1 : 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 : (a : eG) → G)
eμ : Measure eG := Measure.map (⇑isoG.symm : (a : G) → eG) μ
eg : eP → eG → eE' :=
  fun (ep : eP) (ex : eG) ↦ (isoE'.symm : (a : E') → eE') (g ((isoP : (a : eP) → P) ep) ((isoG : (a : eG) → G) ex))
eL : E →L[𝕜] eE' →L[𝕜] eF :=
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
    (↑(ContinuousLinearEquiv.symm (isoE'.arrowCongr (𝕜 := 𝕜) (E := eE') (F := E') (G := F) (H := eF) isoF)) :
      (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF)
    L
R : (q : eP × eG) → eF := fun (q : eP × eG) ↦ convolution (𝕜 := 𝕜) ef (eg q.1) eL eμ q.2
⊢ ContDiffOn 𝕜 (↑n : WithTop ℕ∞) R (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)

Tactic:
have R_contdiff : ContDiffOn 𝕜 n R ((isoP ⁻¹' s) ×ˢ univ) := by
    have hek : IsCompact (isoG ⁻¹' k) := isoG.toHomeomorph.isClosedEmbedding.isCompact_preimage hk
    have hes : IsOpen (isoP ⁻¹' s) := isoP.continuous.isOpen_preimage _ hs
    refine contDiffOn_convolution_right_with_param_aux eL hes hek ?_ ?_ ?_
    · intro p x hp hx
      simp only [eg,
        ContinuousLinearEquiv.map_eq_zero_iff]
      exact hgs _ _ hp hx
    · exact (locallyIntegrable_map_homeomorph isoG.symm.toHomeomorph).2 hf
    · apply isoE'.symm.contDiff.comp_contDiffOn
      apply hg.comp (isoP.prodCongr isoG).contDiff.contDiffOn
      rintro ⟨p, x⟩ ⟨hp, -⟩
      simpa only [mem_preimage, ContinuousLinearEquiv.prodCongr_apply, prodMk_mem_set_prod_eq,
        mem_univ, and_true] using hp