-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem AnalyticOn.contDiffOn (h : AnalyticOn 𝕜 f s) (hs : UniqueDiffOn 𝕜 s) :
    ContDiffOn 𝕜 n f s

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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 n f s

Tactic:
suffices ContDiffOn 𝕜 ω f s from this.of_le le_top

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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 ω f s

Proof state:
case 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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p s ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) s
⊢ ContDiffOn 𝕜 ω f s

Tactic:
intro x hx

Result:
case 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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p s ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 ω f s x

Proof state:
case 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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p s ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) s
x : E
hx : x ∈ s
⊢ s ∈ 𝓝[s] x

Tactic:
exact self_mem_nhdsWithin

Result:
no goals

Proof state:
case 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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p s ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) s
x : E
hx : x ∈ s
⊢ s ∈ 𝓝[insert x s] x

Tactic:
rw [insert_eq_of_mem hx]

Result:
case 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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p s ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) s
x : E
hx : x ∈ s
⊢ s ∈ 𝓝[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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 ω f s

Tactic:
rcases h.exists_hasFTaylorSeriesUpToOn hs with ⟨p, hp⟩

Result:
case 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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p s ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) s
⊢ ContDiffOn 𝕜 ω f s

Proof state:
case 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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p s ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
refine ⟨s, ?_, p, hp⟩

Result:
case 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
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p s ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) s
x : E
hx : x ∈ s
⊢ s ∈ 𝓝[insert x s] x