-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffWithinAt.continuousWithinAt (h : ContDiffWithinAt 𝕜 n f s x) :
    ContinuousWithinAt 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
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
⊢ ContinuousWithinAt f s x

Tactic:
have := h.of_le (zero_le _)

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
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
this : ContDiffWithinAt 𝕜 0 f s x
⊢ ContinuousWithinAt f s x

Proof state:
case 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
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
u : Set E
hu : x ∈ u ∧ u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn 0 f p u
⊢ ContinuousWithinAt f s x

Tactic:
exact (H.continuousOn.continuousWithinAt hu.1).mono_of_mem_nhdsWithin hu.2

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
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
this : ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn 0 f p u
⊢ ContinuousWithinAt f s x

Tactic:
rcases this with ⟨u, hu, p, H⟩

Result:
case 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
n : WithTop ℕ∞
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

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
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
this : ContDiffWithinAt 𝕜 0 f s x
⊢ ContinuousWithinAt f s x

Tactic:
simp only [ContDiffWithinAt, nonpos_iff_eq_zero, Nat.cast_eq_zero,
  mem_pure, forall_eq, CharP.cast_eq_zero] at this

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
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
this : ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn 0 f p u
⊢ ContinuousWithinAt f s x

Proof state:
case 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
n : WithTop ℕ∞
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

Tactic:
rw [mem_nhdsWithin_insert] at hu

Result:
case 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
n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
u : Set E
hu : x ∈ u ∧ u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn 0 f p u
⊢ ContinuousWithinAt f s x