awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
simp :
  iteratedDerivWithin 2 (g ∘ f) univ x =
    iteratedDerivWithin 2 g univ (f x) * HPow.hPow (β := ℕ) (derivWithin f univ x) 2 +
      derivWithin g univ (f x) * iteratedDerivWithin 2 f univ x
⊢ iteratedDeriv 2 (g ∘ f) x =
    iteratedDeriv 2 g (f x) * HPow.hPow (β := ℕ) (deriv f x) 2 + deriv g (f x) * iteratedDeriv 2 f x

Tactic:
simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]

Premises used: derivWithin_univ, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDerivWithin 2 (g ∘ f) univ x =
    iteratedDerivWithin 2 g univ (f x) * HPow.hPow (β := ℕ) (derivWithin f univ x) 2 +
      derivWithin g univ (f x) * iteratedDerivWithin 2 f univ x

Tactic:
iteratedDerivWithin_comp_two hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _)
    (mapsTo_univ _ _)

Premises used: iteratedDerivWithin_comp_two, Set.mapsTo_univ, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDerivWithin 2 (g ∘ f) univ x =
    iteratedDerivWithin 2 g univ (f x) * HPow.hPow (β := ℕ) (derivWithin f univ x) 2 +
      derivWithin g univ (f x) * iteratedDerivWithin 2 f univ x

Tactic:
exact iteratedDerivWithin_comp_two hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _)
    (mapsTo_univ _ _)

Premises used: iteratedDerivWithin_comp_two, Set.mapsTo_univ, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
rw :
  HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
        HSMul.hSMul (α := ℕ) 3 (iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x)) +
      iteratedDerivWithin 3 f s x • derivWithin g t (f x) =
    iteratedDerivWithin 3 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 3 +
        3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x +
      derivWithin g t (f x) * iteratedDerivWithin 3 f s x
⊢ iteratedDerivWithin 3 (g ∘ f) s x =
    iteratedDerivWithin 3 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 3 +
        3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x +
      derivWithin g t (f x) * iteratedDerivWithin 3 f s x

Tactic:
rw [iteratedDerivWithin_scomp_three hg hf ht hs hx hst]

Premises used: iteratedDerivWithin_scomp_three
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
simp :
  HPow.hPow (β := ℕ) (derivWithin f s x) 3 * iteratedDerivWithin 3 g t (f x) +
        3 * (iteratedDerivWithin 2 f s x * (derivWithin f s x * iteratedDerivWithin 2 g t (f x))) +
      iteratedDerivWithin 3 f s x * derivWithin g t (f x) =
    iteratedDerivWithin 3 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 3 +
        3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x +
      derivWithin g t (f x) * iteratedDerivWithin 3 f s x
⊢ HPow.hPow (β := ℕ) (derivWithin f s x) 3 • iteratedDerivWithin 3 g t (f x) +
        HSMul.hSMul (α := ℕ) 3 (iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x)) +
      iteratedDerivWithin 3 f s x • derivWithin g t (f x) =
    iteratedDerivWithin 3 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 3 +
        3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x +
      derivWithin g t (f x) * iteratedDerivWithin 3 f s x

Tactic:
simp only [nsmul_eq_mul, smul_eq_mul, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, nsmul_eq_mul, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ HPow.hPow (β := ℕ) (derivWithin f s x) 3 * iteratedDerivWithin 3 g t (f x) +
        3 * (iteratedDerivWithin 2 f s x * (derivWithin f s x * iteratedDerivWithin 2 g t (f x))) +
      iteratedDerivWithin 3 f s x * derivWithin g t (f x) =
    iteratedDerivWithin 3 g t (f x) * HPow.hPow (β := ℕ) (derivWithin f s x) 3 +
        3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x +
      derivWithin g t (f x) * iteratedDerivWithin 3 f s x

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
simp :
  iteratedDerivWithin 3 (g ∘ f) univ x =
    iteratedDerivWithin 3 g univ (f x) * HPow.hPow (β := ℕ) (derivWithin f univ x) 3 +
        3 * iteratedDerivWithin 2 g univ (f x) * iteratedDerivWithin 2 f univ x * derivWithin f univ x +
      derivWithin g univ (f x) * iteratedDerivWithin 3 f univ x
⊢ iteratedDeriv 3 (g ∘ f) x =
    iteratedDeriv 3 g (f x) * HPow.hPow (β := ℕ) (deriv f x) 3 +
        3 * iteratedDeriv 2 g (f x) * iteratedDeriv 2 f x * deriv f x +
      deriv g (f x) * iteratedDeriv 3 f x

Tactic:
simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]

