awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDerivWithin n f univ x = (fun (g : 𝕜 → F) ↦ derivWithin g univ)^[n] f x

Tactic:
iteratedDerivWithin_eq_iterate (F := F)

Premises used: iteratedDerivWithin_eq_iterate
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
h : ∀ (x : 𝕜 → F), deriv x = derivWithin x univ
⊢ iteratedDerivWithin n f univ x = deriv^[n] f x

Tactic:
convert! iteratedDerivWithin_eq_iterate (F := F)

Premises used: iteratedDerivWithin_eq_iterate
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
x_1 : 𝕜 → F
⊢ deriv x_1 = derivWithin x_1 univ

Tactic:
simp [derivWithin_univ]

Premises used: derivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
simp_rw : ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) = iteratedDeriv n f x
simp_rw₁ :
  Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
    ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
⊢ iteratedDerivWithin n f s x = iteratedDeriv n f x

Tactic:
simp_rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_of_isOpen n hs hx]

Premises used: iteratedFDerivWithin_of_isOpen, iteratedDerivWithin, iteratedDeriv
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
s t : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
r : 𝕜
hr : r ∈ s ∩ t
rw : iteratedDeriv n f r = iteratedDerivWithin n f t r
rw₁ rw₂ : iteratedDeriv n f r = iteratedDeriv n f r
⊢ iteratedDerivWithin n f s r = iteratedDerivWithin n f t r

Tactic:
rw [iteratedDerivWithin_of_isOpen hs hr.1, iteratedDerivWithin_of_isOpen ht hr.2]

Premises used: And.right, And.left, iteratedDerivWithin_of_isOpen
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
apply : EqOn (iteratedDeriv n f) (deriv^[n] f) s
⊢ EqOn (iteratedDerivWithin n f s) (deriv^[n] f) s

Tactic:
apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen hs)

Premises used: Set.EqOn.trans, iteratedDerivWithin_of_isOpen
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
rw : EqOn (deriv^[n] f) (deriv^[n] f) s
⊢ EqOn (iteratedDeriv n f) (deriv^[n] f) s

Tactic:
rw [iteratedDeriv_eq_iterate]

Premises used: iteratedDeriv_eq_iterate
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ EqOn (deriv^[n] f) (deriv^[n] f) s

Tactic:
Set.eqOn_refl _ _

Premises used: Set.eqOn_refl
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ EqOn (deriv^[n] f) (deriv^[n] f) s

Tactic:
exact Set.eqOn_refl _ _

Premises used: Set.eqOn_refl
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
rw : deriv^[n + 1] f = iteratedDeriv n (deriv f)
rw₁ : deriv^[n + 1] f = deriv^[n] (deriv f)
rw₂ rw₃ : deriv^[n] (deriv f) = deriv^[n] (deriv f)
⊢ iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)

Tactic:
rw [iteratedDeriv_eq_iterate, iteratedDeriv_eq_iterate, Function.iterate_succ_apply]

