awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n_1 : ℕ∞ω
n : ℕ∞
mp : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ → ContDiff 𝕜 (↑n : ℕ∞ω) f
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ ↔ ContDiff 𝕜 (↑n : ℕ∞ω) f
have mpr : ContDiff 𝕜 (↑n : ℕ∞ω) f → ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n_1 : ℕ∞ω
n : ℕ∞
H : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f
have h : HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f univ)
Tactic: use ftaylorSeriesWithin 𝕜 f univ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n_1 : ℕ∞ω
n : ℕ∞
H : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ
⊢ HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f univ)
have h : HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f univ) univ
Tactic: rw [← hasFTaylorSeriesUpToOn_univ_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
⊢ ContDiff 𝕜 0 f ↔
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      f
have rw : ContDiffOn 𝕜 0 f univ ↔ ContinuousOn f univ
Tactic: rw [← contDiffOn_univ, ← continuousOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
⊢ ContDiffAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑0 : ℕ∞ω) 1) f x ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
have simp_rw : (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑0 : ℕ∞ω) f' x) ↔
  ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
Tactic: simp_rw [contDiffAt_succ_iff_hasFDerivAt, show ((0 : ℕ) : ℕ∞ω) = 0 from rfl,
    contDiffAt_zero, exists_mem_and_iff antitone_bforall antitone_continuousOn, and_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
simp_rw :
  (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑0 : ℕ∞ω) f' x) ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
⊢ ContDiffAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑0 : ℕ∞ω) 1) f x ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
have simp_rw₁ : (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 0 f' x) ↔
  ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
Tactic: simp_rw [contDiffAt_succ_iff_hasFDerivAt, show ((0 : ℕ) : ℕ∞ω) = 0 from rfl,
    contDiffAt_zero, exists_mem_and_iff antitone_bforall antitone_continuousOn, and_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
simp_rw :
  (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑0 : ℕ∞ω) f' x) ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
simp_rw₁ :
  (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 0 f' x) ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
⊢ ContDiffAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑0 : ℕ∞ω) 1) f x ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
have simp_rw₂ : (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ∃ u ∈ 𝓝 x, ContinuousOn f' u) ↔
  ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
Tactic: simp_rw [contDiffAt_succ_iff_hasFDerivAt, show ((0 : ℕ) : ℕ∞ω) = 0 from rfl,
    contDiffAt_zero, exists_mem_and_iff antitone_bforall antitone_continuousOn, and_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
simp_rw :
  (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑0 : ℕ∞ω) f' x) ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
simp_rw₁ :
  (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 0 f' x) ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
simp_rw₂ :
  (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ∃ u ∈ 𝓝 x, ContinuousOn f' u) ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
⊢ ContDiffAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑0 : ℕ∞ω) 1) f x ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
have simp_rw₃ : (∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, (∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContinuousOn f' u) ↔
  ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
Tactic: simp_rw [contDiffAt_succ_iff_hasFDerivAt, show ((0 : ℕ) : ℕ∞ω) = 0 from rfl,
    contDiffAt_zero, exists_mem_and_iff antitone_bforall antitone_continuousOn, and_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContDiff 𝕜 (↑m : ℕ∞ω) f
have simp_rw : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContDiffOn 𝕜 (↑m : ℕ∞ω) f univ
Tactic: simp_rw [← contDiffOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
⊢ ContDiff 𝕜 1 f ↔
    ∃ (f' : E → E →L[𝕜] F),
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x
have h : ∀ (x : E → E →L[𝕜] F), Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] x ↔ ContDiff 𝕜 (↑0 : ℕ∞ω) x
Tactic: convert! contDiff_succ_iff_hasFDerivAt using 4
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
hf : AnalyticOn 𝕜 f univ
⊢ ContDiff 𝕜 n f
have rw : ContDiffOn 𝕜 n f univ
Tactic: rw [← contDiffOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
h : ContDiff 𝕜 ω f
⊢ AnalyticOnNhd 𝕜 f s
have h₁ : ContDiffOn 𝕜 ω f univ
Tactic: rw [← contDiffOn_univ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
h : ContDiffOn 𝕜 ω f univ
⊢ AnalyticOnNhd 𝕜 f s
have this : AnalyticOn 𝕜 f univ
Tactic: have := h.analyticOn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
h : ContDiffOn 𝕜 ω f univ
this : AnalyticOn 𝕜 f univ
⊢ AnalyticOnNhd 𝕜 f s
have this₁ : AnalyticOnNhd 𝕜 f univ
Tactic: rw [analyticOn_univ] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
hf : ContDiff 𝕜 n f
⊢ HasFTaylorSeriesUpTo n f (_root_.ftaylorSeries 𝕜 f)
have simp : ∀ (hf : ContDiffOn 𝕜 n f univ), HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f univ) univ
Tactic: simp only [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]
    at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f ↔ HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeries 𝕜 f)
have mp : ContDiff 𝕜 (↑n : ℕ∞ω) f → HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeries 𝕜 f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
mp : ContDiff 𝕜 (↑n : ℕ∞ω) f → HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeries 𝕜 f)
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f ↔ HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeries 𝕜 f)
have mpr : HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeries 𝕜 f) → ContDiff 𝕜 (↑n : ℕ∞ω) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f → HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeries 𝕜 f)
have mp : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ → HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f univ) univ
Tactic: rw [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f ↔
    (∀ m ≤ n, Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ iteratedFDeriv 𝕜 m f x) ∧
      ∀ m < n,
        Differentiable 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
          iteratedFDeriv 𝕜 m f x
have rw : ((∀ (m : ℕ),
      LE.le (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) →
        Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ iteratedFDeriv 𝕜 m f x) ∧
    ∀ (m : ℕ),
      LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) →
        Differentiable 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
          iteratedFDeriv 𝕜 m f x) ↔
  (∀ m ≤ n, Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ iteratedFDeriv 𝕜 m f x) ∧
    ∀ m < n,
      Differentiable 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
        iteratedFDeriv 𝕜 m f x
Tactic: rw [← WithTop.coe_natCast, contDiff_iff_continuous_differentiable]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
⊢ ContDiff 𝕜 1 f ↔ Differentiable 𝕜 f ∧ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv 𝕜 f)
have rw : Differentiable 𝕜 f ∧ (Eq (α := ℕ∞ω) 0 ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 (F := E →L[𝕜] F) 0 (fderiv 𝕜 f) ↔
  Differentiable 𝕜 f ∧ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv 𝕜 f)
Tactic: rw [← zero_add 1, contDiff_succ_iff_fderiv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Defs (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
⊢ ContDiff 𝕜 ∞ f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 (F := E →L[𝕜] F) ∞ (fderiv 𝕜 f)
have rw : Differentiable 𝕜 f ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 (F := E →L[𝕜] F) ∞ (fderiv 𝕜 f) ↔
  Differentiable 𝕜 f ∧ ContDiff 𝕜 (F := E →L[𝕜] F) (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (fderiv 𝕜 f)
Tactic: rw [← ENat.coe_top_add_one, contDiff_succ_iff_fderiv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ derivWithin f s =
    Function.comp (β := 𝕜 →L[𝕜] F)
      ((⇑(ContinuousLinearEquiv.symm ContinuousLinearMap.toSpanSingletonCLE : (𝕜 →L[𝕜] F) ≃L[𝕜] F) :
          (a : 𝕜 →L[𝕜] F) → F) :
        (a : 𝕜 →L[𝕜] F) → F)
      (fderivWithin 𝕜 f s : (x : 𝕜) → 𝕜 →L[𝕜] F)
have h : ∀ (x : 𝕜),
  derivWithin f s x =
    Function.comp (β := 𝕜 →L[𝕜] F)
      ((⇑(ContinuousLinearEquiv.symm ContinuousLinearMap.toSpanSingletonCLE : (𝕜 →L[𝕜] F) ≃L[𝕜] F) :
          (a : 𝕜 →L[𝕜] F) → F) :
        (a : 𝕜 →L[𝕜] F) → F)
      (fderivWithin 𝕜 f s : (x : 𝕜) → 𝕜 →L[𝕜] F) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (hypothesis)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
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
have this : derivWithin f s =
  Function.comp (β := 𝕜 →L[𝕜] F)
    ((⇑(ContinuousLinearEquiv.symm ContinuousLinearMap.toSpanSingletonCLE : (𝕜 →L[𝕜] F) ≃L[𝕜] F) :
        (a : 𝕜 →L[𝕜] F) → F) :
      (a : 𝕜 →L[𝕜] F) → F)
    (fderivWithin 𝕜 f s : (x : 𝕜) → 𝕜 →L[𝕜] F)
Tactic: have : derivWithin f s =
      ContinuousLinearMap.toSpanSingletonCLE.symm ∘ fderivWithin 𝕜 f s := by
    ext; simp [← fderivWithin_derivWithin]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 1 f s ↔ DifferentiableOn 𝕜 f s ∧ ContinuousOn (derivWithin f s) s
have rw : DifferentiableOn 𝕜 f s ∧ (Eq (α := ℕ∞ω) 0 ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 0 (derivWithin f s) s ↔
  DifferentiableOn 𝕜 f s ∧ ContinuousOn (derivWithin f s) s
Tactic: rw [show (1 : ℕ∞ω) = 0 + 1 from rfl, contDiffOn_succ_iff_derivWithin hs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (derivWithin f s) s
have rw : DifferentiableOn 𝕜 f s ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (derivWithin f s) s ↔
  DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (derivWithin f s) s
Tactic: rw [show ∞ = ∞ + 1 by rfl, contDiffOn_succ_iff_derivWithin hs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (deriv f) s
have rw : DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (derivWithin f s) s ↔
  DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (deriv f) s
Tactic: rw [contDiffOn_succ_iff_derivWithin hs.uniqueDiffOn]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (deriv f) s
have rw : DifferentiableOn 𝕜 f s ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (deriv f) s ↔
  DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (deriv f) s
Tactic: rw [show ∞ = ∞ + 1 by rfl, contDiffOn_succ_iff_deriv_of_isOpen hs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (hypothesis)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hn : 1 ≤ n
⊢ ContinuousOn (derivWithin f s) s
have hn₁ : HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n
Tactic: rw [show (1 : ℕ∞ω) = 0 + 1 from rfl] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (hypothesis)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : IsOpen s
hn : 1 ≤ n
⊢ ContinuousOn (deriv f) s
have hn₁ : HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n
Tactic: rw [show (1 : ℕ∞ω) = 0 + 1 from rfl] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ ContDiff 𝕜 1 f ↔ Differentiable 𝕜 f ∧ Continuous (deriv f)
have rw : Differentiable 𝕜 f ∧ (Eq (α := ℕ∞ω) 0 ω → AnalyticOn 𝕜 f univ) ∧ ContDiff 𝕜 0 (deriv f) ↔
  Differentiable 𝕜 f ∧ Continuous (deriv f)
Tactic: rw [show (1 : ℕ∞ω) = 0 + 1 from rfl, contDiff_succ_iff_deriv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ ContDiff 𝕜 ∞ f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 ∞ (deriv f)
have rw : Differentiable 𝕜 f ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f univ) ∧ ContDiff 𝕜 ∞ (deriv f) ↔
  Differentiable 𝕜 f ∧ ContDiff 𝕜 (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (deriv f)
Tactic: rw [show (∞ : ℕ∞ω) = ∞ + 1 from rfl, contDiff_succ_iff_deriv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (hypothesis)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
h : ContDiff 𝕜 n f
hn : 1 ≤ n
⊢ Continuous (deriv f)
have hn₁ : HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n
Tactic: rw [show (1 : ℕ∞ω) = 0 + 1 from rfl] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
h : ContDiff 𝕜 2 f
⊢ Differentiable 𝕜 (deriv f)
have unfold : Differentiable.{u_1, u_1, u_2} 𝕜 (F := F) fun (x : 𝕜) ↦ ((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1
Tactic: unfold deriv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Deriv (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
h : ContDiff 𝕜 (n + 1) f
⊢ ContDiff 𝕜 n (deriv f)
have unfold : ContDiff.{u_1, u_1, u_2} 𝕜 (F := F) n fun (x : 𝕜) ↦ ((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1
Tactic: unfold deriv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
x : E
hx : x ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (p x 0)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
      (f x))
have rw : Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (p x 0)
  ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
      (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
    (ContinuousMultilinearMap.curry0 (p x 0)))
Tactic: rw [← h.zero_eq x hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn n f p ∅
have zero_eq : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → ContinuousMultilinearMap.curry0 (p x 0) = f x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
zero_eq : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → ContinuousMultilinearMap.curry0 (p x 0) = f x
⊢ HasFTaylorSeriesUpToOn n f p ∅
have fderivWithin : ∀ (m : ℕ),
  (↑m : ℕ∞ω) < n →
    ∀ (x : E),
      Membership.mem (γ := Set E) ∅ x →
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) ∅ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
zero_eq : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → ContinuousMultilinearMap.curry0 (p x 0) = f x
fderivWithin :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) < n →
      ∀ (x : E),
        Membership.mem (γ := Set E) ∅ x →
          HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F)
            (fun (x : E) ↦ p x m) (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) ∅ x
⊢ HasFTaylorSeriesUpToOn n f p ∅
have cont : ∀ (m : ℕ),
  (↑m : ℕ∞ω) ≤ n →
    ContinuousOn (Y := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m) ∅
Tactic: constructor