awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
⊢ ∀ x < k, ¬k + 1 - x = 0

Tactic:
lia
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
simp : ∀ x < k, ¬k + 1 - x = 1
⊢ ∀ x ∈ Finset.range k, k + 1 - x ≠ 1

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
⊢ ∀ x < k, ¬k + 1 - x = 1

Tactic:
lia
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
⊢ k < i → i - k = i - (k + 1) + 1

Tactic:
lia
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
⊢ ∑ i_1 ∈ Finset.range (k + 1 + 1),
      HMul.hMul (α := 𝕜) (↑((k + 1).choose i_1) : 𝕜) (iteratedDerivWithin i_1 (fun (x : 𝕜) ↦ x ^ i) s x) *
        iteratedDerivWithin (k + 1 - i_1) (fun (x : 𝕜) ↦ x) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))

Tactic:
simp +contextual [IH, iteratedDerivWithin_fun_id, h, hx, Finset.sum_range_succ,
        show ∀ x ∈ Finset.range k, k + 1 - x ≠ 0 by simp; lia, -Nat.descFactorial_succ,
        show ∀ x ∈ Finset.range k, k + 1 - x ≠ 1 by simp; lia, this,
        Nat.descFactorial_eq_zero_iff_lt.mpr, hik,
        show k < i → i - k = (i - (k + 1) + 1) by lia]

Premises used: Iff.mpr, iteratedDerivWithin_fun_id, Nat.descFactorial_succ, Nat.descFactorial_eq_zero_iff_lt, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
simp : ∀ x < k, ¬k + 1 - x = 0
⊢ ∀ x ∈ Finset.range k, k + 1 - x ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
⊢ ∀ x < k, ¬k + 1 - x = 0

Tactic:
lia
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
simp : ∀ x < k, ¬k + 1 - x = 1
⊢ ∀ x ∈ Finset.range k, k + 1 - x ≠ 1

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
⊢ ∀ x < k, ¬k + 1 - x = 1

Tactic:
lia
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
⊢ k < i → i - k = i - (k + 1) + 1

Tactic:
lia
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
succ :
  HAdd.hAdd (α := 𝕜) (↑k : 𝕜) 1 * ((↑(i.descFactorial k) : 𝕜) * x ^ (i - (k + 1) + 1)) +
      (↑(i.descFactorial (k + 1)) : 𝕜) * x ^ (i - (k + 1)) * x =
    (HAdd.hAdd (α := 𝕜) (↑k : 𝕜) 1 * (↑(i.descFactorial k) : 𝕜) + (↑(i.descFactorial (k + 1)) : 𝕜)) *
      x ^ (i - (k + 1) + 1)
⊢ ∑ i_1 ∈ Finset.range (k + 1 + 1),
      HMul.hMul (α := 𝕜) (↑((k + 1).choose i_1) : 𝕜) (iteratedDerivWithin i_1 (fun (x : 𝕜) ↦ x ^ i) s x) *
        iteratedDerivWithin (k + 1 - i_1) (fun (x : 𝕜) ↦ x) s x =
    (↑((i + 1).descFactorial (k + 1)) : 𝕜) * x ^ (i + 1 - (k + 1))

Tactic:
simp +contextual [IH, iteratedDerivWithin_fun_id, h, hx, Finset.sum_range_succ,
        show ∀ x ∈ Finset.range k, k + 1 - x ≠ 0 by simp; lia, -Nat.descFactorial_succ,
        show ∀ x ∈ Finset.range k, k + 1 - x ≠ 1 by simp; lia, this,
        Nat.descFactorial_eq_zero_iff_lt.mpr, hik,
        show k < i → i - k = (i - (k + 1) + 1) by lia]

