-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiffOn_succ_iff_derivWithin (hs : UniqueDiffOn 𝕜 s₂) :
    ContDiffOn 𝕜 (n + 1) f₂ s₂ ↔
      DifferentiableOn 𝕜 f₂ s₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧
        ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
⊢ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂ ↔
    (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
⊢ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂ →
    (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
⊢ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂ →
    (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂
x : 𝕜
⊢ derivWithin f₂ s₂ x = ((fun u => u 1) ∘ fderivWithin 𝕜 f₂ s₂) x

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂
⊢ derivWithin f₂ s₂ = (fun u => u 1) ∘ fderivWithin 𝕜 f₂ s₂

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂
x : 𝕜
⊢ derivWithin f₂ s₂ x = ((fun u => u 1) ∘ fderivWithin 𝕜 f₂ s₂) x

Proof state:
case h.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂
x : 𝕜
⊢ (fderivWithin 𝕜 f₂ s₂ x) 1 = ((smulRight 1 ∘ derivWithin f₂ s₂) x) 1

Tactic:
simp [derivWithin]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂
this : fderivWithin 𝕜 f₂ s₂ = smulRight 1 ∘ derivWithin f₂ s₂
⊢ ContDiff 𝕜 n (smulRight 1)

Tactic:
have : IsBoundedBilinearMap 𝕜 fun _ : (𝕜 →L[𝕜] 𝕜) × F => _ := isBoundedBilinearMap_smulRight

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂
this✝ : fderivWithin 𝕜 f₂ s₂ = smulRight 1 ∘ derivWithin f₂ s₂
this : IsBoundedBilinearMap 𝕜 fun x => x.1.smulRight x.2
⊢ ContDiff 𝕜 n (smulRight 1)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂
this✝ : fderivWithin 𝕜 f₂ s₂ = smulRight 1 ∘ derivWithin f₂ s₂
this : IsBoundedBilinearMap 𝕜 fun x => x.1.smulRight x.2
⊢ ContDiff 𝕜 n (smulRight 1)

Tactic:
exact (this.isBoundedLinearMap_right _).contDiff

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂
this : derivWithin f₂ s₂ = (fun u => u 1) ∘ fderivWithin 𝕜 f₂ s₂
⊢ ContDiff 𝕜 n fun u => u 1

Tactic:
exact (isBoundedBilinearMap_apply.isBoundedLinearMap_left _).contDiff

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂
⊢ fderivWithin 𝕜 f₂ s₂ = smulRight 1 ∘ derivWithin f₂ s₂

Tactic:
ext x

Result:
case h.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂
x : 𝕜
⊢ (fderivWithin 𝕜 f₂ s₂ x) 1 = ((smulRight 1 ∘ derivWithin f₂ s₂) x) 1

Proof state:
case mpr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂
this : fderivWithin 𝕜 f₂ s₂ = smulRight 1 ∘ derivWithin f₂ s₂
⊢ ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂

Tactic:
simp only [this]

Result:
case mpr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂
this : fderivWithin 𝕜 f₂ s₂ = smulRight 1 ∘ derivWithin f₂ s₂
⊢ ContDiffOn 𝕜 n (smulRight 1 ∘ derivWithin f₂ s₂) s₂

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
⊢ DifferentiableOn 𝕜 f₂ s₂ →
    ((n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂ ↔
      (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂)

Tactic:
intro _

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
⊢ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂ ↔
    (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