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
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)
g' : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z
⊢ g = fun (z : E) ↦ g' (z - x)

Tactic:
have : g = fun z ↦ g' (z - x) := rfl
-- 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)
g' : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z
this : g = fun (z : E) ↦ g' (z - x)
rw :
  Eq.{u_3 + 1} (α := F) ((iteratedFDeriv 𝕜 n g' (x - 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) ((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)

Tactic:
rw [this, iteratedFDeriv_comp_sub]

Premises used: iteratedFDeriv_comp_sub
-- 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)
g' : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z
this : g = fun (z : E) ↦ g' (z - x)
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDeriv 𝕜 n g' (x - 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:
(p n).iteratedFDeriv_comp_diagonal _ v

Premises used: ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal
-- 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)
g' : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z
this : g = fun (z : E) ↦ g' (z - x)
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDeriv 𝕜 n g' (x - 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:
exact (p n).iteratedFDeriv_comp_diagonal _ v

Premises used: ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal
-- 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
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)

Tactic:
have : iteratedFDerivWithin 𝕜 n f s x
      = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x :=
    (iteratedFDerivWithin_inter_open Metric.isOpen_eball (Metric.mem_eball_self h.r_pos)).symm
-- 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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
rw :
  Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) 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:
rw [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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
h₁ : HasFPowerSeriesWithinOnBall f p (s ∩ Metric.eball x r) x r
h'₁ : AnalyticOn 𝕜 f (s ∩ Metric.eball x r)
hs₁ : UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)
hx₁ : x ∈ s ∩ Metric.eball x r
h's : s ∩ Metric.eball x r ⊆ Metric.eball x r
r₁ : ℝ≥0∞
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) 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:
apply HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset

Premises used: _private.0.HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
-- 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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ HasFPowerSeriesWithinOnBall f p (s ∩ Metric.eball x r) x r

Tactic:
h.mono inter_subset_left

Premises used: Set.inter_subset_left, HasFPowerSeriesWithinOnBall.mono
-- 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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ HasFPowerSeriesWithinOnBall f p (s ∩ Metric.eball x r) x r

Tactic:
exact h.mono inter_subset_left

Premises used: Set.inter_subset_left, HasFPowerSeriesWithinOnBall.mono
-- 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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ AnalyticOn 𝕜 f (s ∩ Metric.eball x r)

Tactic:
h'.mono inter_subset_left

Premises used: Set.inter_subset_left, AnalyticOn.mono
-- 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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ AnalyticOn 𝕜 f (s ∩ Metric.eball x r)

Tactic:
exact h'.mono inter_subset_left

Premises used: Set.inter_subset_left, AnalyticOn.mono
-- 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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)

Tactic:
hs.inter Metric.isOpen_eball

Premises used: Metric.isOpen_eball, UniqueDiffOn.inter
-- 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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)

Tactic:
exact hs.inter Metric.isOpen_eball

Premises used: Metric.isOpen_eball, UniqueDiffOn.inter
-- 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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ x ∈ s ∩ Metric.eball x r

Tactic:
⟨hx, Metric.mem_eball_self h.r_pos⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro, HasFPowerSeriesWithinOnBall.r_pos, Metric.mem_eball_self
-- 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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ x ∈ s ∩ Metric.eball x r

Tactic:
exact ⟨hx, Metric.mem_eball_self h.r_pos⟩
-- 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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r

Tactic:
inter_subset_right

Premises used: Set.inter_subset_right
-- 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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r

Tactic:
exact inter_subset_right

Premises used: Set.inter_subset_right
-- 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
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
h' : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
simp :
  ∀ (h : HasFPowerSeriesWithinOnBall f p univ x r),
    Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f univ 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) ((iteratedFDeriv 𝕜 n f 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 [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊢

Premises used: hasFPowerSeriesWithinOnBall_univ, iteratedFDerivWithin_univ
-- 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
x : E
r : ℝ≥0∞
h' : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f univ 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:
h.iteratedFDerivWithin_eq_sum h' uniqueDiffOn_univ (mem_univ x) v

Premises used: uniqueDiffOn_univ, Set.mem_univ, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum
-- 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
x : E
r : ℝ≥0∞
h' : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f univ 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:
exact h.iteratedFDerivWithin_eq_sum h' uniqueDiffOn_univ (mem_univ x) v

Premises used: uniqueDiffOn_univ, Set.mem_univ, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum
-- 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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)

Tactic:
have : iteratedFDerivWithin 𝕜 n f s x
      = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x :=
    (iteratedFDerivWithin_inter_open Metric.isOpen_eball (Metric.mem_eball_self h.r_pos)).symm
-- 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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
rw :
  Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) 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:
rw [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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
h₁ : HasFPowerSeriesWithinOnBall f p (s ∩ Metric.eball x r) x r
h' : AnalyticOn 𝕜 f (s ∩ Metric.eball x r)
hs₁ : UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)
hx₁ : x ∈ s ∩ Metric.eball x r
h's : s ∩ Metric.eball x r ⊆ Metric.eball x r
r₁ : ℝ≥0∞
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) 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:
apply HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset

Premises used: _private.0.HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
-- 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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ HasFPowerSeriesWithinOnBall f p (s ∩ Metric.eball x r) x r

Tactic:
h.mono inter_subset_left

Premises used: Set.inter_subset_left, HasFPowerSeriesWithinOnBall.mono