Premises used: Iff.mpr, iteratedDerivWithin_fun_id, Nat.descFactorial_succ, Nat.descFactorial_eq_zero_iff_lt, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
⊢ HAdd.hAdd (α := 𝕜) (↑k : 𝕜) 1 * ((↑(i.descFactorial k) : 𝕜) * x ^ (i - (k + 1) + 1)) +
      (↑(i.descFactorial (k + 1)) : 𝕜) * x ^ (i - (k + 1)) * x =
    (HAdd.hAdd (α := 𝕜) (↑k : 𝕜) 1 * (↑(i.descFactorial k) : 𝕜) + (↑(i.descFactorial (k + 1)) : 𝕜)) *
      x ^ (i - (k + 1) + 1)

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
m k : ℕ
zero :
  ∀ (k : ℕ),
    iteratedDerivWithin k (fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 0) s x = (↑(Nat.descFactorial 0 k) : 𝕜) * x ^ (0 - k)
succ :
  ∀ (i : ℕ) (IH : ∀ (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ i) s x = (↑(i.descFactorial k) : 𝕜) * x ^ (i - k))
    (k : ℕ), iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ (i + 1)) s x = (↑((i + 1).descFactorial k) : 𝕜) * x ^ (i + 1 - k)
⊢ iteratedDerivWithin k (fun (x : 𝕜) ↦ x ^ m) s x = (↑(m.descFactorial k) : 𝕜) * x ^ (m - k)

Tactic:
induction m generalizing k with
  | zero => cases k <;> simp [iteratedDerivWithin_const]
  | succ i IH =>
    obtain (_ | k) := k
    · simp
    simp only [pow_succ]
    refine (iteratedDerivWithin_mul hx h (by fun_prop) (by fun_prop)).trans ?_
    have : ((i + 1).descFactorial (k + 1)) =
        (k + 1) * (i.descFactorial k) + (i.descFactorial (k + 1)) := by
      rw [Nat.succ_descFactorial_succ]
      cases le_or_gt k i <;> simp [Nat.descFactorial, ← add_mul, *]; lia
    obtain hik | hik := le_or_gt i k <;>
      simp +contextual [IH, iteratedDerivWithin_fun_id, h, hx, Finset.sum_range_succ,
        show ∀ x ∈ Finset.range k, k + 1 - x ≠ 0 by simp; lia, -Nat.descFactorial_succ,
        show ∀ x ∈ Finset.range k, k + 1 - x ≠ 1 by simp; lia, this,
        Nat.descFactorial_eq_zero_iff_lt.mpr, hik,
        show k < i → i - k = (i - (k + 1) + 1) by lia]; ring

Premises used: Iff.mpr, pow_succ, iteratedDerivWithin_fun_id, Nat.descFactorial_succ, iteratedDerivWithin_const, iteratedDerivWithin_mul, Nat.descFactorial_eq_zero_iff_lt, Finset.sum_range_succ, Eq.trans
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_7
inst : NontriviallyNormedField 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f₁ f₂ : 𝕜 → F
x : 𝕜
h : f₁ =ᶠ[𝓝 x] f₂
n : ℕ
⊢ iteratedDeriv n f₁ =ᶠ[𝓝 x] iteratedDeriv n f₂

Tactic:
simp_all [← nhdsWithin_univ, ← iteratedDerivWithin_univ, EventuallyEq.iteratedDerivWithin]

Premises used: nhdsWithin_univ, Filter.EventuallyEq.iteratedDerivWithin, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
f g : 𝕜 → F
hf : ContDiffAt 𝕜 (↑n : WithTop ℕ∞) f x
hg : ContDiffAt 𝕜 (↑n : WithTop ℕ∞) g x
⊢ iteratedDeriv n (f + g) x = iteratedDeriv n f x + iteratedDeriv n g x

Tactic:
simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_add (Set.mem_univ _) uniqueDiffOn_univ hf hg

Premises used: uniqueDiffOn_univ, iteratedDerivWithin_univ, Set.mem_univ, iteratedDerivWithin_add
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
f : 𝕜 → F
hn : 0 < n
c : F
⊢ iteratedDeriv n (fun (z : 𝕜) ↦ c + f z) x = iteratedDeriv n f x

