awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
m n : ℕ∞ω
i : ℕ
hf : ContDiffAt 𝕜 n f x₀
hmn : m + (↑i : ℕ∞ω) ≤ n
⊢ ContDiffAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m (iteratedFDeriv 𝕜 i f) x₀
have rw : ∀ (hf : ContDiffWithinAt 𝕜 n f univ x₀) (hmn : m + (↑i : ℕ∞ω) ≤ n),
  ContDiffWithinAt 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) m
    (iteratedFDerivWithin 𝕜 i f univ) univ x₀
Tactic: rw [← iteratedFDerivWithin_univ, ← contDiffWithinAt_univ] at *
Cleared hypotheses: hf, hmn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
m n : ℕ∞ω
f : E → F
hf : ContDiff 𝕜 n f
hmn : m + 1 ≤ n
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (F := F) m fun (p : E × E) ↦ (fderiv 𝕜 f p.1 : (a : E) → F) p.2
have rw : ∀ (hf : ContDiffOn 𝕜 n f univ) (hmn : m + 1 ≤ n),
  ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) m (fun (p : E × E) ↦ (fderiv 𝕜 f p.1 : (a : E) → F) p.2) univ
Tactic: rw [← contDiffOn_univ] at hf ⊢
Cleared hypotheses: hf, hmn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
m n : ℕ∞ω
f : E → F
hf : ContDiffOn 𝕜 n f univ
hmn : m + 1 ≤ n
⊢ ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) m (fun (p : E × E) ↦ (fderiv 𝕜 f p.1 : (a : E) → F) p.2) univ
have rw : ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) m (fun (p : E × E) ↦ (fderivWithin 𝕜 f univ p.1 : (a : E) → F) p.2)
  (SProd.sprod (α := Set E) (β := Set E) univ univ)
Tactic: rw [← fderivWithin_univ, ← univ_prod_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
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
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) (precompR G L) μ x₀) x₀
have inl : ∀ (hcg : HasCompactSupport.{uG, uE'} (α := G) (β := E') 0) (hg : ContDiff.{u𝕜, uG, uE'} 𝕜 (E := G) (F := E') 1 0),
  HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (E' := E') f 0 L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 0) (precompR G L) μ x₀) x₀
Tactic: rcases hcg.eq_zero_or_finiteDimensional 𝕜 hg.continuous with (rfl | fin_dim)
Cleared hypotheses: g, hcg, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
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
inl :
  ∀ (hcg : HasCompactSupport.{uG, uE'} (α := G) (β := E') 0) (hg : ContDiff.{u𝕜, uG, uE'} 𝕜 (E := G) (F := E') 1 0),
    HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (E' := E') f 0 L μ)
      (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 0) (precompR G L) μ x₀) x₀
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) (precompR G L) μ x₀) x₀
have inr : ∀ (fin_dim : FiniteDimensional 𝕜 G),
  HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) (precompR G L) μ x₀) x₀
Tactic: rcases hcg.eq_zero_or_finiteDimensional 𝕜 hg.continuous with (rfl | fin_dim)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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
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
hf : LocallyIntegrable f μ
x₀ : G
hcg : HasCompactSupport.{uG, uE'} (α := G) (β := E') 0
hg : ContDiff.{u𝕜, uG, uE'} 𝕜 (E := G) (F := E') 1 0
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (E' := E') f 0 L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 0) (precompR G L) μ x₀) x₀
have this : Eq (α := (x : G) → G →L[𝕜] E') (fderiv 𝕜 0) 0
Tactic: have : fderiv 𝕜 (0 : G → E') = 0 := fderiv_const (0 : E')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
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
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
hf : LocallyIntegrable f μ
x₀ : G
hcg : HasCompactSupport.{uG, uE'} (α := G) (β := E') 0
hg : ContDiff.{u𝕜, uG, uE'} 𝕜 (E := G) (F := E') 1 0
this : Eq (α := (x : G) → G →L[𝕜] E') (fderiv 𝕜 0) 0
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (E' := E') f 0 L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 0) (precompR G L) μ x₀) x₀
have inl : HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) 0 0 x₀
Tactic: simp only [this, convolution_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) (precompR G L) μ x₀) x₀
have this : ProperSpace G
Tactic: have : ProperSpace G := FiniteDimensional.proper_rclike 𝕜 G
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) L' μ x₀) x₀
have 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))) μ
Tactic: have h1 : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (fun t => L (f t) (g (x - t))) μ :=
    Eventually.of_forall
      (hf.aestronglyMeasurable.convolution_integrand_snd L hg.continuous.aestronglyMeasurable)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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))) μ
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) L' μ x₀) x₀
have 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)))
    μ
