awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
c : F
zero :
  ∀ (x : E),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (HAdd.hAdd (α := ℕ) 0 1) (fun (x : E) ↦ c) s x) (0 x)
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (HAdd.hAdd (α := ℕ) 0 1) (fun (x : E) ↦ c) s) 0

Tactic:
ext1
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
c : F
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (HAdd.hAdd (α := ℕ) 0 1) (fun (x : E) ↦ c) s x) (0 x)

Tactic:
simp [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp, comp_def]

Premises used: iteratedFDerivWithin_succ_eq_comp_left, Function.comp_def, iteratedFDerivWithin_zero_eq_comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
c : F
n : ℕ
IH :
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ c) s) 0
succ :
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1 + 1)) ↦ E) F)
    (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1 + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin (n + 1 + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1 + 1)) ↦ E) F)
      (fderivWithin 𝕜 0 s))
    0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1 + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1 + 1) (fun (x : E) ↦ c) s) 0

Tactic:
rw [iteratedFDerivWithin_succ_eq_comp_left, IH]

Premises used: iteratedFDerivWithin_succ_eq_comp_left
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
c : F
n : ℕ
IH :
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ c) s) 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1 + 1)) ↦ E) F)
    (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1 + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin (n + 1 + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1 + 1)) ↦ E) F)
      (fderivWithin 𝕜 0 s))
    0

Tactic:
simp only [Pi.zero_def, comp_def, fderivWithin_fun_const, map_zero]

Premises used: map_zero, Pi.zero_def, fderivWithin_fun_const, Function.comp_def
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
n : ℕ
c : F
zero :
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (HAdd.hAdd (α := ℕ) 0 1) (fun (x : E) ↦ c) s) 0
succ :
  ∀ (n : ℕ)
    (IH :
      Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ c) s) 0),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1 + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1 + 1) (fun (x : E) ↦ c) s) 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ c) s) 0

Tactic:
induction n with
  | zero =>
    ext1
    simp [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp, comp_def]
  | succ n IH =>
    rw [iteratedFDerivWithin_succ_eq_comp_left, IH]
    simp only [Pi.zero_def, comp_def, fderivWithin_fun_const, map_zero]

Premises used: iteratedFDerivWithin_succ_eq_comp_left, Fin.succ, map_zero, Pi.zero_def, fderivWithin_fun_const, Function.comp_def, iteratedFDerivWithin_zero_eq_comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
zero :
  ∀ (x : E) (x_1 : (i : Fin 0) → E),
    Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 0 0 s x : (a : (i : Fin 0) → E) → F) x_1 : F)
      ((0 x : (a : (i : Fin 0) → E) → F) x_1 : F)
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 0 s) 0

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
x : E
x_1 : (i : Fin 0) → E
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 0 0 s x : (a : (i : Fin 0) → E) → F) x_1 : F)
    ((0 x : (a : (i : Fin 0) → E) → F) x_1 : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
i : ℕ
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (i + 1) 0 s) 0

Tactic:
apply iteratedFDerivWithin_succ_const

Premises used: iteratedFDerivWithin_succ_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
i : ℕ
zero :
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 0 s) 0
succ :
  ∀ (i : ℕ),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (i + 1) 0 s) 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i 0 s) 0

Tactic:
cases i with
  | zero => ext; simp
  | succ i => apply iteratedFDerivWithin_succ_const

Premises used: Fin.succ, iteratedFDerivWithin_succ_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
i : ℕ
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ 0) s) 0

Tactic:
apply iteratedFDerivWithin_zero

Premises used: iteratedFDerivWithin_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
h :
  ∀ (x : Set E) (x_1 : E) (n : ℕ) (x_2 : (i : Fin n) → E),
    Eq.{u_3 + 1} (α := F) ((ftaylorSeriesWithin 𝕜 0 x x_1 n : (a : (i : Fin n) → E) → F) x_2 : F)
      ((0 x x_1 n : (a : (i : Fin n) → E) → F) x_2 : F)