Tactic:
simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_const_add hn c

Premises used: iteratedDerivWithin_const_add, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
f : 𝕜 → F
hn : 0 < n
c : F
⊢ iteratedDeriv n (fun (z : 𝕜) ↦ c - f z) x = iteratedDeriv n (-f) x

Tactic:
simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_const_sub hn c

Premises used: iteratedDerivWithin_const_sub, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
a : 𝕜
⊢ iteratedDeriv n (-f) a = -iteratedDeriv n f a

Tactic:
simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_neg f

Premises used: iteratedDerivWithin_neg, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
f g : 𝕜 → F
hf : ContDiffAt 𝕜 (↑n : WithTop ℕ∞) f x
hg : ContDiffAt 𝕜 (↑n : WithTop ℕ∞) g x
⊢ iteratedDeriv n (f - g) x = iteratedDeriv n f x - iteratedDeriv n g x

Tactic:
simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_sub (Set.mem_univ _) uniqueDiffOn_univ hf hg

Premises used: iteratedDerivWithin_sub, uniqueDiffOn_univ, iteratedDerivWithin_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
R : Type u_3
inst_3 : DistribSMul R F
inst_4 : SMulCommClass 𝕜 R F
inst_5 : ContinuousConstSMul R F
n : ℕ
f : 𝕜 → F
h : ContDiffAt 𝕜 (↑n : WithTop ℕ∞) f x
c : R
⊢ iteratedDeriv n (c • f) x = c • iteratedDeriv n f x

Tactic:
simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_const_smul (Set.mem_univ x) uniqueDiffOn_univ
      c (contDiffWithinAt_univ.mpr h)

Premises used: Iff.mpr, contDiffWithinAt_univ, uniqueDiffOn_univ, iteratedDerivWithin_const_smul, iteratedDerivWithin_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕝 : Type u_4
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
n : ℕ
c : 𝕝
f : 𝕜 → F
⊢ iteratedDeriv n (c • f) x = c • iteratedDeriv n f x

Tactic:
simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_const_smul_field (s := Set.univ) c f

Premises used: iteratedDerivWithin_const_smul_field, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕝 : Type u_4
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
n : ℕ
c : 𝕝
f : 𝕜 → F
⊢ iteratedDeriv n (fun (x : 𝕜) ↦ c • f x) x = c • iteratedDeriv n f x

Tactic:
simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_fun_const_smul_field (s := Set.univ) c f

Premises used: iteratedDerivWithin_fun_const_smul_field, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
inst_5 : Module 𝔸 F
inst_6 : IsBoundedSMul 𝔸 F
inst_7 : IsScalarTower 𝕜 𝔸 F
f : 𝕜 → 𝔸
hf : ContDiffAt 𝕜 (↑n : WithTop ℕ∞) f x
v : F
⊢ iteratedDeriv n (fun (y : 𝕜) ↦ f y • v) x = iteratedDeriv n f x • v

Tactic:
simp [iteratedDeriv, iteratedFDeriv_smul_const_apply hf]

Premises used: iteratedFDeriv_smul_const_apply, iteratedDeriv
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_5
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
f : 𝕜 → 𝔸
c : 𝔸
hf : ContDiffAt 𝕜 (↑n : WithTop ℕ∞) f x
⊢ iteratedDeriv n (fun (x : 𝕜) ↦ c * f x) x = c * iteratedDeriv n f x

Tactic:
simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_const_mul (Set.mem_univ x) uniqueDiffOn_univ c hf

Premises used: uniqueDiffOn_univ, iteratedDerivWithin_univ, Set.mem_univ, iteratedDerivWithin_const_mul
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_6
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
n : ℕ
c : 𝕜'
f : 𝕜 → 𝕜'
⊢ iteratedDeriv n (fun (x : 𝕜) ↦ c * f x) x = c * iteratedDeriv n f x