Premises used: iteratedDeriv_eq_iterate, Function.iterate_succ_apply
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
h : AnalyticAt 𝕜 f x
obtain :
  ∀ (p : FormalMultilinearSeries 𝕜 𝕜 𝕜) (hp : HasFPowerSeriesAt f p x),
    HasFPowerSeriesAt (𝕜 := 𝕜) f
      (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f
    (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x

Tactic:
obtain ⟨p, hp⟩ := h
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
hp : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesAt f p x

Tactic:
hp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
hp : HasFPowerSeriesAt f p x
h : (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) = p
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f
    (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) x

Tactic:
convert! hp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
hp : HasFPowerSeriesAt f p x
h :
  ∀ (r : ENNReal) (hpr : HasFPowerSeriesOnBall f p x r),
    (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) = p
⊢ (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) = p

Tactic:
obtain ⟨r, hpr⟩ := hp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
h :
  ∀ (n : ℕ),
    Eq (α := 𝕜)
      ((FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) n :
            (a : (i : Fin n) → 𝕜) → 𝕜)
          fun (x : Fin n) ↦ 1 :
        𝕜)
      ((p n : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1 : 𝕜)
⊢ (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) = p

Tactic:
ext n
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
⊢ ∀ (n : ℕ),
    HSMul.hSMul (β := 𝕜) n.factorial ((p n : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1 : 𝕜) =
      (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1

Tactic:
have h_fact_smul := hpr.factorial_smul 1
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul :
  ∀ (n : ℕ),
    HSMul.hSMul (β := 𝕜) n.factorial ((p n : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1 : 𝕜) =
      (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
⊢ ∀ (n : ℕ), (↑n.factorial : 𝕜) * p.coeff n = (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1

Tactic:
simp only [FormalMultilinearSeries.apply_eq_prod_smul_coeff, Finset.prod_const, Finset.card_univ,
    Fintype.card_fin, smul_eq_mul, nsmul_eq_mul, one_pow, one_mul] at h_fact_smul

Premises used: one_pow, Finset.card_univ, Fintype.card_fin, Finset.prod_const, FormalMultilinearSeries.apply_eq_prod_smul_coeff, nsmul_eq_mul, smul_eq_mul, one_mul
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul :
  ∀ (n : ℕ), (↑n.factorial : 𝕜) * p.coeff n = (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
h : iteratedDeriv n f x / (↑n.factorial : 𝕜) = p.coeff n ∨ Eq.{u_3 + 1} (α := 𝕜) (∏ x : Fin n, 1) 0
⊢ Eq (α := 𝕜)
    ((FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) n :
          (a : (i : Fin n) → 𝕜) → 𝕜)
        fun (x : Fin n) ↦ 1 :
      𝕜)
    ((p n : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1 : 𝕜)

Tactic:
simp only [FormalMultilinearSeries.apply_eq_prod_smul_coeff,
    FormalMultilinearSeries.coeff_ofScalars, smul_eq_mul, mul_eq_mul_left_iff]

Premises used: mul_eq_mul_left_iff, FormalMultilinearSeries.coeff_ofScalars, FormalMultilinearSeries.apply_eq_prod_smul_coeff, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul :
  ∀ (n : ℕ), (↑n.factorial : 𝕜) * p.coeff n = (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
h : iteratedDeriv n f x / (↑n.factorial : 𝕜) = p.coeff n
⊢ iteratedDeriv n f x / (↑n.factorial : 𝕜) = p.coeff n ∨ Eq.{u_3 + 1} (α := 𝕜) (∏ x : Fin n, 1) 0

Tactic:
left
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul :
  ∀ (n : ℕ), (↑n.factorial : 𝕜) * p.coeff n = (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
h : Ne.{u_3 + 1} (α := 𝕜) (↑n.factorial : 𝕜) 0
⊢ iteratedDeriv n f x / (↑n.factorial : 𝕜) = p.coeff n

Tactic:
rw [div_eq_iff, mul_comm, h_fact_smul, ← iteratedDeriv_eq_iteratedFDeriv]

Premises used: div_eq_iff, iteratedDeriv_eq_iteratedFDeriv, mul_comm
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul :
  ∀ (n : ℕ), (↑n.factorial : 𝕜) * p.coeff n = (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
h : ¬n.factorial = 0
⊢ Ne.{u_3 + 1} (α := 𝕜) (↑n.factorial : 𝕜) 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul :
  ∀ (n : ℕ), (↑n.factorial : 𝕜) * p.coeff n = (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
⊢ ¬n.factorial = 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
c : F
⊢ iteratedDeriv 0 (fun (x : 𝕜) ↦ c) x = if Eq (α := ℕ) 0 0 then c else 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
h : ∀ {c : F}, iteratedDeriv n (fun (x : 𝕜) ↦ c) x = if n = 0 then c else 0
c : F
⊢ iteratedDeriv (n + 1) (fun (x : 𝕜) ↦ c) x = if n + 1 = 0 then c else 0

Tactic:
simp [iteratedDeriv_succ', h]

Premises used: iteratedDeriv_succ'
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
c : F
x : 𝕜
zero : ∀ {c : F}, iteratedDeriv 0 (fun (x : 𝕜) ↦ c) x = if Eq (α := ℕ) 0 0 then c else 0
succ :
  ∀ (n : ℕ) (h : ∀ {c : F}, iteratedDeriv n (fun (x : 𝕜) ↦ c) x = if n = 0 then c else 0) {c : F},
    iteratedDeriv (n + 1) (fun (x : 𝕜) ↦ c) x = if n + 1 = 0 then c else 0
⊢ iteratedDeriv n (fun (x : 𝕜) ↦ c) x = if n = 0 then c else 0

Tactic:
induction n generalizing c with
  | zero => simp
  | succ n h => simp [iteratedDeriv_succ', h]

Premises used: iteratedDeriv_succ'
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
x : 𝕜
c : F
⊢ iteratedDerivWithin 0 (fun (x : 𝕜) ↦ c) s x = if Eq (α := ℕ) 0 0 then c else 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
x : 𝕜
n : ℕ
h : ∀ {c : F}, iteratedDerivWithin n (fun (x : 𝕜) ↦ c) s x = if n = 0 then c else 0
c : F
⊢ iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ c) s x = if n + 1 = 0 then c else 0

Tactic:
simp [iteratedDerivWithin_succ', Pi.zero_def, h]

Premises used: Pi.zero_def, iteratedDerivWithin_succ'
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
c : F
s : Set 𝕜
x : 𝕜
zero : ∀ {c : F}, iteratedDerivWithin 0 (fun (x : 𝕜) ↦ c) s x = if Eq (α := ℕ) 0 0 then c else 0
succ :
  ∀ (n : ℕ) (h : ∀ {c : F}, iteratedDerivWithin n (fun (x : 𝕜) ↦ c) s x = if n = 0 then c else 0) {c : F},
    iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ c) s x = if n + 1 = 0 then c else 0
⊢ iteratedDerivWithin n (fun (x : 𝕜) ↦ c) s x = if n = 0 then c else 0

Tactic:
induction n generalizing c with
  | zero => simp
  | succ n h => simp [iteratedDerivWithin_succ', Pi.zero_def, h]

Premises used: Pi.zero_def, iteratedDerivWithin_succ'
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
⊢ Eq.{u_2 + 1} (α := F) (iteratedDeriv n (fun (x : 𝕜) ↦ 0) x) 0

Tactic:
simpa using @iteratedDeriv_const 𝕜 _ F _ _ n 0

Premises used: iteratedDeriv_const
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
⊢ Eq.{u_2 + 1} (α := F) (iteratedDeriv n 0 x) 0

Tactic:
simp [Pi.zero_def]

Premises used: Pi.zero_def
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (fun (x : 𝕜) ↦ 0) s x) 0

Tactic:
simpa using @iteratedDerivWithin_const 𝕜 _ F _ _ n 0

Premises used: iteratedDerivWithin_const
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n 0 s x) 0

Tactic:
simp [Pi.zero_def]

Premises used: Pi.zero_def
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
simp :
  ((∀ m ≤ n + 1,
        Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
            PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
          (iteratedDeriv m f)) ∧
      ∀ m < n + 1, Differentiable 𝕜 (iteratedDeriv m f)) ↔
    ((∀ m ≤ n,
          Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
              PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
            (iteratedDeriv m f)) ∧
        ∀ m < n, Differentiable 𝕜 (iteratedDeriv m f)) ∧
      Differentiable 𝕜 (iteratedDeriv n f) ∧
        Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
            PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
          (iteratedDeriv (n + 1) f)
⊢ ContDiff 𝕜 (↑(n + 1) : ℕ∞ω) f ↔ ContDiff 𝕜 (↑n : ℕ∞ω) f ∧ ContDiff 𝕜 1 (iteratedDeriv n f)

Tactic:
simp only [contDiff_nat_iff_iteratedDeriv, contDiff_one_iff_deriv, ← iteratedDeriv_succ]

Premises used: iteratedDeriv_succ, contDiff_nat_iff_iteratedDeriv, contDiff_one_iff_deriv
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
⊢ ((∀ m ≤ n + 1,
        Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
            PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
          (iteratedDeriv m f)) ∧
      ∀ m < n + 1, Differentiable 𝕜 (iteratedDeriv m f)) ↔
    ((∀ m ≤ n,
          Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
              PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
            (iteratedDeriv m f)) ∧
        ∀ m < n, Differentiable 𝕜 (iteratedDeriv m f)) ∧
      Differentiable 𝕜 (iteratedDeriv n f) ∧
        Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
            PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
          (iteratedDeriv (n + 1) f)

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
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
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
hi : (↑i : ℕ∞ω) ≤ n
simp :
  Eq.{u_3 + 1} (α := F)
    ((FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g t (f x)) (ftaylorSeriesWithin 𝕜 f s x) i :
          (a : (i : Fin i) → 𝕜) → F)
        fun (x : Fin i) ↦ 1 :
      F)
    (∑ x_1 : OrderedFinpartition i,
        (iteratedFDerivWithin 𝕜 x_1.length g t (f x) : (a : (i : Fin x_1.length) → E) → F) fun (j : Fin x_1.length) ↦
          (iteratedFDerivWithin 𝕜 (x_1.partSize j) f s x : (a : (i : Fin (x_1.partSize j)) → 𝕜) → E)
            fun (x : Fin (x_1.partSize j)) ↦ 1 :
      F)
⊢ iteratedDerivWithin i (g ∘ f) s x =
    ∑ c : OrderedFinpartition i,
      (iteratedFDerivWithin 𝕜 c.length g t (f x) : (a : (i : Fin c.length) → E) → F) fun (j : Fin c.length) ↦
        iteratedDerivWithin (c.partSize j) f s x

Tactic:
simp only [iteratedDerivWithin, iteratedFDerivWithin_comp hg hf ht hs hx hst hi]

Premises used: iteratedDerivWithin, iteratedFDerivWithin_comp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
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
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq.{u_3 + 1} (α := F)
    ((FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g t (f x)) (ftaylorSeriesWithin 𝕜 f s x) i :
          (a : (i : Fin i) → 𝕜) → F)
        fun (x : Fin i) ↦ 1 :
      F)
    (∑ x_1 : OrderedFinpartition i,
        (iteratedFDerivWithin 𝕜 x_1.length g t (f x) : (a : (i : Fin x_1.length) → E) → F) fun (j : Fin x_1.length) ↦
          (iteratedFDerivWithin 𝕜 (x_1.partSize j) f s x : (a : (i : Fin (x_1.partSize j)) → 𝕜) → E)
            fun (x : Fin (x_1.partSize j)) ↦ 1 :
      F)

Tactic:
simp [FormalMultilinearSeries.taylorComp, ftaylorSeriesWithin,
    OrderedFinpartition.applyOrderedFinpartition_apply, comp_def]

Premises used: FormalMultilinearSeries.taylorComp, ftaylorSeriesWithin, Function.comp_def, OrderedFinpartition.applyOrderedFinpartition_apply
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
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
g : E → F
f : 𝕜 → E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : (↑i : ℕ∞ω) ≤ n
simp :
  iteratedDerivWithin i (g ∘ f) univ x =
    ∑ x_1 : OrderedFinpartition i,
      (iteratedFDerivWithin 𝕜 x_1.length g univ (f x) : (a : (i : Fin x_1.length) → E) → F) fun (j : Fin x_1.length) ↦
        iteratedDerivWithin (x_1.partSize j) f univ x
⊢ iteratedDeriv i (g ∘ f) x =
    ∑ c : OrderedFinpartition i,
      (iteratedFDeriv 𝕜 c.length g (f x) : (a : (i : Fin c.length) → E) → F) fun (j : Fin c.length) ↦
        iteratedDeriv (c.partSize j) f x

Tactic:
simp only [← iteratedDerivWithin_univ, ← iteratedFDerivWithin_univ]

Premises used: iteratedDerivWithin_univ, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
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
g : E → F
f : 𝕜 → E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : (↑i : ℕ∞ω) ≤ n
⊢ iteratedDerivWithin i (g ∘ f) univ x =
    ∑ x_1 : OrderedFinpartition i,
      (iteratedFDerivWithin 𝕜 x_1.length g univ (f x) : (a : (i : Fin x_1.length) → E) → F) fun (j : Fin x_1.length) ↦
        iteratedDerivWithin (x_1.partSize j) f univ x

Tactic:
iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf uniqueDiffOn_univ
    uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _) hi

Premises used: Set.mapsTo_univ, uniqueDiffOn_univ, Set.mem_univ, iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
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
g : E → F
f : 𝕜 → E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : (↑i : ℕ∞ω) ≤ n
⊢ iteratedDerivWithin i (g ∘ f) univ x =
    ∑ x_1 : OrderedFinpartition i,
      (iteratedFDerivWithin 𝕜 x_1.length g univ (f x) : (a : (i : Fin x_1.length) → E) → F) fun (j : Fin x_1.length) ↦
        iteratedDerivWithin (x_1.partSize j) f univ x

Tactic:
exact iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf uniqueDiffOn_univ
    uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _) hi

Premises used: Set.mapsTo_univ, uniqueDiffOn_univ, Set.mem_univ, iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition