awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
m : ℕ
hm : n + 1 ≤ m
⊢ n ≠ m

Tactic:
lia
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
m : ℕ
hm : n + 1 ≤ m
⊢ n ≠ m

Tactic:
have : n ≠ m := by lia
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
m : ℕ
hm : n + 1 ≤ m
this : n ≠ m
⊢ q m = 0

Tactic:
simp [q, this]
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
⊢ HasFiniteFPowerSeriesOnBall g q x (n + 1) r

Tactic:
have A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r := by
    apply HasFiniteFPowerSeriesOnBall.mk' _ h.r_pos
    · intro y hy
      rw [Finset.sum_eq_single_of_mem n]
      · simp [q, g]
      · simp
      · intro i hi h'i
        simp [q, h'i.symm]
    · intro m hm
      have : n ≠ m := by lia
      simp [q, this]
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
⊢ HasFPowerSeriesWithinOnBall g q s x r

Tactic:
have B : HasFPowerSeriesWithinOnBall g q s x r :=
    A.toHasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
⊢ f = g + (f - g)

Tactic:
abel
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
⊢ f = g + (f - g)

Tactic:
have : f = g + (f - g) := by abel
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
this : f = g + (f - g)
nth_rewrite :
  iteratedFDerivWithin 𝕜 n (g + (f - g)) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x)
⊢ iteratedFDerivWithin 𝕜 n f s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x)

Tactic:
nth_rewrite 1 [this]
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
this : f = g + (f - g)
⊢ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) (f - g) s x

Tactic:
(fcont _ hx).sub (gcont.of_le le_top).contDiffWithinAt

Premises used: ContDiffWithinAt.sub, ContDiff.of_le, ContDiff.contDiffWithinAt, le_top
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
this : f = g + (f - g)
⊢ ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) (f - g) s x

Tactic:
exact (fcont _ hx).sub (gcont.of_le le_top).contDiffWithinAt

Premises used: ContDiffWithinAt.sub, ContDiff.of_le, ContDiff.contDiffWithinAt, le_top
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
this : f = g + (f - g)
rw rw₁ :
  HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x) =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x)
⊢ iteratedFDerivWithin 𝕜 n (g + (f - g)) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x)

Tactic:
rw [iteratedFDerivWithin_add_apply (gcont.of_le le_top).contDiffWithinAt
      (by exact (fcont _ hx).sub (gcont.of_le le_top).contDiffWithinAt) hs hx]

Premises used: iteratedFDerivWithin_add_apply, ContDiff.of_le, ContDiff.contDiffWithinAt, le_top
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
⊢ iteratedFDerivWithin 𝕜 n f s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x)

Tactic:
have J1 : iteratedFDerivWithin 𝕜 n f s x =
      iteratedFDerivWithin 𝕜 n g s x + iteratedFDerivWithin 𝕜 n (f - g) s x := by
    have : f = g + (f - g) := by abel
    nth_rewrite 1 [this]
    rw [iteratedFDerivWithin_add_apply (gcont.of_le le_top).contDiffWithinAt
      (by exact (fcont _ hx).sub (gcont.of_le le_top).contDiffWithinAt) hs hx]
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 :
  iteratedFDerivWithin 𝕜 n f s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x)
apply : (p - q) n = 0
apply₁ : AnalyticOn 𝕜 g s
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n (f - g) s x)
    0

Tactic:
apply (h.sub B).iteratedFDerivWithin_eq_zero (h'.sub ?_) hs hx

Premises used: AnalyticOn.sub, HasFPowerSeriesWithinOnBall.sub, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_zero
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 :
  iteratedFDerivWithin 𝕜 n f s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x)
⊢ (p - q) n = 0

Tactic:
simp [q]
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 :
  iteratedFDerivWithin 𝕜 n f s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x)
⊢ AnalyticOn 𝕜 g s

Tactic:
apply gcont.contDiffOn.analyticOn

Premises used: ContDiff.contDiffOn, ContDiffOn.analyticOn
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 :
  iteratedFDerivWithin 𝕜 n f s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n (f - g) s x)
    0

Tactic:
have J2 : iteratedFDerivWithin 𝕜 n (f - g) s x = 0 := by
    apply (h.sub B).iteratedFDerivWithin_eq_zero (h'.sub ?_) hs hx
    · simp [q]
    · apply gcont.contDiffOn.analyticOn
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 :
  iteratedFDerivWithin 𝕜 n f s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x)
J2 :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n (f - g) s x)
    0
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n g s x)
    (iteratedFDeriv 𝕜 n g x)

Tactic:
have J3 : iteratedFDerivWithin 𝕜 n g s x = iteratedFDeriv 𝕜 n g x :=
    iteratedFDerivWithin_eq_iteratedFDeriv hs (gcont.of_le le_top).contDiffAt hx
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 :
  iteratedFDerivWithin 𝕜 n f s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x)
J2 :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n (f - g) s x)
    0
J3 :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n g s x)
    (iteratedFDeriv 𝕜 n g x)
simp :
  Eq.{u_3 + 1} (α := F) ((iteratedFDeriv 𝕜 n g x : (a : (i : Fin n) → E) → F) v : F)
    (∑ σ : Perm (Fin n), (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ v ((σ : (a : Fin n) → Fin n) i) : F)
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
    (∑ σ : Perm (Fin n), (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ v ((σ : (a : Fin n) → Fin n) i) : F)

Tactic:
simp only [J1, J3, J2, add_zero]

Premises used: add_zero