Tactic:
simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_const_mul_field (s := .univ) c f

Premises used: iteratedDerivWithin_const_mul_field, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_6
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
n : ℕ
f : 𝕜 → 𝕜'
c : 𝕜'
⊢ iteratedDeriv n (fun (x : 𝕜) ↦ f x * c) x = iteratedDeriv n f x * c

Tactic:
simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_mul_const_field (s := .univ) f c

Premises used: iteratedDerivWithin_univ, iteratedDerivWithin_mul_const_field
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_6
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
n : ℕ
f : 𝕜 → 𝕜'
c : 𝕜'
⊢ iteratedDeriv n (fun (x : 𝕜) ↦ f x / c) x = iteratedDeriv n f x / c

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
h : ContDiff 𝕜 (↑n : WithTop ℕ∞) f
c : 𝕜
h₁ : ∀ (x : 𝕜), iteratedDeriv n (fun (x : 𝕜) ↦ f (c * x)) x = c ^ n • iteratedDeriv n f (c * x)
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (x : 𝕜) ↦ f (c * x)) fun (x : 𝕜) ↦ c ^ n • iteratedDeriv n f (c * x)

Tactic:
funext x
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
h : ContDiff 𝕜 (↑n : WithTop ℕ∞) f
c x : 𝕜
⊢ iteratedDeriv n (fun (x : 𝕜) ↦ f (c * x)) x = c ^ n • iteratedDeriv n f (c * x)

Tactic:
simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_comp_const_smul (Set.mem_univ x) uniqueDiffOn_univ (contDiffOn_univ.mpr h)
      c (Set.mapsTo_univ _ _)

Premises used: Iff.mpr, Set.mapsTo_univ, uniqueDiffOn_univ, iteratedDerivWithin_comp_const_smul, iteratedDerivWithin_univ, Set.mem_univ, contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
f : 𝕜 → 𝕜
h : ContDiff 𝕜 (↑n : WithTop ℕ∞) f
c : 𝕜
⊢ Eq.{u_1 + 1} (α := (x : 𝕜) → 𝕜) (iteratedDeriv n fun (x : 𝕜) ↦ f (c * x)) fun (x : 𝕜) ↦
    c ^ n * iteratedDeriv n f (c * x)

Tactic:
simpa only [smul_eq_mul] using iteratedDeriv_comp_const_smul h c

Premises used: iteratedDeriv_comp_const_smul, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
a : 𝕜
⊢ iteratedDeriv n (fun (x : 𝕜) ↦ f (-x)) a = HPow.hPow (α := 𝕜) (-1) n • iteratedDeriv n f (-a)

Tactic:
simp [iteratedDeriv, ← iteratedFDerivWithin_univ, iteratedFDerivWithin_comp_neg]

Premises used: iteratedFDerivWithin_comp_neg, iteratedDeriv, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
zero : iteratedDeriv 0 id x = if Eq (α := ℕ) 0 0 then x else if Eq (α := ℕ) 0 1 then 1 else 0
succ :
  iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) id x =
    if HAdd.hAdd (α := ℕ) 0 1 = 0 then x else if HAdd.hAdd (α := ℕ) 0 1 = 1 then 1 else 0
succ₁ : ∀ (n : ℕ), iteratedDeriv (n + 1 + 1) id x = if n + 1 + 1 = 0 then x else if n + 1 + 1 = 1 then 1 else 0
⊢ iteratedDeriv n id x = if n = 0 then x else if n = 1 then 1 else 0

Tactic:
obtain (_ | _ | n) := n
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ iteratedDeriv 0 id x = if Eq (α := ℕ) 0 0 then x else if Eq (α := ℕ) 0 1 then 1 else 0

Tactic:
simp [iteratedDeriv_succ', iteratedDeriv_const]

Premises used: iteratedDeriv_succ', iteratedDeriv_const
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) id x =
    if HAdd.hAdd (α := ℕ) 0 1 = 0 then x else if HAdd.hAdd (α := ℕ) 0 1 = 1 then 1 else 0

