awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
simp : ∀ (hf : ContDiffOn 𝕜 n f univ), HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f univ) univ
⊢ HasFTaylorSeriesUpTo n f (_root_.ftaylorSeries 𝕜 f)

Tactic:
simp only [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]
    at hf ⊢

Premises used: hasFTaylorSeriesUpToOn_univ_iff, ftaylorSeriesWithin_univ, contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ContDiffOn 𝕜 n f univ
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f univ) univ

Tactic:
ContDiffOn.ftaylorSeriesWithin hf uniqueDiffOn_univ

Premises used: uniqueDiffOn_univ, ContDiffOn.ftaylorSeriesWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ContDiffOn 𝕜 n f univ
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f univ) univ

Tactic:
exact ContDiffOn.ftaylorSeriesWithin hf uniqueDiffOn_univ

Premises used: uniqueDiffOn_univ, ContDiffOn.ftaylorSeriesWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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)
mpr : HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeries 𝕜 f) → ContDiff 𝕜 (↑n : ℕ∞ω) f
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f ↔ HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeries 𝕜 f)

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ → HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f univ) univ
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f → HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeries 𝕜 f)

Tactic:
rw [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]

Premises used: hasFTaylorSeriesUpToOn_univ_iff, ftaylorSeriesWithin_univ, contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ → HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f univ) univ

Tactic:
fun h ↦ ContDiffOn.ftaylorSeriesWithin h uniqueDiffOn_univ

Premises used: uniqueDiffOn_univ, ContDiffOn.ftaylorSeriesWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ → HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f univ) univ

Tactic:
exact fun h ↦ ContDiffOn.ftaylorSeriesWithin h uniqueDiffOn_univ

Premises used: uniqueDiffOn_univ, ContDiffOn.ftaylorSeriesWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞
⊢ HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeries 𝕜 f) → ContDiff 𝕜 (↑n : ℕ∞ω) f

Tactic:
fun h ↦ ⟨ftaylorSeries 𝕜 f, h⟩

Premises used: ftaylorSeries, ContDiff, Exists.intro
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞
⊢ HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeries 𝕜 f) → ContDiff 𝕜 (↑n : ℕ∞ω) f

Tactic:
exact fun h ↦ ⟨ftaylorSeries 𝕜 f, h⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 →
          Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ iteratedFDeriv 𝕜 m f x) ∧
      ∀ (m : ℕ),
        (↑m : ℕ∞) < n →
          Differentiable 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
            iteratedFDeriv 𝕜 m f x

Tactic:
simp [contDiffOn_univ.symm, continuousOn_univ, differentiableOn_univ.symm,
    iteratedFDerivWithin_univ, contDiffOn_iff_continuousOn_differentiableOn uniqueDiffOn_univ]

Premises used: contDiffOn_iff_continuousOn_differentiableOn, differentiableOn_univ, uniqueDiffOn_univ, continuousOn_univ, contDiffOn_univ, Iff.symm, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ
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
⊢ 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

Tactic:
rw [← WithTop.coe_natCast, contDiff_iff_continuous_differentiable]

Premises used: contDiff_iff_continuous_differentiable, WithTop.coe_natCast
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ
⊢ ((∀ (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:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞ω
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
hf : ContDiff 𝕜 n f
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ iteratedFDeriv 𝕜 m f x

Tactic:
(contDiff_iff_continuous_differentiable.mp (hf.of_le hm)).1 m le_rfl

Premises used: le_rfl, contDiff_iff_continuous_differentiable, ContDiff.of_le, And.left, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
m : ℕ
hf : ContDiff 𝕜 (↑m : ℕ∞ω) f
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦ iteratedFDeriv 𝕜 m f x

Tactic:
(contDiff_iff_continuous_differentiable.mp hf).1 m le_rfl

Premises used: le_rfl, contDiff_iff_continuous_differentiable, And.left, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞ω
m : ℕ
hm : (↑m : ℕ∞ω) < n
hf : ContDiff 𝕜 n f
⊢ Differentiable 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
    iteratedFDeriv 𝕜 m f x

Tactic:
(contDiff_iff_continuous_differentiable.mp
    (hf.of_le (ENat.add_one_natCast_le_withTop_of_lt hm))).2 m (mod_cast lt_add_one m)

Premises used: ENat.add_one_natCast_le_withTop_of_lt, Nat.cast_lt._simp_1, lt_add_one, cast, contDiff_iff_continuous_differentiable, ContDiff.of_le, And.right, Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞
h :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ n →
      Differentiable 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m f)
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f

Tactic:
contDiff_iff_continuous_differentiable.2
    ⟨fun m hm => (h m hm).continuous, fun m hm => h m (le_of_lt hm)⟩

Premises used: Iff.mpr, le_of_lt, contDiff_iff_continuous_differentiable, And.intro, Differentiable.continuous
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 + 1) f ↔
    Differentiable 𝕜 f ∧ (n = ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 (F := E →L[𝕜] F) n (fderiv 𝕜 f)

Tactic:
simp only [← contDiffOn_univ, ← differentiableOn_univ, ← fderivWithin_univ,
    contDiffOn_succ_iff_fderivWithin uniqueDiffOn_univ, analyticOn_univ]

Premises used: differentiableOn_univ, fderivWithin_univ, uniqueDiffOn_univ, analyticOn_univ, contDiffOn_succ_iff_fderivWithin, contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
rw :
  Differentiable 𝕜 f ∧ (Eq (α := ℕ∞ω) 0 ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 (F := E →L[𝕜] F) 0 (fderiv 𝕜 f) ↔
    Differentiable 𝕜 f ∧ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv 𝕜 f)
⊢ ContDiff 𝕜 1 f ↔ Differentiable 𝕜 f ∧ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv 𝕜 f)

Tactic:
rw [← zero_add 1, contDiff_succ_iff_fderiv]

Premises used: contDiff_succ_iff_fderiv, zero_add, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ Differentiable 𝕜 f ∧ (Eq (α := ℕ∞ω) 0 ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 (F := E →L[𝕜] F) 0 (fderiv 𝕜 f) ↔
    Differentiable 𝕜 f ∧ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv 𝕜 f)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
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)
⊢ ContDiff 𝕜 ∞ f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 (F := E →L[𝕜] F) ∞ (fderiv 𝕜 f)

Tactic:
rw [← ENat.coe_top_add_one, contDiff_succ_iff_fderiv]

Premises used: ENat.coe_top_add_one, contDiff_succ_iff_fderiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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
⊢ 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:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞ω
h : ContDiff 𝕜 n f
hn : n ≠ 0
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv 𝕜 f)

Tactic:
(contDiff_one_iff_fderiv.1 (h.of_le <| ENat.one_le_iff_ne_zero_withTop.mpr hn)).2

Premises used: Iff.mpr, contDiff_one_iff_fderiv, ENat.one_le_iff_ne_zero_withTop, ContDiff.of_le, And.right, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
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 : ℕ∞ω
h : ContDiff 𝕜 n f
hn : n ≠ 0
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : E × E) ↦
    (fderiv 𝕜 f p.1 : (a : E) → F) p.2

Tactic:
have A : Continuous fun q : (E →L[𝕜] F) × E => q.1 q.2 := isBoundedBilinearMap_apply.continuous
  have B : Continuous fun p : E × E => (fderiv 𝕜 f p.1, p.2) :=
    ((h.continuous_fderiv hn).comp continuous_fst).prodMk continuous_snd
  A.comp B

Premises used: Continuous.comp, ContDiff.continuous_fderiv, continuous_snd, continuous_fst, IsBoundedBilinearMap.continuous, isBoundedBilinearMap_apply, Continuous.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
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
⊢ 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:
ext
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
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:
simp [← fderivWithin_derivWithin]

Premises used: fderivWithin_derivWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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)

Tactic:
have : derivWithin f s =
      ContinuousLinearMap.toSpanSingletonCLE.symm ∘ fderivWithin 𝕜 f s := by
    ext; simp [← fderivWithin_derivWithin]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
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)
⊢ ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (derivWithin f s) s

