-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffWithinAt.of_le (h : ContDiffWithinAt 𝕜 n f s x) (hmn : m ≤ n) :
    ContDiffWithinAt 𝕜 m f s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m✝ n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 ω f s x
m : ℕ∞
hmn : ↑m ≤ ω
k : ℕ
a✝ : ↑k ≤ m
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑k) f p u

Tactic:
obtain ⟨u, hu, p, hp, -⟩ := h

Result:
case intro.intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m✝ n : WithTop ℕ∞
m : ℕ∞
hmn : ↑m ≤ ω
k : ℕ
a✝ : ↑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, HasFTaylorSeriesUpToOn (↑k) f p u

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m n✝ : WithTop ℕ∞
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))

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
s : Set E
f : E → F
x : E
m n : WithTop ℕ∞
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⟩

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
s : Set E
f : E → F
x : E
m n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 ω f s x
hmn : ω ≤ ω
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
exact h

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
s : Set E
f : E → F
x : E
m n✝ : WithTop ℕ∞
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n) f s x
hmn : ω ≤ ↑n
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
simp at hmn

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
s : Set E
f : E → F
x : E
m✝ n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 ω f s x
m : ℕ∞
hmn : ↑m ≤ ω
⊢ ContDiffWithinAt 𝕜 (↑m) f s x

Tactic:
intro k _

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m✝ n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 ω f s x
m : ℕ∞
hmn : ↑m ≤ ω
k : ℕ
a✝ : ↑k ≤ m
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑k) f p u

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m✝ n✝ : WithTop ℕ∞
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))

Result:
no goals

Proof state:
case intro.intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m✝ n : WithTop ℕ∞
m : ℕ∞
hmn : ↑m ≤ ω
k : ℕ
a✝ : ↑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, HasFTaylorSeriesUpToOn (↑k) f p u

Tactic:
exact ⟨u, hu, p, hp.of_le le_top⟩

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
s : Set E
f : E → F
x : E
m n : WithTop ℕ∞
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))

Result:
no goals