⊢ Eq (α := (s : Set E) → (x : E) → FormalMultilinearSeries 𝕜 E F) (ftaylorSeriesWithin 𝕜 0) 0

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : Set E
x_1 : E
n : ℕ
x_2 : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F) ((ftaylorSeriesWithin 𝕜 0 x x_1 n : (a : (i : Fin n) → E) → F) x_2 : F)
    ((0 x x_1 n : (a : (i : Fin n) → E) → F) x_2 : F)

Tactic:
simp [ftaylorSeriesWithin]

Premises used: ftaylorSeriesWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ Eq (α := (s : Set E) → (x : E) → FormalMultilinearSeries 𝕜 E F) (ftaylorSeriesWithin 𝕜 fun (x : E) ↦ 0) 0

Tactic:
apply ftaylorSeriesWithin_zero

Premises used: ftaylorSeriesWithin_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n 0 x) (0 x)

Tactic:
simp only [← iteratedFDerivWithin_univ, iteratedFDerivWithin_zero]

Premises used: iteratedFDerivWithin_zero, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv 𝕜 n fun (x : E) ↦ 0) 0

Tactic:
apply iteratedFDeriv_zero

Premises used: iteratedFDeriv_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
h :
  ∀ (x : E) (n : ℕ) (x_1 : (i : Fin n) → E),
    Eq.{u_3 + 1} (α := F) ((ftaylorSeries 𝕜 0 x n : (a : (i : Fin n) → E) → F) x_1 : F)
      ((0 x n : (a : (i : Fin n) → E) → F) x_1 : F)
⊢ Eq (α := (x : E) → FormalMultilinearSeries 𝕜 E F) (ftaylorSeries 𝕜 0) 0

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ
x_1 : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F) ((ftaylorSeries 𝕜 0 x n : (a : (i : Fin n) → E) → F) x_1 : F)
    ((0 x n : (a : (i : Fin n) → E) → F) x_1 : F)

Tactic:
simp [ftaylorSeries]

Premises used: ftaylorSeries
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
h :
  ∀ (x : E) (n : ℕ) (x_1 : (i : Fin n) → E),
    Eq.{u_3 + 1} (α := F) ((ftaylorSeries 𝕜 (fun (x : E) ↦ 0) x n : (a : (i : Fin n) → E) → F) x_1 : F)
      ((0 x n : (a : (i : Fin n) → E) → F) x_1 : F)
⊢ Eq (α := (x : E) → FormalMultilinearSeries 𝕜 E F) (ftaylorSeries 𝕜 fun (x : E) ↦ 0) 0

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ
x_1 : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F) ((ftaylorSeries 𝕜 (fun (x : E) ↦ 0) x n : (a : (i : Fin n) → E) → F) x_1 : F)
    ((0 x n : (a : (i : Fin n) → E) → F) x_1 : F)

Tactic:
simp [ftaylorSeries]

Premises used: ftaylorSeries
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (F := F) n fun (x : E) ↦ 0

Tactic:
analyticOnNhd_const.contDiff

Premises used: AnalyticOnNhd.contDiff, analyticOnNhd_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
c : F
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (F := F) n fun (x : E) ↦ c

Tactic:
analyticOnNhd_const.contDiff

Premises used: AnalyticOnNhd.contDiff, analyticOnNhd_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
c : F
s : Set E
⊢ ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ c) s

Tactic:
contDiff_const.contDiffOn

Premises used: ContDiff.contDiffOn, contDiff_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
c : F
⊢ ContDiffAt.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ c) x

Tactic:
contDiff_const.contDiffAt

Premises used: contDiff_const, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
x : E
n : ℕ∞ω
c : F
⊢ ContDiffWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ c) s x

Tactic:
contDiffAt_const.contDiffWithinAt

Premises used: contDiffAt_const, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
inst_5 : Subsingleton F
rw : ContDiff.{u_1, u_2, u_3} 𝕜 (F := F) n fun (x : E) ↦ 0
⊢ ContDiff 𝕜 n f

Tactic:
rw [Subsingleton.elim f fun _ => 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
inst_5 : Subsingleton F
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (F := F) n fun (x : E) ↦ 0

Tactic:
contDiff_const

Premises used: contDiff_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
inst_5 : Subsingleton F
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (F := F) n fun (x : E) ↦ 0

Tactic:
exact contDiff_const

Premises used: contDiff_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
inst_5 : Subsingleton F
rw : ContDiffAt.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ 0) x
⊢ ContDiffAt 𝕜 n f x

Tactic:
rw [Subsingleton.elim f fun _ => 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
inst_5 : Subsingleton F
⊢ ContDiffAt.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ 0) x

Tactic:
contDiffAt_const

Premises used: contDiffAt_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
inst_5 : Subsingleton F
⊢ ContDiffAt.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ 0) x

Tactic:
exact contDiffAt_const

Premises used: contDiffAt_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
inst_5 : Subsingleton F
rw : ContDiffWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ 0) s x
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
rw [Subsingleton.elim f fun _ => 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
inst_5 : Subsingleton F
⊢ ContDiffWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ 0) s x

Tactic:
contDiffWithinAt_const

Premises used: contDiffWithinAt_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
inst_5 : Subsingleton F
⊢ ContDiffWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ 0) s x

Tactic:
exact contDiffWithinAt_const

Premises used: contDiffWithinAt_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
inst_5 : Subsingleton F
rw : ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ 0) s
⊢ ContDiffOn 𝕜 n f s

Tactic:
rw [Subsingleton.elim f fun _ => 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
inst_5 : Subsingleton F
⊢ ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ 0) s

Tactic:
contDiffOn_const

Premises used: contDiffOn_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
inst_5 : Subsingleton F
⊢ ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ 0) s

Tactic:
exact contDiffOn_const

Premises used: contDiffOn_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
c : F
s : Set E
hn : Ne (α := ℕ) 0 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDerivWithin 𝕜 0 (fun (x : E) ↦ c) s) 0

Tactic:
contradiction
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
c : F
s : Set E
n : ℕ
hn : n + 1 ≠ 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ c) s) 0

Tactic:
iteratedFDerivWithin_succ_const n c

Premises used: iteratedFDerivWithin_succ_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
c : F
s : Set E
n : ℕ
hn : n + 1 ≠ 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ c) s) 0

Tactic:
exact iteratedFDerivWithin_succ_const n c

Premises used: iteratedFDerivWithin_succ_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
hn : n ≠ 0
c : F
s : Set E
zero :
  ∀ (hn : Ne (α := ℕ) 0 0),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (iteratedFDerivWithin 𝕜 0 (fun (x : E) ↦ c) s) 0
succ :
  ∀ (n : ℕ) (hn : n + 1 ≠ 0),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ c) s) 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ c) s) 0

Tactic:
cases n with
  | zero => contradiction
  | succ n => exact iteratedFDerivWithin_succ_const n c

Premises used: Fin.succ, iteratedFDerivWithin_succ_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
hn : n ≠ 0
c : F
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv 𝕜 n fun (x : E) ↦ c) 0

Tactic:
simp only [← iteratedFDerivWithin_univ, iteratedFDerivWithin_const_of_ne hn]

Premises used: iteratedFDerivWithin_const_of_ne, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : F
⊢ n + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
⊢ ∀ (y : E), Membership.mem (γ := Set E) {x} y → f y = f x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
hf : IsBoundedLinearMap 𝕜 f
⊢ ContDiff 𝕜 n f

Tactic:
(ContinuousLinearMap.analyticOnNhd hf.toContinuousLinearMap univ).contDiff

Premises used: Set.univ, IsBoundedLinearMap.toContinuousLinearMap, AnalyticOnNhd.contDiff, ContinuousLinearMap.analyticOnNhd