-- 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:
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₂

Tactic:
apply ContDiff.comp_contDiffOn _ h

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₂
⊢ ContDiff 𝕜 n (smulRight 1)

Proof state:
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₂

Tactic:
rintro ⟨h', h⟩

Result:
case mp.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 (fderivWithin 𝕜 f₂ s₂) s₂
⊢ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂

Proof state:
case mp.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 (fderivWithin 𝕜 f₂ s₂) s₂
this : derivWithin f₂ s₂ = (fun u => u 1) ∘ fderivWithin 𝕜 f₂ s₂
⊢ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂

Tactic:
simp_rw [this]

Result:
case mp.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 (fderivWithin 𝕜 f₂ s₂) s₂
this : derivWithin f₂ s₂ = (fun u => u 1) ∘ fderivWithin 𝕜 f₂ s₂
⊢ ContDiffOn 𝕜 n ((fun u => u 1) ∘ fderivWithin 𝕜 f₂ s₂) s₂

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₂
⊢ ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂

Tactic:
have : fderivWithin 𝕜 f₂ s₂ = smulRight (1 : 𝕜 →L[𝕜] 𝕜) ∘ derivWithin f₂ s₂ := by
  ext x; simp [derivWithin]

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 (fderivWithin 𝕜 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₂
⊢ ContDiffOn 𝕜 (n + 1) f₂ s₂ ↔
    DifferentiableOn 𝕜 f₂ s₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂

Tactic:
rw [contDiffOn_succ_iff_fderivWithin hs, and_congr_right_iff]

Result:
𝕜 : 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₂)

Proof state:
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₂

Tactic:
rintro ⟨h', h⟩

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₂
⊢ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂

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₂
⊢ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂

Tactic:
refine ⟨h', ?_⟩

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₂
⊢ ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂

Proof state:
case mp.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 (fderivWithin 𝕜 f₂ s₂) s₂
⊢ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂

Tactic:
refine ⟨h', ?_⟩

Result:
case mp.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 (fderivWithin 𝕜 f₂ s₂) s₂
⊢ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂

Proof state:
case mp.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 (fderivWithin 𝕜 f₂ s₂) s₂
this : derivWithin f₂ s₂ = (fun u => u 1) ∘ fderivWithin 𝕜 f₂ s₂
⊢ ContDiffOn 𝕜 n ((fun u => u 1) ∘ fderivWithin 𝕜 f₂ s₂) s₂

Tactic:
apply ContDiff.comp_contDiffOn _ h

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 (fderivWithin 𝕜 f₂ s₂) s₂
this : derivWithin f₂ s₂ = (fun u => u 1) ∘ fderivWithin 𝕜 f₂ s₂
⊢ ContDiff 𝕜 n fun u => u 1