Tactic:
simp [contDiffOn_succ_iff_fderivWithin hs, this, ContinuousLinearEquiv.comp_contDiffOn_iff]

Premises used: ContinuousLinearEquiv.comp_contDiffOn_iff, contDiffOn_succ_iff_fderivWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
rw :
  DifferentiableOn 𝕜 f s ∧ (Eq (α := ℕ∞ω) 0 ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 0 (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContinuousOn (derivWithin f s) s
⊢ ContDiffOn 𝕜 1 f s ↔ DifferentiableOn 𝕜 f s ∧ ContinuousOn (derivWithin f s) s

Tactic:
rw [show (1 : ℕ∞ω) = 0 + 1 from rfl, contDiffOn_succ_iff_derivWithin hs]

Premises used: contDiffOn_succ_iff_derivWithin, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
⊢ DifferentiableOn 𝕜 f s ∧ (Eq (α := ℕ∞ω) 0 ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 0 (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContinuousOn (derivWithin f s) s

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
⊢ ∞ = HAdd.hAdd (α := ℕ∞ω) ∞ 1

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
rw :
  DifferentiableOn 𝕜 f s ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (derivWithin f s) s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (derivWithin f s) s

Tactic:
rw [show ∞ = ∞ + 1 by rfl, contDiffOn_succ_iff_derivWithin hs]

Premises used: contDiffOn_succ_iff_derivWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
⊢ DifferentiableOn 𝕜 f s ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (derivWithin f s) s

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
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
⊢ ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (deriv f) s

Tactic:
rw [contDiffOn_succ_iff_derivWithin hs.uniqueDiffOn]

Premises used: contDiffOn_succ_iff_derivWithin, IsOpen.uniqueDiffOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
⊢ 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:
Iff.rfl.and (Iff.rfl.and (contDiffOn_congr fun _ => derivWithin_of_isOpen hs))

Premises used: contDiffOn_congr, Iff.rfl, Iff.and, derivWithin_of_isOpen
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
⊢ 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:
exact Iff.rfl.and (Iff.rfl.and (contDiffOn_congr fun _ => derivWithin_of_isOpen hs))

Premises used: contDiffOn_congr, Iff.rfl, Iff.and, derivWithin_of_isOpen
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
⊢ ∞ = HAdd.hAdd (α := ℕ∞ω) ∞ 1

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
rw :
  DifferentiableOn 𝕜 f s ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (deriv f) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (deriv f) s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (deriv f) s

Tactic:
rw [show ∞ = ∞ + 1 by rfl, contDiffOn_succ_iff_deriv_of_isOpen hs]

Premises used: contDiffOn_succ_iff_deriv_of_isOpen
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
⊢ DifferentiableOn 𝕜 f s ∧ (Eq (α := ℕ∞ω) ∞ ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (deriv f) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (HAdd.hAdd (α := ℕ∞ω) ∞ 1) (deriv f) s

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
⊢ ContDiffOn 𝕜 m (derivWithin f s) s

Tactic:
((contDiffOn_succ_iff_derivWithin hs).1 (hf.of_le hmn)).2.2

Premises used: ContDiffOn.of_le, And.right, Iff.mp, contDiffOn_succ_iff_derivWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
hf : ContDiffOn 𝕜 n f s
hs : IsOpen s
hmn : m + 1 ≤ n
⊢ ContDiffOn 𝕜 m (deriv f) s

Tactic:
(hf.derivWithin hs.uniqueDiffOn hmn).congr fun _ hx => (derivWithin_of_isOpen hs hx).symm

Premises used: ContDiffOn.congr, ContDiffOn.derivWithin, IsOpen.uniqueDiffOn, Eq.symm, derivWithin_of_isOpen
-- Module: Mathlib.Analysis.Calculus.ContDiff.Deriv
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
⊢ HAdd.hAdd (α := ℕ∞ω) 0 1 ≤ n

Tactic:
rw [show (1 : ℕ∞ω) = 0 + 1 from rfl] at hn

Premises used: rfl