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
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
R_contdiff :
  ContDiffOn 𝕜 (↑n : WithTop ℕ∞) R (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)
A :
  ContDiffOn 𝕜 (F := F) (↑n : WithTop ℕ∞)
    ((⇑isoF : (a : eF) → F) ∘ R ∘ (⇑(isoP.prodCongr isoG).symm : (a : P × G) → eP × eG))
    (SProd.sprod (β := Set G) s univ)
p : P
x : G
⊢ Eq.{uF + 1} (α := F) (((⇑isoF : (a : eF) → F) ∘ R ∘ (⇑(isoP.prodCongr isoG).symm : (a : P × G) → eP × eG)) (p, x))
    (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f (g (p, x).1) L μ (p, x).2)
have h : Eq.{uF + 1} (α := F) ((isoF : (a : eF) → F) (R ((isoP.symm : (a : P) → eP) p, (isoG.symm : (a : G) → eG) x)) : F)
  (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f (g p) L μ x : F)
Tactic: simp only [(· ∘ ·), ContinuousLinearEquiv.prodCongr_symm, ContinuousLinearEquiv.prodCongr_apply]
-- 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
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
R_contdiff :
  ContDiffOn 𝕜 (↑n : WithTop ℕ∞) R (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)
A :
  ContDiffOn 𝕜 (F := F) (↑n : WithTop ℕ∞)
    ((⇑isoF : (a : eF) → F) ∘ R ∘ (⇑(isoP.prodCongr isoG).symm : (a : P × G) → eP × eG))
    (SProd.sprod (β := Set G) s univ)
p : P
x : G
⊢ Eq.{uF + 1} (α := F) ((isoF : (a : eF) → F) (R ((isoP.symm : (a : P) → eP) p, (isoG.symm : (a : G) → eG) x)) : F)
    (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f (g p) L μ x : F)