Premises used: derivWithin_univ, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDerivWithin 3 (g ∘ f) univ x =
    iteratedDerivWithin 3 g univ (f x) * HPow.hPow (β := ℕ) (derivWithin f univ x) 3 +
        3 * iteratedDerivWithin 2 g univ (f x) * iteratedDerivWithin 2 f univ x * derivWithin f univ x +
      derivWithin g univ (f x) * iteratedDerivWithin 3 f univ x

Tactic:
iteratedDerivWithin_comp_three hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _)
    (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, iteratedDerivWithin_comp_three, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDerivWithin 3 (g ∘ f) univ x =
    iteratedDerivWithin 3 g univ (f x) * HPow.hPow (β := ℕ) (derivWithin f univ x) 3 +
        3 * iteratedDerivWithin 2 g univ (f x) * iteratedDerivWithin 2 f univ x * derivWithin f univ x +
      derivWithin g univ (f x) * iteratedDerivWithin 3 f univ x

Tactic:
exact iteratedDerivWithin_comp_three hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _)
    (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, iteratedDerivWithin_comp_three, uniqueDiffOn_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
n : ℕ
x : 𝕜
s : Set 𝕜
f g : 𝕜 → F
hfg : f =ᶠ[𝓝[s] x] g
hfg' : f x = g x
⊢ iteratedDerivWithin n f s x = iteratedDerivWithin n g s x

Tactic:
congr($(hfg.iteratedFDerivWithin_eq hfg' n) _)

Premises used: congrArg, id, Filter.EventuallyEq.iteratedFDerivWithin_eq, OfNat.ofNat, DFunLike.coe
-- 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 : 𝕜
f g : 𝕜 → F
s t : Set 𝕜
h : f =ᶠ[𝓝[s] x] g
ht : t ⊆ s
n : ℕ
unfold :
  EventuallyEq.{u_1, u_2} (β := F) (𝓝[s] x)
    (fun (x : 𝕜) ↦ (iteratedFDerivWithin 𝕜 n f t x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) fun (x : 𝕜) ↦
    (iteratedFDerivWithin 𝕜 n g t x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1
⊢ iteratedDerivWithin n f t =ᶠ[𝓝[s] x] iteratedDerivWithin n g t

Tactic:
unfold iteratedDerivWithin

Premises used: iteratedDerivWithin
-- 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 : 𝕜
f g : 𝕜 → F
s t : Set 𝕜
h : f =ᶠ[𝓝[s] x] g
ht : t ⊆ s
n : ℕ
⊢ EventuallyEq.{u_1, u_2} (β := F) (𝓝[s] x)
    (fun (x : 𝕜) ↦ (iteratedFDerivWithin 𝕜 n f t x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) fun (x : 𝕜) ↦
    (iteratedFDerivWithin 𝕜 n g t x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1

Tactic:
h.iteratedFDerivWithin' ht n |>.fun_comp (fun a ↦ a fun _ ↦ 1)

Premises used: Filter.EventuallyEq.iteratedFDerivWithin', OfNat.ofNat, Filter.EventuallyEq.fun_comp, DFunLike.coe
-- 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 : 𝕜
f g : 𝕜 → F
s t : Set 𝕜
h : f =ᶠ[𝓝[s] x] g
ht : t ⊆ s
n : ℕ
⊢ EventuallyEq.{u_1, u_2} (β := F) (𝓝[s] x)
    (fun (x : 𝕜) ↦ (iteratedFDerivWithin 𝕜 n f t x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) fun (x : 𝕜) ↦
    (iteratedFDerivWithin 𝕜 n g t x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1

Tactic:
exact h.iteratedFDerivWithin' ht n |>.fun_comp (fun a ↦ a fun _ ↦ 1)

Premises used: Filter.EventuallyEq.iteratedFDerivWithin', OfNat.ofNat, Filter.EventuallyEq.fun_comp, DFunLike.coe
-- 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 : 𝕜
f g : 𝕜 → F
s : Set 𝕜
h : f =ᶠ[𝓝[s] x] g
n : ℕ
⊢ iteratedDerivWithin n f s =ᶠ[𝓝[s] x] iteratedDerivWithin n g s

Tactic:
h.iteratedDerivWithin' Set.Subset.rfl n

Premises used: Filter.EventuallyEq.iteratedDerivWithin', Set.Subset.rfl
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_7
F : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hfg : f =ᶠ[𝓝[insert x s] x] g
⊢ 𝓝[s] x ≤ 𝓝[insert x s] x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_7
F : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hfg : f =ᶠ[𝓝[insert x s] x] g
⊢ x ∈ insert x s

Tactic:
simp
-- 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 : ℕ
s : Set 𝕜
f g : 𝕜 → F
hfg : Set.EqOn f g s
⊢ Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s

Tactic:
fun _ hx ↦ hfg.eventuallyEq_nhdsWithin.iteratedDerivWithin_eq (hfg hx)

Premises used: Set.EqOn.eventuallyEq_nhdsWithin, Filter.EventuallyEq.iteratedDerivWithin_eq, Set.EqOn
-- 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 : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) g s x
simp_rw :
  ((iteratedFDerivWithin 𝕜 n (f + g) s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) =
    HAdd.hAdd (α := F) (β := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
      ((iteratedFDerivWithin 𝕜 n g s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
simp_rw₁ :
  ((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n f s x)
          (iteratedFDerivWithin 𝕜 n g s x) :
        (a : (i : Fin n) → 𝕜) → F)
      fun (x : Fin n) ↦ 1) =
    HAdd.hAdd (α := F) (β := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
      ((iteratedFDerivWithin 𝕜 n g s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
⊢ iteratedDerivWithin n (f + g) s x = iteratedDerivWithin n f s x + iteratedDerivWithin n g s x

Tactic:
simp_rw [iteratedDerivWithin, iteratedFDerivWithin_add_apply hf hg h hx,
    ContinuousMultilinearMap.add_apply]

Premises used: iteratedDerivWithin, iteratedFDerivWithin_add_apply, ContinuousMultilinearMap.add_apply
-- 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 : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
hg : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) g s x
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ f z + g z) s x = iteratedDerivWithin n f s x + iteratedDerivWithin n g s x

Tactic:
simpa using iteratedDerivWithin_add hx h hf hg

Premises used: 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 : 𝕜
s : Set 𝕜
f : 𝕜 → F
hn : 0 < n
c : F
obtain :
  ∀ (n : ℕ) (hn : 0 < n.succ), iteratedDerivWithin n.succ (fun (z : 𝕜) ↦ c + f z) s x = iteratedDerivWithin n.succ f s x
⊢ iteratedDerivWithin n (fun (z : 𝕜) ↦ c + f z) s x = iteratedDerivWithin n f s x

Tactic:
obtain ⟨n, rfl⟩ := n.exists_eq_succ_of_ne_zero hn.ne'

Premises used: LT.lt.ne', Nat.exists_eq_succ_of_ne_zero, rfl
-- 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 : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
rw : iteratedDerivWithin n (derivWithin (fun (z : 𝕜) ↦ c + f z) s) s x = iteratedDerivWithin n (derivWithin f s) s x
⊢ iteratedDerivWithin n.succ (fun (z : 𝕜) ↦ c + f z) s x = iteratedDerivWithin n.succ f s x

Tactic:
rw [iteratedDerivWithin_succ', iteratedDerivWithin_succ']

Premises used: iteratedDerivWithin_succ'
-- 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 : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
e_f : ∀ (y : 𝕜), derivWithin (fun (z : 𝕜) ↦ c + f z) s y = derivWithin f s y
⊢ iteratedDerivWithin n (derivWithin (fun (z : 𝕜) ↦ c + f z) s) s x = iteratedDerivWithin n (derivWithin f s) s x

Tactic:
congr 1 with y
-- 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 : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
y : 𝕜
⊢ derivWithin (fun (z : 𝕜) ↦ c + f z) s y = derivWithin f s y

Tactic:
derivWithin_const_add _

Premises used: derivWithin_const_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
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
y : 𝕜
⊢ derivWithin (fun (z : 𝕜) ↦ c + f z) s y = derivWithin f s y

Tactic:
exact derivWithin_const_add _

Premises used: derivWithin_const_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 : 𝕜
s : Set 𝕜
f : 𝕜 → F
hn : 0 < n
c : F
obtain :
  ∀ (n : ℕ) (hn : 0 < n.succ),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n.succ (fun (z : 𝕜) ↦ c - f z) s x)
      (iteratedDerivWithin n.succ (fun (z : 𝕜) ↦ -f z) s x)
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (fun (z : 𝕜) ↦ c - f z) s x)
    (iteratedDerivWithin n (fun (z : 𝕜) ↦ -f z) s x)

Tactic:
obtain ⟨n, rfl⟩ := n.exists_eq_succ_of_ne_zero hn.ne'

Premises used: LT.lt.ne', Nat.exists_eq_succ_of_ne_zero, rfl
-- 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 : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
rw :
  Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (derivWithin (fun (z : 𝕜) ↦ c - f z) s) s x)
    (iteratedDerivWithin n (derivWithin (fun (z : 𝕜) ↦ -f z) s) s x)
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n.succ (fun (z : 𝕜) ↦ c - f z) s x)
    (iteratedDerivWithin n.succ (fun (z : 𝕜) ↦ -f z) s x)

Tactic:
rw [iteratedDerivWithin_succ', iteratedDerivWithin_succ']

Premises used: iteratedDerivWithin_succ'
-- 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 : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
e_f : ∀ (y : 𝕜), Eq.{u_2 + 1} (α := F) (derivWithin (fun (z : 𝕜) ↦ c - f z) s y) (derivWithin (fun (z : 𝕜) ↦ -f z) s y)
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (derivWithin (fun (z : 𝕜) ↦ c - f z) s) s x)
    (iteratedDerivWithin n (derivWithin (fun (z : 𝕜) ↦ -f z) s) s x)

Tactic:
congr 1 with y
-- 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 : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
y : 𝕜
e_f : derivWithin (fun (z : 𝕜) ↦ c - f z) s y = -derivWithin f s y
⊢ Eq.{u_2 + 1} (α := F) (derivWithin (fun (z : 𝕜) ↦ c - f z) s y) (derivWithin (fun (z : 𝕜) ↦ -f z) s y)

Tactic:
rw [derivWithin.fun_neg]

Premises used: derivWithin.fun_neg
-- 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 : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
y : 𝕜
⊢ derivWithin (fun (z : 𝕜) ↦ c - f z) s y = -derivWithin f s y

Tactic:
derivWithin_const_sub _

Premises used: derivWithin_const_sub
-- 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 : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
y : 𝕜
⊢ derivWithin (fun (z : 𝕜) ↦ c - f z) s y = -derivWithin f s y

Tactic:
exact derivWithin_const_sub _

Premises used: derivWithin_const_sub
-- 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 : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
R : Type u_3
inst_3 : DistribSMul R F
inst_4 : SMulCommClass 𝕜 R F
inst_5 : ContinuousConstSMul R F
c : R
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
simp_rw :
  ((iteratedFDerivWithin 𝕜 n (c • f) s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) =
    HSMul.hSMul (β := F) c ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
⊢ iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x

Tactic:
simp_rw [iteratedDerivWithin]

Premises used: iteratedDerivWithin
-- 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 : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
R : Type u_3
inst_3 : DistribSMul R F
inst_4 : SMulCommClass 𝕜 R F
inst_5 : ContinuousConstSMul R F
c : R
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
rw :
  ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) c (iteratedFDerivWithin 𝕜 n f s x) :
        (a : (i : Fin n) → 𝕜) → F)
      fun (x : Fin n) ↦ 1) =
    HSMul.hSMul (β := F) c ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
⊢ ((iteratedFDerivWithin 𝕜 n (c • f) s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1) =
    HSMul.hSMul (β := F) c ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)

Tactic:
rw [iteratedFDerivWithin_const_smul_apply (a := c) hf h hx]

Premises used: iteratedFDerivWithin_const_smul_apply
-- 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 : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
R : Type u_3
inst_3 : DistribSMul R F
inst_4 : SMulCommClass 𝕜 R F
inst_5 : ContinuousConstSMul R F
c : R
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
⊢ ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) c (iteratedFDerivWithin 𝕜 n f s x) :
        (a : (i : Fin n) → 𝕜) → F)
      fun (x : Fin n) ↦ 1) =
    HSMul.hSMul (β := F) c ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)

Tactic:
simp only [ContinuousMultilinearMap.smul_apply]

Premises used: ContinuousMultilinearMap.smul_apply
-- 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 : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
R : Type u_3
inst_3 : DistribSMul R F
inst_4 : SMulCommClass 𝕜 R F
inst_5 : ContinuousConstSMul R F
c : R
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) f s x
⊢ iteratedDerivWithin n (fun (w : 𝕜) ↦ c • f w) s x = c • iteratedDerivWithin n f s x

