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
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.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.{uG, uF} (β := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
h2 :
  ∀ (x : G),
    AEStronglyMeasurable (β := G →L[𝕜] F)
      (fun (t : G) ↦
        (((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f t) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - t)))
      μ
h3 : ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
inr : IntegrableOn (ε := ℝ) (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) K' μ
⊢ Integrable (ε := ℝ)
    (fun (t : G) ↦
      (-tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1).indicator
        (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) t)
    μ

Tactic:
rw [integrable_indicator_iff hK'.measurableSet]

Premises used: MeasureTheory.integrable_indicator_iff, IsCompact.measurableSet
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.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.{uG, uF} (β := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
h2 :
  ∀ (x : G),
    AEStronglyMeasurable (β := G →L[𝕜] F)
      (fun (t : G) ↦
        (((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f t) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - t)))
      μ
h3 : ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
⊢ IntegrableOn (ε := ℝ) (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) K' μ

Tactic:
((hf.integrableOn_isCompact hK').norm.const_mul _).mul_const _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.IntegrableOn, MeasureTheory.LocallyIntegrable.integrableOn_isCompact, MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.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.{uG, uF} (β := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
h2 :
  ∀ (x : G),
    AEStronglyMeasurable (β := G →L[𝕜] F)
      (fun (t : G) ↦
        (((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f t) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - t)))
      μ
h3 : ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
⊢ IntegrableOn (ε := ℝ) (fun (t : G) ↦ ‖L'‖ * ‖f t‖ * ⨆ (i : G), norm (E := G →L[𝕜] E') (fderiv 𝕜 g i)) K' μ

Tactic:
exact ((hf.integrableOn_isCompact hK').norm.const_mul _).mul_const _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.LocallyIntegrable.integrableOn_isCompact, MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.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.{uG, uF} (β := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
h2 :
  ∀ (x : G),
    AEStronglyMeasurable (β := G →L[𝕜] F)
      (fun (t : G) ↦
        (((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f t) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - t)))
      μ
h3 : ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
⊢ ∀ᵐ (a : G) ∂μ,
    ∀ x ∈ ball x₀ 1,
      HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F)
        (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a)))
        ((((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f a) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - a)))
        x

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

Premises used: ContinuousLinearMap.hasFDerivAt, Filter.Eventually.of_forall, DFunLike.coe, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.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.{uG, uF} (β := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
h2 :
  ∀ (x : G),
    AEStronglyMeasurable (β := G →L[𝕜] F)
      (fun (t : G) ↦
        (((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f t) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - t)))
      μ
h3 : ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
⊢ ∀ᵐ (a : G) ∂μ,
    ∀ x ∈ ball x₀ 1,
      HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F)
        (fun (x : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g (x - a)))
        ((((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f a) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - a)))
        x

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

Premises used: ContinuousLinearMap.hasFDerivAt, Filter.Eventually.of_forall, DFunLike.coe, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.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.{uG, uF} (β := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
h2 :
  ∀ (x : G),
    AEStronglyMeasurable (β := G →L[𝕜] F)
      (fun (t : G) ↦
        (((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f t) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - t)))
      μ
h3 : ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
⊢ Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) μ

Tactic:
hcg.convolutionExists_right L hf hg.continuous x₀

Premises used: ContDiff.continuous, HasCompactSupport.convolutionExists_right, MeasureTheory.ConvolutionExistsAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.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.{uG, uF} (β := F)
      (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) μ
h2 :
  ∀ (x : G),
    AEStronglyMeasurable (β := G →L[𝕜] F)
      (fun (t : G) ↦
        (((L' : (a : E) → (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) (f t) : (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F) :
            (a : G →L[𝕜] E') → G →L[𝕜] F)
          (fderiv 𝕜 g (x - t)))
      μ
h3 : ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (α := G →L[𝕜] E') (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
⊢ Integrable.{uF, uG} (ε := F)
    (fun (t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x₀ - t))) μ

Tactic:
exact hcg.convolutionExists_right L hf hg.continuous x₀

Premises used: ContDiff.continuous, HasCompactSupport.convolutionExists_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.IsAddLeftInvariant
inst_14 : μ.IsNegInvariant
hcf : HasCompactSupport f
hf : ContDiff 𝕜 1 f
hg : LocallyIntegrable g μ
x₀ : G
simp :
  HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE', uE, uF} (𝕜 := 𝕜) g f L.flip μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E) g (fderiv 𝕜 f) (ContinuousLinearMap.flip (precompL G L)) μ x₀) x₀
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E := G →L[𝕜] E) (fderiv 𝕜 f) g (precompL G L) μ x₀) x₀

Tactic:
simp +singlePass only [← convolution_flip]

Premises used: MeasureTheory.convolution_flip
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.IsAddLeftInvariant
inst_14 : μ.IsNegInvariant
hcf : HasCompactSupport f
hf : ContDiff 𝕜 1 f
hg : LocallyIntegrable g μ
x₀ : G
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE', uE, uF} (𝕜 := 𝕜) g f L.flip μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E) g (fderiv 𝕜 f) (ContinuousLinearMap.flip (precompL G L)) μ x₀) x₀

Tactic:
hcf.hasFDerivAt_convolution_right L.flip hg hf x₀

Premises used: ContinuousLinearMap.comp, LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, HasCompactSupport.hasFDerivAt_convolution_right, LinearMap.mkContinuousOfExistsBound₂, ContinuousLinearMap.flip, ContinuousLinearMap.precompR
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
inst_12 : SFinite μ
inst_13 : μ.IsAddLeftInvariant
inst_14 : μ.IsNegInvariant
hcf : HasCompactSupport f
hf : ContDiff 𝕜 1 f
hg : LocallyIntegrable g μ
x₀ : G
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE', uE, uF} (𝕜 := 𝕜) g f L.flip μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E) g (fderiv 𝕜 f) (ContinuousLinearMap.flip (precompL G L)) μ x₀) x₀

Tactic:
exact hcf.hasFDerivAt_convolution_right L.flip hg hf x₀

Premises used: HasCompactSupport.hasFDerivAt_convolution_right, ContinuousLinearMap.flip
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
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
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst_8 : μ.IsAddLeftInvariant
inst_9 : SFinite μ
hf : LocallyIntegrable f₀ μ
hcg : HasCompactSupport g₀
hg : ContDiff 𝕜 1 g₀
x₀ : 𝕜
⊢ HasDerivAt.{u𝕜, uF} (F := F) (convolution (𝕜 := 𝕜) f₀ g₀ L μ : 𝕜 → F)
    ((convolution (𝕜 := 𝕜) (E' := 𝕜 →L[𝕜] E') f₀ (fderiv 𝕜 g₀) (precompR 𝕜 L) μ x₀ : (a : 𝕜) → F) 1 : F) x₀

Tactic:
(hcg.hasFDerivAt_convolution_right L hf hg x₀).hasDerivAt

Premises used: HasCompactSupport.hasFDerivAt_convolution_right, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
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
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst_8 : μ.IsAddLeftInvariant
inst_9 : SFinite μ
hf : LocallyIntegrable f₀ μ
hcg : HasCompactSupport g₀
hg : ContDiff 𝕜 1 g₀
x₀ : 𝕜
h :
  Eq.{uF + 1} (α := F) (convolution (𝕜 := 𝕜) f₀ (deriv g₀) L μ x₀ : F)
    ((convolution (𝕜 := 𝕜) (E' := 𝕜 →L[𝕜] E') f₀ (fderiv 𝕜 g₀) (precompR 𝕜 L) μ x₀ : (a : 𝕜) → F) 1 : F)
⊢ HasDerivAt.{u𝕜, uF} (F := F) (convolution (𝕜 := 𝕜) f₀ g₀ L μ) (convolution (𝕜 := 𝕜) f₀ (deriv g₀) L μ x₀) x₀

Tactic:
convert! (hcg.hasFDerivAt_convolution_right L hf hg x₀).hasDerivAt using 1

Premises used: HasCompactSupport.hasFDerivAt_convolution_right, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
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
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst_8 : μ.IsAddLeftInvariant
inst_9 : SFinite μ
hf : LocallyIntegrable f₀ μ
hcg : HasCompactSupport g₀
hg : ContDiff 𝕜 1 g₀
x₀ : 𝕜
h :
  Eq.{uF + 1} (α := F) (convolution (𝕜 := 𝕜) f₀ (deriv g₀) L μ x₀)
    (convolution.{u𝕜, u𝕜, uE, uE', uF} (𝕜 := 𝕜) (E' := E') f₀
      (fun (a : 𝕜) ↦ ((fderiv 𝕜 g₀ a : 𝕜 →L[𝕜] E') : (a : 𝕜) → E') 1) L μ x₀)
⊢ Eq.{uF + 1} (α := F) (convolution (𝕜 := 𝕜) f₀ (deriv g₀) L μ x₀ : F)
    ((convolution (𝕜 := 𝕜) (E' := 𝕜 →L[𝕜] E') f₀ (fderiv 𝕜 g₀) (precompR 𝕜 L) μ x₀ : (a : 𝕜) → F) 1 : F)

Tactic:
rw [convolution_precompR_apply L hf (hcg.fderiv 𝕜) (hg.continuous_fderiv one_ne_zero)]

Premises used: HasCompactSupport.fderiv, MeasureTheory.convolution_precompR_apply, ContDiff.continuous_fderiv, one_ne_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
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
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst_8 : μ.IsAddLeftInvariant
inst_9 : SFinite μ
hf : LocallyIntegrable f₀ μ
hcg : HasCompactSupport g₀
hg : ContDiff 𝕜 1 g₀
x₀ : 𝕜
⊢ Eq.{uF + 1} (α := F) (convolution (𝕜 := 𝕜) f₀ (deriv g₀) L μ x₀)
    (convolution.{u𝕜, u𝕜, uE, uE', uF} (𝕜 := 𝕜) (E' := E') f₀
      (fun (a : 𝕜) ↦ ((fderiv 𝕜 g₀ a : 𝕜 →L[𝕜] E') : (a : 𝕜) → E') 1) L μ x₀)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
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
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst_8 : μ.IsAddLeftInvariant
inst_9 : SFinite μ
inst_10 : μ.IsNegInvariant
hcf : HasCompactSupport f₀
hf : ContDiff 𝕜 1 f₀
hg : LocallyIntegrable g₀ μ
x₀ : 𝕜
simp :
  HasDerivAt.{u𝕜, uF} (F := F) (convolution (𝕜 := 𝕜) g₀ f₀ L.flip μ) (convolution (𝕜 := 𝕜) g₀ (deriv f₀) L.flip μ x₀) x₀
⊢ HasDerivAt.{u𝕜, uF} (F := F) (convolution (𝕜 := 𝕜) f₀ g₀ L μ) (convolution (𝕜 := 𝕜) (deriv f₀) g₀ L μ x₀) x₀

Tactic:
simp +singlePass only [← convolution_flip]

Premises used: MeasureTheory.convolution_flip
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
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
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst_8 : μ.IsAddLeftInvariant
inst_9 : SFinite μ
inst_10 : μ.IsNegInvariant
hcf : HasCompactSupport f₀
hf : ContDiff 𝕜 1 f₀
hg : LocallyIntegrable g₀ μ
x₀ : 𝕜
⊢ HasDerivAt.{u𝕜, uF} (F := F) (convolution (𝕜 := 𝕜) g₀ f₀ L.flip μ) (convolution (𝕜 := 𝕜) g₀ (deriv f₀) L.flip μ x₀) x₀

Tactic:
hcf.hasDerivAt_convolution_right L.flip hg hf x₀

Premises used: HasCompactSupport.hasDerivAt_convolution_right, ContinuousLinearMap.flip
-- Module: Mathlib.Analysis.Calculus.ContDiff.Convolution
Goal:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
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
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst_8 : μ.IsAddLeftInvariant
inst_9 : SFinite μ
inst_10 : μ.IsNegInvariant
hcf : HasCompactSupport f₀
hf : ContDiff 𝕜 1 f₀
hg : LocallyIntegrable g₀ μ
x₀ : 𝕜
⊢ HasDerivAt.{u𝕜, uF} (F := F) (convolution (𝕜 := 𝕜) g₀ f₀ L.flip μ) (convolution (𝕜 := 𝕜) g₀ (deriv f₀) L.flip μ x₀) x₀

Tactic:
exact hcf.hasDerivAt_convolution_right L.flip hg hf x₀

Premises used: HasCompactSupport.hasDerivAt_convolution_right, ContinuousLinearMap.flip
-- 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
f : G → E
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
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) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
p : P
hp : p ∈ s
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (g p)

Tactic:
hg.continuousOn.comp_continuous (.prodMk_right _) fun x => ?_

Premises used: ContinuousOn.comp_continuous, Continuous.prodMk_right, ContDiffOn.continuousOn
-- 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
f : G → E
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
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) (SProd.sprod (β := Set G) s univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : (x : P × G) → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
p : P
hp : p ∈ s
refine : ∀ (x : G), (p, x) ∈ SProd.sprod (β := Set G) s univ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (g p)

Tactic:
refine hg.continuousOn.comp_continuous (.prodMk_right _) fun x => ?_

Premises used: ContinuousOn.comp_continuous, Continuous.prodMk_right, ContDiffOn.continuousOn