-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffOn_univ : ContDiffOn 𝕜 n f univ ↔ ContDiff 𝕜 n f

Proof state:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
⊢ ContDiffOn 𝕜 ω f univ → ContDiff 𝕜 ω f

Tactic:
intro H

Result:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
H : ContDiffOn 𝕜 ω f univ
⊢ ContDiff 𝕜 ω f

Proof state:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ → ContDiff 𝕜 (↑n) f

Tactic:
intro H

Result:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
H : ContDiffOn 𝕜 (↑n) f univ
⊢ ContDiff 𝕜 (↑n) f

Proof state:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
H : ContDiffOn 𝕜 ω f univ
i : ℕ
⊢ AnalyticOnNhd 𝕜 (fun x => ftaylorSeriesWithin 𝕜 f univ x i) univ

Tactic:
rw [← analyticOn_univ]

Result:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
H : ContDiffOn 𝕜 ω f univ
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => ftaylorSeriesWithin 𝕜 f univ x i) univ

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ ↔ ContDiff 𝕜 (↑n) f

Tactic:
constructor

Result:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ → ContDiff 𝕜 (↑n) f

case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f → ContDiffOn 𝕜 (↑n) f univ

Proof state:
case mpr.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpTo (↑n) f p
x : E
a✝ : x ∈ univ
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[insert x univ] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u

Tactic:
exact ⟨univ, Filter.univ_sets _, p,
  (hp.hasFTaylorSeriesUpToOn univ).of_le (mod_cast hm)⟩

Result:
no goals

Proof state:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
H : ContDiffOn 𝕜 (↑n) f univ
⊢ HasFTaylorSeriesUpToOn (↑n) f (ftaylorSeriesWithin 𝕜 f univ) univ

Tactic:
exact H.ftaylorSeriesWithin uniqueDiffOn_univ

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
⊢ ContDiffOn 𝕜 ω f univ ↔ ContDiff 𝕜 ω f

Tactic:
constructor

Result:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
⊢ ContDiffOn 𝕜 ω f univ → ContDiff 𝕜 ω f

case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
⊢ ContDiff 𝕜 ω f → ContDiffOn 𝕜 ω f univ

Proof state:
case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
⊢ ContDiff 𝕜 ω f → ContDiffOn 𝕜 ω f univ

Tactic:
rintro ⟨p, hp, h'p⟩ x _

Result:
case mpr.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpTo ω f p
h'p : ∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun x => p x i) univ
x : E
a✝ : x ∈ univ
⊢ ContDiffWithinAt 𝕜 ω f univ x

Proof state:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
H : ContDiffOn 𝕜 (↑n) f univ
⊢ ContDiff 𝕜 (↑n) f

Tactic:
use ftaylorSeriesWithin 𝕜 f univ

Result:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
H : ContDiffOn 𝕜 (↑n) f univ
⊢ HasFTaylorSeriesUpTo (↑n) f (ftaylorSeriesWithin 𝕜 f univ)

Proof state:
case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f → ContDiffOn 𝕜 (↑n) f univ

Tactic:
rintro ⟨p, hp⟩ x _ m hm

Result:
case mpr.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpTo (↑n) f p
x : E
a✝ : x ∈ univ
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[insert x univ] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u

Proof state:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
H : ContDiffOn 𝕜 ω f univ
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => ftaylorSeriesWithin 𝕜 f univ x i) univ

Tactic:
exact H.analyticOn.iteratedFDerivWithin uniqueDiffOn_univ _

Result:
no goals

Proof state:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
H : ContDiffOn 𝕜 (↑n) f univ
⊢ HasFTaylorSeriesUpTo (↑n) f (ftaylorSeriesWithin 𝕜 f univ)

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff]

Result:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : WithTop ℕ∞
n : ℕ∞
H : ContDiffOn 𝕜 (↑n) f univ
⊢ HasFTaylorSeriesUpToOn (↑n) f (ftaylorSeriesWithin 𝕜 f univ) univ