Tactic: have h2 : ∀ x, AEStronglyMeasurable (fun t => L' (f t) (fderiv 𝕜 g (x - t))) μ :=
    hf.aestronglyMeasurable.convolution_integrand_snd L'
      (hg.continuous_fderiv one_ne_zero).aestronglyMeasurable
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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)))
      μ
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) L' μ x₀) x₀
have h3 : ∀ (x t : G), HasFDerivAt (fun (x : G) ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
Tactic: have h3 : ∀ x t, HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x := fun x t ↦ by
    simpa using
      (hg.differentiable one_ne_zero).differentiableAt.hasFDerivAt.comp x
        ((hasFDerivAt_id x).sub (hasFDerivAt_const t x))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (hypothesis)
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
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) L' μ x₀) x₀
have hK' : IsCompact K'
Tactic: have hK' : IsCompact K' := (hcg.fderiv 𝕜).isCompact.neg.add (isCompact_closedBall x₀ 1)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
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'
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) L' μ x₀) x₀
have inr : ∀ᵐ (a : G) ∂μ,
  ∀ x ∈ ball x₀ 1,
    norm (E := G →L[𝕜] F)
        ((((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)) :
          G →L[𝕜] F) ≤
      (-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)) a
Tactic: apply hasFDerivAt_integral_of_dominated_of_fderiv_le (ball_mem_nhds _ zero_lt_one) h1 _ (h2 x₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
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 :
  ∀ᵐ (a : G) ∂μ,
    ∀ x ∈ ball x₀ 1,
      norm (E := G →L[𝕜] F)
          ((((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)) :
            G →L[𝕜] F) ≤
        (-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)) a
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) L' μ x₀) x₀
have inr₁ : 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: apply hasFDerivAt_integral_of_dominated_of_fderiv_le (ball_mem_nhds _ zero_lt_one) h1 _ (h2 x₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
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 :
  ∀ᵐ (a : G) ∂μ,
    ∀ x ∈ ball x₀ 1,
      norm (E := G →L[𝕜] F)
          ((((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)) :
            G →L[𝕜] F) ≤
        (-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)) a
inr₁ :
  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)
    μ
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) L' μ x₀) x₀
have inr₂ : ∀ᵐ (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: apply hasFDerivAt_integral_of_dominated_of_fderiv_le (ball_mem_nhds _ zero_lt_one) h1 _ (h2 x₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Convolution (goal)
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 :
  ∀ᵐ (a : G) ∂μ,
    ∀ x ∈ ball x₀ 1,
      norm (E := G →L[𝕜] F)
          ((((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)) :
            G →L[𝕜] F) ≤
        (-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)) a
inr₁ :
  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)
    μ
inr₂ :
  ∀ᵐ (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
⊢ HasFDerivAt.{u𝕜, uG, uF} (𝕜 := 𝕜) (F := F) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
    (convolution (𝕜 := 𝕜) (E' := G →L[𝕜] E') f (fderiv 𝕜 g) L' μ x₀) x₀
have apply : G → ℝ
Tactic: apply hasFDerivAt_integral_of_dominated_of_fderiv_le (ball_mem_nhds _ zero_lt_one) h1 _ (h2 x₀)