have h : Eq.{uF + 1} (α := F)
  ((isoF : (a : eF) → F)
      (∫ (t : eG),
        (((eL : (a : E) → eE' →L[𝕜] eF) (ef t) : eE' →L[𝕜] eF) : (a : eE') → eF)
          (eg ((isoP.symm : (a : P) → eP) p) (HSub.hSub (α := eG) ((isoG.symm : (a : G) → eG) x : eG) t)) ∂eμ) :
    F)
  (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g p (x - t)) ∂μ : F)
Tactic: simp only [R, convolution]
-- 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
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
R_contdiff :
  ContDiffOn 𝕜 (↑n : WithTop ℕ∞) R (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)
A :
  ContDiffOn 𝕜 (F := F) (↑n : WithTop ℕ∞)
    ((⇑isoF : (a : eF) → F) ∘ R ∘ (⇑(isoP.prodCongr isoG).symm : (a : P × G) → eP × eG))
    (SProd.sprod (β := Set G) s univ)
p : P
x : G
⊢ Eq.{uF + 1} (α := F)
    ((isoF : (a : eF) → F)
        (∫ (t : eG),
          (((eL : (a : E) → eE' →L[𝕜] eF) (ef t) : eE' →L[𝕜] eF) : (a : eE') → eF)
            (eg ((isoP.symm : (a : P) → eP) p) (HSub.hSub (α := eG) ((isoG.symm : (a : G) → eG) x : eG) t)) ∂eμ) :
      F)
    (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g p (x - t)) ∂μ : F)
have h : Eq.{uF + 1} (α := F)
  (∫ (x_1 : G),
    (isoF : (a : eF) → F)
      ((((eL : (a : E) → eE' →L[𝕜] eF) (ef ((isoG.symm : (a : G) → eG) x_1)) : eE' →L[𝕜] eF) : (a : eE') → eF)
          (eg ((isoP.symm : (a : P) → eP) p)
            (HSub.hSub (α := eG) (β := eG) ((isoG.symm : (a : G) → eG) x : eG) ((isoG.symm : (a : G) → eG) x_1 : eG))) :
        eF) ∂μ)
  (∫ (t : G), (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g p (x - t)) ∂μ)
Tactic: rw [IsClosedEmbedding.integral_map, ← isoF.integral_comp_comm]
-- 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
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
R_contdiff :
  ContDiffOn 𝕜 (↑n : WithTop ℕ∞) R (SProd.sprod (α := Set eP) (β := Set eG) ((⇑isoP : (a : eP) → P) ⁻¹' s) univ)
A :
  ContDiffOn 𝕜 (F := F) (↑n : WithTop ℕ∞)
    ((⇑isoF : (a : eF) → F) ∘ R ∘ (⇑(isoP.prodCongr isoG).symm : (a : P × G) → eP × eG))
    (SProd.sprod (β := Set G) s univ)
⊢ ContDiffOn 𝕜 (F := F) (↑n : WithTop ℕ∞)
    (fun (q : P × G) ↦ convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f (g q.1) L μ q.2) (SProd.sprod (β := Set G) s univ)
have this : Eq (α := P × G → F) ((⇑isoF : (a : eF) → F) ∘ R ∘ (⇑(isoP.prodCongr isoG).symm : (a : P × G) → eP × eG))
  fun (q : P × G) ↦ convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f (g q.1) L μ q.2
Tactic: have : isoF ∘ R ∘ (isoP.prodCongr isoG).symm = fun q : P × G => (f ⋆[L, μ] g q.1) q.2 := by
    apply funext
    rintro ⟨p, x⟩
    simp only [(· ∘ ·), ContinuousLinearEquiv.prodCongr_symm, ContinuousLinearEquiv.prodCongr_apply]
    simp only [R, convolution]
    rw [IsClosedEmbedding.integral_map, ← isoF.integral_comp_comm]
    · rfl
    · exact isoG.symm.toHomeomorph.isClosedEmbedding
-- 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
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
n : ℕ∞
L : E →L[𝕜] E' →L[𝕜] F
s : Set P
v : P → G
hv : ContDiffOn 𝕜 (↑n : WithTop ℕ∞) v s
f : G → E
g : P → G → E'
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)
⊢ ContDiffOn.{u𝕜, uP, uF} 𝕜 (F := F) (↑n : WithTop ℕ∞)
    (fun (x : P) ↦ convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f (g x) L μ (v x)) s
have apply : MapsTo (fun (x : P) ↦ (id x, v x)) s (SProd.sprod (β := Set G) s univ)
Tactic: apply (contDiffOn_convolution_right_with_param L hs hk hgs hf hg).comp (contDiffOn_id.prodMk hv)
-- 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
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
inst_14 : μ.IsAddLeftInvariant
inst_15 : μ.IsNegInvariant
L : E' →L[𝕜] E →L[𝕜] F
s : Set P
n : ℕ∞
v : P → G
hv : ContDiffOn 𝕜 (↑n : WithTop ℕ∞) v s
f : G → E
g : P → G → E'
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)
⊢ ContDiffOn.{u𝕜, uP, uF} 𝕜 (F := F) (↑n : WithTop ℕ∞)
    (fun (x : P) ↦ convolution.{u𝕜, uG, uE', uE, uF} (𝕜 := 𝕜) (g x) f L μ (v x)) s
have apply : MapsTo (fun (x : P) ↦ (id x, v x)) s (SProd.sprod (β := Set G) s univ)
Tactic: apply (contDiffOn_convolution_left_with_param L hs hk hgs hf hg).comp (contDiffOn_id.prodMk hv)
-- 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
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
n : ℕ∞
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 (↑n : WithTop ℕ∞) g
⊢ ContDiff.{u𝕜, uG, uF} 𝕜 (F := F) (↑n : WithTop ℕ∞) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
have rcases : ∀ (k : Set G) (hk : IsCompact k) (h'k : ∀ x ∉ k, g x = 0),
  ContDiff.{u𝕜, uG, uF} 𝕜 (F := F) (↑n : WithTop ℕ∞) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
Tactic: rcases exists_compact_iff_hasCompactSupport.2 hcg with ⟨k, hk, h'k⟩
-- 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
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
n : ℕ∞
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 (↑n : WithTop ℕ∞) g
k : Set G
hk : IsCompact k
h'k : ∀ x ∉ k, g x = 0
⊢ ContDiff.{u𝕜, uG, uF} 𝕜 (F := F) (↑n : WithTop ℕ∞) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
have rw : ContDiffOn.{u𝕜, uG, uF} 𝕜 (F := F) (↑n : WithTop ℕ∞) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ) univ
Tactic: rw [← contDiffOn_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
inst_9 : NormedAddCommGroup G
inst_10 : BorelSpace G
inst_11 : NormedSpace 𝕜 G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_12 : μ.IsAddLeftInvariant
inst_13 : μ.IsNegInvariant
n : ℕ∞
hcf : HasCompactSupport f
hf : ContDiff 𝕜 (↑n : WithTop ℕ∞) f
hg : LocallyIntegrable g μ
⊢ ContDiff.{u𝕜, uG, uF} 𝕜 (F := F) (↑n : WithTop ℕ∞) (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L μ)
have rw : ContDiff.{u𝕜, uG, uF} 𝕜 (F := F) (↑n : WithTop ℕ∞) (convolution.{u𝕜, uG, uE', uE, uF} (𝕜 := 𝕜) g f L.flip μ)
Tactic: rw [← convolution_flip]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn ω f p s
h : AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (fun (x : E) ↦ p x 0) s
⊢ AnalyticOn 𝕜 f s
have this : AnalyticOn.{u, uE, uF} 𝕜 (F := F)
  (fun (x : E) ↦
    (continuousMultilinearCurryFin0 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) → F) (p x 0))
  s
Tactic: have : AnalyticOn 𝕜 (fun x ↦ (continuousMultilinearCurryFin0 𝕜 E F) (p x 0)) s :=
    (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn
      h (Set.mapsTo_univ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u
have obtain : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (hp : HasFTaylorSeriesUpToOn ω f p u)
  (h'p :
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u),
  ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u
Tactic: obtain ⟨u, hu, p, hp, h'p⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f s x
⊢ AnalyticWithinAt 𝕜 f s x
have obtain : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (hf : AnalyticOn 𝕜 f u), AnalyticWithinAt 𝕜 f s x
Tactic: obtain ⟨u, hu, hf⟩ := h.analyticOn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : AnalyticOn 𝕜 f u
⊢ AnalyticWithinAt 𝕜 f s x
have xu : x ∈ u
Tactic: have xu : x ∈ u := mem_of_mem_nhdsWithin (by simp) hu
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
inst_5 : CompleteSpace F
⊢ ContDiffWithinAt 𝕜 ω f s x ↔ AnalyticWithinAt 𝕜 f s x
have refine : ∀ (h : AnalyticWithinAt 𝕜 f s x), ContDiffWithinAt 𝕜 ω f s x
Tactic: refine ⟨fun h ↦ h.analyticWithinAt, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
inst_5 : CompleteSpace F
h : AnalyticWithinAt 𝕜 f s x
⊢ ContDiffWithinAt 𝕜 ω f s x
have obtain : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (hp : HasFTaylorSeriesUpToOn ω f p u)
  (h'p :
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u),
  ContDiffWithinAt 𝕜 ω f s x
Tactic: obtain ⟨u, hu, p, hp, h'p⟩ := h.exists_hasFTaylorSeriesUpToOn ω
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m_1 n : ℕ∞ω
h : ContDiffWithinAt 𝕜 ω f s x
m : ℕ∞
hmn : (↑m : ℕ∞ω) ≤ ω
k : ℕ
h_1 : (↑k : ℕ∞) ≤ m
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑k : ℕ∞ω) f p u
have obtain : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (hp : HasFTaylorSeriesUpToOn ω f p u),
  ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑k : ℕ∞ω) f p u
Tactic: obtain ⟨u, hu, p, hp, -⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
⊢ ContinuousWithinAt f s x
have this : ContDiffWithinAt 𝕜 0 f s x
Tactic: have := h.of_le zero_le
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
this : ContDiffWithinAt 𝕜 0 f s x
⊢ ContinuousWithinAt f s x
have this₁ : ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn 0 f p u
Tactic: simp only [ContDiffWithinAt, nonpos_iff_eq_zero, Nat.cast_eq_zero, forall_eq, CharP.cast_eq_zero]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
this : ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn 0 f p u
⊢ ContinuousWithinAt f s x
have rcases : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (H : HasFTaylorSeriesUpToOn 0 f p u),
  ContinuousWithinAt f s x
Tactic: rcases this with ⟨u, hu, p, H⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn 0 f p u
⊢ ContinuousWithinAt f s x
have rw : ∀ (hu : x ∈ u ∧ u ∈ 𝓝[s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (H : HasFTaylorSeriesUpToOn 0 f p u),
  ContinuousWithinAt f s x
Tactic: rw [mem_nhdsWithin_insert] at hu
Cleared hypotheses: hu, p, H