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
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} (𝕜 := 𝕜) g f L.flip μ)

Tactic:
hcf.contDiff_convolution_right L.flip hg hf

Premises used: ContinuousLinearMap.flip, HasCompactSupport.contDiff_convolution_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
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} (𝕜 := 𝕜) g f L.flip μ)

Tactic:
exact hcf.contDiff_convolution_right L.flip hg hf

Premises used: ContinuousLinearMap.flip, HasCompactSupport.contDiff_convolution_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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.{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 _ _)
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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
⊢ AnalyticOn 𝕜 f s

Tactic:
this.congr (fun y hy ↦ (hf.zero_eq _ hy).symm)

Premises used: HasFTaylorSeriesUpToOn.zero_eq, AnalyticOn.congr, Eq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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
⊢ AnalyticOn 𝕜 f s

Tactic:
exact this.congr (fun y hy ↦ (hf.zero_eq _ hy).symm)

Premises used: HasFTaylorSeriesUpToOn.zero_eq, AnalyticOn.congr, Eq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Tactic:
obtain ⟨u, hu, p, hp, h'p⟩ := h
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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:
⟨u, hu, hp.analyticOn (h'p 0)⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat, HasFTaylorSeriesUpToOn.analyticOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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:
exact ⟨u, hu, hp.analyticOn (h'p 0)⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
obtain : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (hf : AnalyticOn 𝕜 f u), AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
obtain ⟨u, hu, hf⟩ := h.analyticOn

Premises used: ContDiffWithinAt.analyticOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ x ∈ insert x s

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ x ∈ u

Tactic:
have xu : x ∈ u := mem_of_mem_nhdsWithin (by simp) hu
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
xu : x ∈ u
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
(hf x xu).mono_of_mem_nhdsWithin (nhdsWithin_mono _ (subset_insert _ _) hu)

Premises used: AnalyticWithinAt.mono_of_mem_nhdsWithin, Set.subset_insert, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
xu : x ∈ u
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
exact (hf x xu).mono_of_mem_nhdsWithin (nhdsWithin_mono _ (subset_insert _ _) hu)

Premises used: AnalyticWithinAt.mono_of_mem_nhdsWithin, Set.subset_insert, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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

Tactic:
⟨fun h ↦ h.analyticWithinAt, fun h ↦ ?_⟩

Premises used: Iff.intro, ContDiffWithinAt.analyticWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
refine : ∀ (h : AnalyticWithinAt 𝕜 f s x), ContDiffWithinAt 𝕜 ω f s x
⊢ ContDiffWithinAt 𝕜 ω f s x ↔ AnalyticWithinAt 𝕜 f s x

Tactic:
refine ⟨fun h ↦ h.analyticWithinAt, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
obtain ⟨u, hu, p, hp, h'p⟩ := h.exists_hasFTaylorSeriesUpToOn ω

Premises used: Top.top, AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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:
⟨u, hu, p, hp.of_le le_top, fun i ↦ h'p i⟩

Premises used: HasFTaylorSeriesUpToOn.of_le, le_top, And.intro, Exists.intro, ContDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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:
exact ⟨u, hu, p, hp.of_le le_top, fun i ↦ h'p i⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ
⊢ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x ↔
    ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p u

Tactic:
⟨fun H => H n le_rfl, fun ⟨u, hu, p, hp⟩ _m hm => ⟨u, hu, p, hp.of_le (mod_cast hm)⟩⟩

Premises used: le_rfl, nhdsWithin, HasFTaylorSeriesUpToOn.of_le, cast, Membership.mem, Exists, Insert.insert, Nat.cast_le._simp_1, Nat.cast, _private.0.contDiffWithinAt_nat.match_1, And, And.intro, Iff.intro, Exists.intro, Eq.symm, HasFTaylorSeriesUpToOn, Eq.trans
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞ω
hn : Ne (α := ℕ∞ω) ω ∞
⊢ ContDiffWithinAt 𝕜 ω f s x ↔
    ∃ u ∈ 𝓝[insert x s] x,
      ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
        HasFTaylorSeriesUpToOn ω f p u ∧
          (Eq (α := ℕ∞ω) ω ω →
            ∀ (i : ℕ),
              AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
                (fun (x : E) ↦ p x i) u)

Tactic:
simp [ContDiffWithinAt]

Premises used: ContDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞ω
hn : Ne (α := ℕ∞ω) ∞ ∞
⊢ ContDiffWithinAt 𝕜 ∞ f s x ↔
    ∃ u ∈ 𝓝[insert x s] x,
      ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
        HasFTaylorSeriesUpToOn ∞ f p u ∧
          (Eq (α := ℕ∞ω) ∞ ω →
            ∀ (i : ℕ),
              AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
                (fun (x : E) ↦ p x i) u)

Tactic:
simp at hn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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_1 : ℕ∞ω
n : ℕ
hn : Ne (α := ℕ∞ω) (↑n : ℕ∞ω) ∞
⊢ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x ↔
    ∃ u ∈ 𝓝[insert x s] x,
      ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
        HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f p u ∧
          (Eq (α := ℕ∞ω) (↑n : ℕ∞ω) ω →
            ∀ (i : ℕ),
              AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
                (fun (x : E) ↦ p x i) u)

Tactic:
simp [contDiffWithinAt_nat]

Premises used: contDiffWithinAt_nat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞ω
hn : n ≠ ∞
⊢ ContDiffWithinAt 𝕜 n f s x ↔
    ∃ u ∈ 𝓝[insert x s] x,
      ∃ (p : E → FormalMultilinearSeries 𝕜 E F),
        HasFTaylorSeriesUpToOn n f p u ∧
          (n = ω →
            ∀ (i : ℕ),
              AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
                (fun (x : E) ↦ p x i) u)

Tactic:
match n with
  | ω => simp [ContDiffWithinAt]
  | ∞ => simp at hn
  | (n : ℕ) => simp [contDiffWithinAt_nat]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 n : ℕ∞ω
h : ContDiffWithinAt 𝕜 ω f s x
hmn : LE.le (α := ℕ∞ω) ω ω
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
h
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 n : ℕ∞ω
h : ContDiffWithinAt 𝕜 ω f s x
hmn : LE.le (α := ℕ∞ω) ω ω
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
exact h
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ
_ :
  (↑k : ℕ∞) ≤ m →
    ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑k : ℕ∞ω) f p u
⊢ (↑k : ℕ∞) ≤ m →
    ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑k : ℕ∞ω) f p u

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑k : ℕ∞ω) f p u

