-- Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean
theorem CPolynomialOn.contDiffOn (h : CPolynomialOn 𝕜 f s) {n : WithTop ℕ∞} :
    ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : WithTop ℕ∞
t : Set E := {x | CPolynomialAt 𝕜 f x}
H : CPolynomialOn 𝕜 f t
⊢ AnalyticOnNhd 𝕜 f t

Tactic:
exact H.analyticOnNhd

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : WithTop ℕ∞
t : Set E := {x | CPolynomialAt 𝕜 f x}
this : AnalyticOnNhd 𝕜 f t
⊢ ContDiffOn 𝕜 n f t

Tactic:
have t_open : IsOpen t := isOpen_cPolynomialAt 𝕜 f

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : WithTop ℕ∞
t : Set E := {x | CPolynomialAt 𝕜 f x}
this : AnalyticOnNhd 𝕜 f t
t_open : IsOpen t
⊢ ContDiffOn 𝕜 n f t

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : WithTop ℕ∞
t : Set E := {x | CPolynomialAt 𝕜 f x}
⊢ AnalyticOnNhd 𝕜 f t

Tactic:
have H : CPolynomialOn 𝕜 f t := fun _x hx ↦ hx

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : WithTop ℕ∞
t : Set E := {x | CPolynomialAt 𝕜 f x}
H : CPolynomialOn 𝕜 f t
⊢ AnalyticOnNhd 𝕜 f t

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : WithTop ℕ∞
t : Set E := {x | CPolynomialAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f t

Tactic:
suffices AnalyticOnNhd 𝕜 f t by
  have t_open : IsOpen t := isOpen_cPolynomialAt 𝕜 f
  exact AnalyticOnNhd.contDiffOn this t_open.uniqueDiffOn

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : WithTop ℕ∞
t : Set E := {x | CPolynomialAt 𝕜 f x}
⊢ AnalyticOnNhd 𝕜 f t

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : WithTop ℕ∞
t : Set E := {x | CPolynomialAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f s

Tactic:
suffices ContDiffOn 𝕜 n f t from this.mono h

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : WithTop ℕ∞
t : Set E := {x | CPolynomialAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f t

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : WithTop ℕ∞
⊢ ContDiffOn 𝕜 n f s

Tactic:
let t := { x | CPolynomialAt 𝕜 f x }

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : WithTop ℕ∞
t : Set E := {x | CPolynomialAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : WithTop ℕ∞
t : Set E := {x | CPolynomialAt 𝕜 f x}
this : AnalyticOnNhd 𝕜 f t
t_open : IsOpen t
⊢ ContDiffOn 𝕜 n f t

Tactic:
exact AnalyticOnNhd.contDiffOn this t_open.uniqueDiffOn

Result:
no goals