Tactic:
iteratedDerivWithin_const_smul hx h c hf

Premises used: iteratedDerivWithin_const_smul
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
𝕝 : Type u_4
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
x : 𝕜
f : 𝕜 → F
⊢ iteratedDerivWithin 0 (c • f) s x = c • iteratedDerivWithin 0 f s x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
𝕝 : Type u_4
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
n : ℕ
IH : ∀ {x : 𝕜} (f : 𝕜 → F), iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
x : 𝕜
f : 𝕜 → F
succ : derivWithin (iteratedDerivWithin n (c • f) s) s x = c • derivWithin (iteratedDerivWithin n f s) s x
succ₁ :
  derivWithin (fun (x : 𝕜) ↦ c • iteratedDerivWithin n f s x) s x = c • derivWithin (iteratedDerivWithin n f s) s x
succ₂ : derivWithin (c • iteratedDerivWithin n f s) s x = c • derivWithin (iteratedDerivWithin n f s) s x
⊢ iteratedDerivWithin (n + 1) (c • f) s x = c • iteratedDerivWithin (n + 1) f s x

Tactic:
simp_rw [iteratedDerivWithin_succ, funext (@IH · f), ← Pi.smul_def,
      derivWithin_const_smul_field]

Premises used: derivWithin_const_smul_field, funext, iteratedDerivWithin_succ, Pi.smul_def
-- 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 : 𝕜
s : Set 𝕜
𝕝 : Type u_4
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
zero : ∀ {x : 𝕜} (f : 𝕜 → F), iteratedDerivWithin 0 (c • f) s x = c • iteratedDerivWithin 0 f s x
succ :
  ∀ (n : ℕ) (IH : ∀ {x : 𝕜} (f : 𝕜 → F), iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x) {x : 𝕜}
    (f : 𝕜 → F), iteratedDerivWithin (n + 1) (c • f) s x = c • iteratedDerivWithin (n + 1) f s x
⊢ iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x

Tactic:
induction n generalizing f x with
  | zero => simp
  | succ n IH =>
    simp_rw [iteratedDerivWithin_succ, funext (@IH · f), ← Pi.smul_def,
      derivWithin_const_smul_field]

Premises used: derivWithin_const_smul_field, iteratedDerivWithin_succ, Pi.smul_def