Tactic:
obtain ⟨u, hu, p, hp, -⟩ := h
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞ω
m : ℕ∞
hmn : (↑m : ℕ∞ω) ≤ ω
k : ℕ
h : (↑k : ℕ∞) ≤ m
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:
⟨u, hu, p, hp.of_le le_top⟩

Premises used: HasFTaylorSeriesUpToOn.of_le, le_top, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞ω
m : ℕ∞
hmn : (↑m : ℕ∞ω) ≤ ω
k : ℕ
h : (↑k : ℕ∞) ≤ m
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:
exact ⟨u, hu, p, hp.of_le le_top⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 n : ℕ∞ω
h : ContDiffWithinAt 𝕜 ω f s x
hmn : m ≤ ω
⊢ ContDiffWithinAt 𝕜 m f s x

Tactic:
match m with
    | ω => exact h
    | (m : ℕ∞) =>
      intro k _
      obtain ⟨u, hu, p, hp, -⟩ := h
      exact ⟨u, hu, p, hp.of_le le_top⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 n_1 : ℕ∞ω
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
hmn : ω ≤ (↑n : ℕ∞ω)
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
simp at hmn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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_1 : ℕ∞ω
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
m : ℕ∞
hmn : (↑m : ℕ∞ω) ≤ (↑n : ℕ∞ω)
⊢ ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f s x

Tactic:
fun k hk ↦ h k (le_trans hk (mod_cast hmn))

Premises used: WithTop.coe_le_coe._simp_1, cast, ContDiffWithinAt, le_trans
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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_1 : ℕ∞ω
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
m : ℕ∞
hmn : (↑m : ℕ∞ω) ≤ (↑n : ℕ∞ω)
⊢ ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f s x

Tactic:
exact fun k hk ↦ h k (le_trans hk (mod_cast hmn))

Premises used: le_trans
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 n_1 : ℕ∞ω
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
hmn : m ≤ (↑n : ℕ∞ω)
⊢ ContDiffWithinAt 𝕜 m f s x

Tactic:
match m with
    | ω => simp at hmn
    | (m : ℕ∞) => exact fun k hk ↦ h k (le_trans hk (mod_cast hmn))
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hmn : m ≤ n
⊢ ContDiffWithinAt 𝕜 m f s x

Tactic:
match n with
  | ω => match m with
    | ω => exact h
    | (m : ℕ∞) =>
      intro k _
      obtain ⟨u, hu, p, hp, -⟩ := h
      exact ⟨u, hu, p, hp.of_le le_top⟩
  | (n : ℕ∞) => match m with
    | ω => simp at hmn
    | (m : ℕ∞) => exact fun k hk ↦ h k (le_trans hk (mod_cast hmn))
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞ω
inst_5 : CompleteSpace F
h : AnalyticWithinAt 𝕜 f s x
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
(contDiffWithinAt_omega_iff_analyticWithinAt.2 h).of_le le_top

Premises used: Iff.mpr, ContDiffWithinAt.of_le, contDiffWithinAt_omega_iff_analyticWithinAt, le_top
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞
⊢ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f s x

Tactic:
⟨fun H _ hm => H.of_le (mod_cast hm), fun H m hm => H m hm _ le_rfl⟩

Premises used: le_rfl, ContDiffWithinAt.of_le, WithTop.coe_le_coe._simp_1, cast, Iff.intro, Eq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ), LE.le (α := ℕ∞) (↑m : ℕ∞) ⊤ → ContDiffWithinAt 𝕜 (↑m : ℕ∞ω) f s x) ↔
    ∀ (n : ℕ), ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x

Tactic:
simp only [forall_prop_of_true, le_top]

Premises used: le_top, forall_prop_of_true
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ ContDiffWithinAt 𝕜 0 f s x

Tactic:
have := h.of_le zero_le
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ ∃ 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

Premises used: CharP.cast_eq_zero, forall_eq, Nat.cast_eq_zero, ContDiffWithinAt, nonpos_iff_eq_zero