Tactic:
simp [iteratedDeriv_succ', iteratedDeriv_const]

Premises used: iteratedDeriv_succ', iteratedDeriv_const
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
⊢ iteratedDeriv (n + 1 + 1) id x = if n + 1 + 1 = 0 then x else if n + 1 + 1 = 1 then 1 else 0

Tactic:
simp [iteratedDeriv_succ', iteratedDeriv_const]

Premises used: iteratedDeriv_succ', iteratedDeriv_const
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
⊢ Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (a : 𝕜) ↦ a) 0) (if n = 1 then 1 else 0)

Tactic:
simp +contextual [iteratedDeriv_fun_id]

Premises used: iteratedDeriv_fun_id
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
𝔸 : Type u_5
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f g : 𝕜 → 𝔸
hf : ContDiffAt 𝕜 (↑n : WithTop ℕ∞) f x
hg : ContDiffAt 𝕜 (↑n : WithTop ℕ∞) g x
⊢ iteratedDeriv n (f * g) x =
    ∑ i ∈ Finset.range (n + 1), (↑(n.choose i) : 𝔸) * iteratedDeriv i f x * iteratedDeriv (n - i) g x

Tactic:
simpa using iteratedDerivWithin_mul
    (Set.mem_univ x) uniqueDiffOn_univ hf.contDiffWithinAt hg.contDiffWithinAt

Premises used: uniqueDiffOn_univ, iteratedDerivWithin_mul, Set.mem_univ, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
m k : ℕ
⊢ iteratedDeriv k (fun (x : 𝕜) ↦ x ^ m) x = (↑(m.descFactorial k) : 𝕜) * x ^ (m - k)

Tactic:
simpa using iteratedDerivWithin_pow (Set.mem_univ x) uniqueDiffOn_univ m k

Premises used: uniqueDiffOn_univ, iteratedDerivWithin_pow, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ
inl :
  ∀ (h : n < m),
    Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)
inr :
  ∀ (h : n = m),
    Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)
inr₁ :
  ∀ (h : m < n),
    Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)

Tactic:
obtain h | h | h := lt_trichotomy n m

Premises used: lt_trichotomy
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ
h : n < m
⊢ Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)

Tactic:
simp_all [Nat.descFactorial_self, Nat.descFactorial_eq_zero_iff_lt.mpr, ne_of_lt, ne_of_gt]

Premises used: Iff.mpr, ne_of_gt, Nat.descFactorial_eq_zero_iff_lt, Nat.descFactorial_self, ne_of_lt
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ
h : n = m
⊢ Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)

Tactic:
simp_all [Nat.descFactorial_self, Nat.descFactorial_eq_zero_iff_lt.mpr, ne_of_lt, ne_of_gt]

Premises used: Iff.mpr, ne_of_gt, Nat.descFactorial_eq_zero_iff_lt, Nat.descFactorial_self, ne_of_lt
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ
h : m < n
⊢ Eq.{u_1 + 1} (α := 𝕜) (iteratedDeriv n (fun (x : 𝕜) ↦ x ^ m) 0) (↑(if n = m then m.factorial else 0) : 𝕜)

Tactic:
simp_all [Nat.descFactorial_self, Nat.descFactorial_eq_zero_iff_lt.mpr, ne_of_lt, ne_of_gt]

Premises used: Iff.mpr, ne_of_gt, Nat.descFactorial_eq_zero_iff_lt, Nat.descFactorial_self, ne_of_lt
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f g : 𝕜 → F
x : 𝕜
hfg : f =ᶠ[𝓝 x] g
simp :
  Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f Set.univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
    ((iteratedFDerivWithin 𝕜 n g Set.univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
⊢ iteratedDeriv n f x = iteratedDeriv n g x

Tactic:
simp only [← iteratedDerivWithin_univ, iteratedDerivWithin_eq_iteratedFDerivWithin]

Premises used: iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedDerivWithin_univ