awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) 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.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (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[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
I4 :
  ∀ᵐ (a : G) ∂μ,
    ∀ (x : P × G),
      dist x q₀ < δ →
        norm (E := P × G →L[𝕜] F)
            ((((precompR (P × G) L : (a : E) → (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (f a) :
                    (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :
                  (a : P × G →L[𝕜] E') → P × G →L[𝕜] F)
                (g' (x.1, x.2 - a)) :
              P × G →L[𝕜] F) ≤
          bound a
⊢ Integrable bound μ
have rw : IntegrableOn (ε := ℝ)
  (fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C) U μ
Tactic: rw [integrable_indicator_iff U_open.measurableSet]
-- 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
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
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) 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.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (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[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
I4 :
  ∀ᵐ (a : G) ∂μ,
    ∀ (x : P × G),
      dist x q₀ < δ →
        norm (E := P × G →L[𝕜] F)
            ((((precompR (P × G) L : (a : E) → (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (f a) :
                    (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :
                  (a : P × G →L[𝕜] E') → P × G →L[𝕜] F)
                (g' (x.1, x.2 - a)) :
              P × G →L[𝕜] F) ≤
          bound a
⊢ HasFDerivAt (𝕜 := 𝕜) (F := F) (fun (q : P × G) ↦ convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f (g q.1) L μ q.2)
    (convolution (𝕜 := 𝕜) (E' := P × G →L[𝕜] E') f (fun (x : G) ↦ fderiv 𝕜 ↿g (q₀.1, x)) (precompR (P × G) L) μ q₀.2) q₀
have I5 : Integrable bound μ
Tactic: have I5 : Integrable bound μ := by
    rw [integrable_indicator_iff U_open.measurableSet]
    exact (hU.norm.const_mul _).mul_const _
-- 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
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
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) 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.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (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[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
I4 :
  ∀ᵐ (a : G) ∂μ,
    ∀ (x : P × G),
      dist x q₀ < δ →
        norm (E := P × G →L[𝕜] F)
            ((((precompR (P × G) L : (a : E) → (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (f a) :
                    (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :
                  (a : P × G →L[𝕜] E') → P × G →L[𝕜] F)
                (g' (x.1, x.2 - a)) :
              P × G →L[𝕜] F) ≤
          bound a
I5 : Integrable bound μ
a : G
x : P × G
hx : dist x q₀ < δ
⊢ HasFDerivAt (𝕜 := 𝕜) (F := F)
    (fun (x : P × G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a)))
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (g' (x.1, x.2 - a))) x
have h : HasFDerivAt (𝕜 := 𝕜) (F := E') (fun (x : P × G) ↦ g x.1 (x.2 - a)) (g' (x.1, x.2 - a)) x
Tactic: apply (L _).hasFDerivAt.comp 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
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
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) 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.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (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[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
I4 :
  ∀ᵐ (a : G) ∂μ,
    ∀ (x : P × G),
      dist x q₀ < δ →
        norm (E := P × G →L[𝕜] F)
            ((((precompR (P × G) L : (a : E) → (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (f a) :
                    (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :
                  (a : P × G →L[𝕜] E') → P × G →L[𝕜] F)
                (g' (x.1, x.2 - a)) :
              P × G →L[𝕜] F) ≤
          bound a
I5 : Integrable bound μ
a : G
x : P × G
hx : dist x q₀ < δ
⊢ SProd.sprod (β := Set G) s univ ∈ 𝓝 (x.1, x.2 - a)
have a₁ : (x.1, x.2 - a).1 ∈ s
Tactic: apply A'
-- 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
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
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) 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.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (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[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
I4 :
  ∀ᵐ (a : G) ∂μ,
    ∀ (x : P × G),
      dist x q₀ < δ →
        norm (E := P × G →L[𝕜] F)
            ((((precompR (P × G) L : (a : E) → (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (f a) :
                    (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :
                  (a : P × G →L[𝕜] E') → P × G →L[𝕜] F)
                (g' (x.1, x.2 - a)) :
              P × G →L[𝕜] F) ≤
          bound a
I5 : Integrable bound μ
a : G
x : P × G
hx : dist x q₀ < δ
⊢ (x.1, x.2 - a).1 ∈ s
have a₁ : (x.1, x.2 - a).1 ∈ ball q₀.1 ε
Tactic: apply h₀ε
-- 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
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
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) 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.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (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[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
I4 :
  ∀ᵐ (a : G) ∂μ,
    ∀ (x : P × G),
      dist x q₀ < δ →
        norm (E := P × G →L[𝕜] F)
            ((((precompR (P × G) L : (a : E) → (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (f a) :
                    (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :
                  (a : P × G →L[𝕜] E') → P × G →L[𝕜] F)
                (g' (x.1, x.2 - a)) :
              P × G →L[𝕜] F) ≤
          bound a
I5 : Integrable bound μ
a : G
x : P × G
hx : dist x q₀ < δ
⊢ (x.1, x.2 - a).1 ∈ ball q₀.1 ε
have hx₁ : max (dist x.1 q₀.1) (dist x.2 q₀.2) < δ
Tactic: rw [Prod.dist_eq] at hx
Cleared hypotheses: hx
-- 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
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
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) 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.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (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[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
I4 :
  ∀ᵐ (a : G) ∂μ,
    ∀ (x : P × G),
      dist x q₀ < δ →
        norm (E := P × G →L[𝕜] F)
            ((((precompR (P × G) L : (a : E) → (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (f a) :
                    (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :
                  (a : P × G →L[𝕜] E') → P × G →L[𝕜] F)
                (g' (x.1, x.2 - a)) :
              P × G →L[𝕜] F) ≤
          bound a
I5 : Integrable bound μ
a : G
x : P × G
hx : dist x q₀ < δ
⊢ HasFDerivAt (𝕜 := 𝕜) (F := E') (fun (x : P × G) ↦ g x.1 (x.2 - a)) (g' (x.1, x.2 - a)) x
have N : SProd.sprod (β := Set G) s univ ∈ 𝓝 (x.1, x.2 - a)
Tactic: have N : s ×ˢ univ ∈ 𝓝 (x.1, x.2 - a) := by
      apply A'
      apply h₀ε
      rw [Prod.dist_eq] at hx
      exact lt_of_lt_of_le (lt_of_le_of_lt (le_max_left _ _) hx) δε
-- 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
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
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → SProd.sprod (β := Set G) 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.{uG, uF} (β := F)
      (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g x.1 (x.2 - a))) μ
I2 :
  Integrable.{uF, uG} (ε := F)
    (fun (a : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f a) : E' →L[𝕜] F) : (a : E') → F) (g q₀.1 (q₀.2 - a))) μ
I3 :
  AEStronglyMeasurable (β := P × G →L[𝕜] F)
    (fun (a : G) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((L : (a : E) → E' →L[𝕜] F) (f a)) (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[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E) (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)
bound : G → ℝ :=
  U.indicator fun (t : G) ↦ norm (E := E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (precompR (P × G) L) * ‖f t‖ * C
I4 :
  ∀ᵐ (a : G) ∂μ,
    ∀ (x : P × G),
      dist x q₀ < δ →
        norm (E := P × G →L[𝕜] F)
            ((((precompR (P × G) L : (a : E) → (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (f a) :
                    (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) :
                  (a : P × G →L[𝕜] E') → P × G →L[𝕜] F)
                (g' (x.1, x.2 - a)) :
              P × G →L[𝕜] F) ≤
          bound a
I5 : Integrable bound μ
a : G
x : P × G
hx : dist x q₀ < δ
N : SProd.sprod (β := Set G) s univ ∈ 𝓝 (x.1, x.2 - a)
⊢ HasFDerivAt (𝕜 := 𝕜) (F := E') (fun (x : P × G) ↦ g x.1 (x.2 - a)) (g' (x.1, x.2 - a)) x
have Z : HasFDerivAt (↿g) (fderiv 𝕜 ↿g (x.1, x.2 - a)) (x.1, x.2 - a)
Tactic: have Z := ((hg.differentiableOn one_ne_zero).differentiableAt N).hasFDerivAt