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
k : ℕ
ih :
  HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r
succ :
  HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F :=
    ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
    (Function.comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (k + 1)) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 k f s) s))
    (p.iteratedFDerivSeries (k + 1)) s x r
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F :=
    ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F) (iteratedFDerivWithin 𝕜 (k + 1) f s)
    (p.iteratedFDerivSeries (k + 1)) s x r

Tactic:
rw [iteratedFDerivWithin_succ_eq_comp_left]

Premises used: iteratedFDerivWithin_succ_eq_comp_left
-- 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
k : ℕ
ih :
  HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F :=
    ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
    (Function.comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (k + 1)) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 k f s) s))
    (p.iteratedFDerivSeries (k + 1)) s x r

Tactic:
apply (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (k + 1) ↦ E) F).symm
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall
        (ih.fderivWithin_of_mem_of_analyticOn (h'.iteratedFDerivWithin hs _) hs hx)

Premises used: AnalyticOn.iteratedFDerivWithin, ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall, HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_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
k : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
zero :
  HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDerivWithin 𝕜 0 f s) (p.iteratedFDerivSeries 0) s x r
succ :
  ∀ (k : ℕ)
    (ih :
      HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
        (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r),
    HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F :=
      ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F) (iteratedFDerivWithin 𝕜 (k + 1) f s)
      (p.iteratedFDerivSeries (k + 1)) s x r
⊢ HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r

Tactic:
induction k with
  | zero =>
    exact (continuousMultilinearCurryFin0 𝕜 E F).symm
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall h
  | succ k ih =>
    rw [iteratedFDerivWithin_succ_eq_comp_left]
    apply (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (k + 1) ↦ E) F).symm
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall
        (ih.fderivWithin_of_mem_of_analyticOn (h'.iteratedFDerivWithin hs _) hs hx)

Premises used: LinearIsometryEquiv.symm, iteratedFDerivWithin_succ_eq_comp_left, continuousMultilinearCurryFin0, ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.toContinuousLinearMap
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 0)) ↦ E) F) (p (n + 0)) 0
zero :
  ∀ (x : (i : Fin n) → E) (x_1 : (i : Fin 0) → E),
    Eq.{u_3 + 1} (α := F)
      ((((p.iteratedFDerivSeries 0 n : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) x :
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) :
            (a : (i : Fin 0) → E) → F)
          x_1 :
        F)
      ((((0 : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) x :
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) :
            (a : (i : Fin 0) → E) → F)
          x_1 :
        F)
⊢ Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
      (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F))
    (p.iteratedFDerivSeries 0 n) 0

Tactic:
ext
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 0)) ↦ E) F) (p (n + 0)) 0
x : (i : Fin n) → E
x_1 : (i : Fin 0) → E
⊢ p n = 0

Tactic:
have : p n = 0 := p.congr_zero rfl h
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 0)) ↦ E) F) (p (n + 0)) 0
x : (i : Fin n) → E
x_1 : (i : Fin 0) → E
this : p n = 0
⊢ Eq.{u_3 + 1} (α := F)
    ((((p.iteratedFDerivSeries 0 n : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) x :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) :
          (a : (i : Fin 0) → E) → F)
        x_1 :
      F)
    ((((0 : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) x :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) :
          (a : (i : Fin 0) → E) → F)
        x_1 :
      F)

Tactic:
simp [FormalMultilinearSeries.iteratedFDerivSeries, this]

Premises used: FormalMultilinearSeries.iteratedFDerivSeries
-- 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
p : FormalMultilinearSeries 𝕜 E F
k : ℕ
ih :
  ∀ {n : ℕ} (h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) 0),
    p.iteratedFDerivSeries k n = 0
n : ℕ
h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + (k + 1))) ↦ E) F) (p (n + (k + 1))) 0
succ :
  ∀ (x : (i : Fin n) → E) (x_1 : (i : Fin (k + 1)) → E),
    Eq.{u_3 + 1} (α := F)
      ((((p.iteratedFDerivSeries (k + 1) n :
                  (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
                x :
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F) :
            (a : (i : Fin (k + 1)) → E) → F)
          x_1 :
        F)
      ((((0 : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + 1)) ↦ E) F) x :
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F) :
            (a : (i : Fin (k + 1)) → E) → F)
          x_1 :
        F)
⊢ Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
      (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F))
    (p.iteratedFDerivSeries (k + 1) n) 0

Tactic:
ext
-- 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
p : FormalMultilinearSeries 𝕜 E F
k : ℕ
ih :
  ∀ {n : ℕ} (h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) 0),
    p.iteratedFDerivSeries k n = 0
n : ℕ
h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + (k + 1))) ↦ E) F) (p (n + (k + 1))) 0
x : (i : Fin n) → E
x_1 : (i : Fin (k + 1)) → E
⊢ Eq.{u_3 + 1} (α := F)
    ((((p.iteratedFDerivSeries (k + 1) n :
                (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
              x :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F) :
          (a : (i : Fin (k + 1)) → E) → F)
        x_1 :
      F)
    ((((0 : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + 1)) ↦ E) F) x :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F) :
          (a : (i : Fin (k + 1)) → E) → F)
        x_1 :
      F)

Tactic:
simp only [iteratedFDerivSeries, Nat.succ_eq_add_one,
      ContinuousLinearMap.compFormalMultilinearSeries_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
      LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply,
      continuousMultilinearCurryLeftEquiv_symm_apply, ContinuousMultilinearMap.zero_apply,
      ContinuousLinearMap.zero_apply,
      derivSeries_eq_zero _ (ih (p.congr_zero (Nat.succ_add_eq_add_succ _ _).symm h))]

Premises used: Nat.succ_eq_add_one, LinearIsometryEquiv.coe_toContinuousLinearEquiv, ContinuousLinearMap.compFormalMultilinearSeries_apply, ContinuousLinearMap.compContinuousMultilinearMap_coe, FormalMultilinearSeries.congr_zero, FormalMultilinearSeries.derivSeries_eq_zero, Function.comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply, ContinuousMultilinearMap.zero_apply, ContinuousLinearEquiv.coe_coe, Eq.symm, FormalMultilinearSeries.iteratedFDerivSeries, Nat.succ_add_eq_add_succ, ContinuousLinearMap.zero_apply
-- 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
p : FormalMultilinearSeries 𝕜 E F
k n : ℕ
h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) 0
zero :
  ∀ {n : ℕ} (h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 0)) ↦ E) F) (p (n + 0)) 0),
    Eq (α :=
      ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
        (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F))
      (p.iteratedFDerivSeries 0 n) 0
succ :
  ∀ (k : ℕ)
    (ih :
      ∀ {n : ℕ}
        (h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) 0),
        p.iteratedFDerivSeries k n = 0)
    {n : ℕ}
    (h :
      Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + (k + 1))) ↦ E) F) (p (n + (k + 1))) 0),
    Eq (α :=
      ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
        (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F))
      (p.iteratedFDerivSeries (k + 1) n) 0
⊢ p.iteratedFDerivSeries k n = 0

Tactic:
induction k generalizing n with
  | zero =>
    ext
    have : p n = 0 := p.congr_zero rfl h
    simp [FormalMultilinearSeries.iteratedFDerivSeries, this]
  | succ k ih =>
    ext
    simp only [iteratedFDerivSeries, Nat.succ_eq_add_one,
      ContinuousLinearMap.compFormalMultilinearSeries_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
      LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply,
      continuousMultilinearCurryLeftEquiv_symm_apply, ContinuousMultilinearMap.zero_apply,
      ContinuousLinearMap.zero_apply,
      derivSeries_eq_zero _ (ih (p.congr_zero (Nat.succ_add_eq_add_succ _ _).symm h))]

Premises used: Nat.succ_eq_add_one, LinearIsometryEquiv.coe_toContinuousLinearEquiv, ContinuousLinearMap.compFormalMultilinearSeries_apply, ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply, ContinuousMultilinearMap.zero_apply, ContinuousLinearEquiv.coe_coe, FormalMultilinearSeries.iteratedFDerivSeries, ContinuousLinearMap.zero_apply
-- 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
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : p n = 0
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    ((p.iteratedFDerivSeries n 0 : (a : (i : Fin 0) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F)
      fun (x : Fin 0) ↦ 0)

Tactic:
have : iteratedFDerivWithin 𝕜 n f s x = p.iteratedFDerivSeries n 0 (fun _ ↦ 0) :=
    ((h.iteratedFDerivWithin h' n hu hx).coeff_zero _).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
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : p n = 0
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    ((p.iteratedFDerivSeries n 0 : (a : (i : Fin 0) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F)
      fun (x : Fin 0) ↦ 0)
rw :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
    ((p.iteratedFDerivSeries n 0 : (a : (i : Fin 0) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F)
      fun (x : Fin 0) ↦ 0)
    0
rw₁ :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
    ((0 : (a : (i : Fin 0) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) fun (x : Fin 0) ↦ 0) 0
rw₂ rw₃ : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) 0 0
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x) 0

Tactic:
rw [this, p.iteratedFDerivSeries_eq_zero (p.congr_zero (Nat.zero_add n).symm hn),
    ContinuousMultilinearMap.zero_apply]

Premises used: FormalMultilinearSeries.iteratedFDerivSeries_eq_zero, FormalMultilinearSeries.congr_zero, ContinuousMultilinearMap.zero_apply, Nat.zero_add, Eq.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
n : ℕ
f : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
x : E
v : Fin n → E
rw :
  Eq.{u_3 + 1} (α := F)
    ((iteratedFDeriv 𝕜 n (fun (x : E) ↦ (f : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ x) x :
          (a : (i : Fin n) → E) → F)
        v :
      F)
    (∑ i : Perm (Fin n),
        (f : (a : (i : Fin n) → E) → F) fun (i_1 : Fin n) ↦
          v
            ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n)) i : Perm (Fin n)) : (a : Fin n) → Fin n)
              i_1) :
      F)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDeriv 𝕜 n (fun (x : E) ↦ (f : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ x) x :
          (a : (i : Fin n) → E) → F)
        v :
      F)
    (∑ σ : Perm (Fin n), (f : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ v ((σ : (a : Fin n) → Fin n) i) : F)

Tactic:
rw [← sum_comp (Equiv.inv (Perm (Fin n)))]

Premises used: Equiv.inv, Equiv.sum_comp, Equiv.Perm, Fin
-- 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
n : ℕ
f : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi (φ := fun (a : Fin n) ↦ E) fun (i : Fin n) ↦ ContinuousLinearMap.id 𝕜 E
change :
  Eq.{u_3 + 1} (α := F)
    ((iteratedFDeriv 𝕜 n
            (Function.comp (β := (i : Fin n) → E) (⇑f : (a : (i : Fin n) → E) → F) (⇑g : (a : E) → Fin n → E)) x :
          (a : (i : Fin n) → E) → F)
        v :
      F)
    (∑ i : Perm (Fin n),
        (f : (a : (i : Fin n) → E) → F) fun (i_1 : Fin n) ↦
          v
            ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n)) i : Perm (Fin n)) : (a : Fin n) → Fin n)
              i_1) :
      F)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDeriv 𝕜 n (fun (x : E) ↦ (f : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ x) x :
          (a : (i : Fin n) → E) → F)
        v :
      F)
    (∑ i : Perm (Fin n),
        (f : (a : (i : Fin n) → E) → F) fun (i_1 : Fin n) ↦
          v
            ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n)) i : Perm (Fin n)) : (a : Fin n) → Fin n)
              i_1) :
      F)

Tactic:
change iteratedFDeriv 𝕜 n (f ∘ g) x v = _

Premises used: Function.comp, iteratedFDeriv, DFunLike.coe
-- 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
n : ℕ
f : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi (φ := fun (a : Fin n) ↦ E) fun (i : Fin n) ↦ ContinuousLinearMap.id 𝕜 E
rw :
  Eq.{u_3 + 1} (α := F)
    (((compContinuousLinearMap (M₁ := fun (x : Fin n) ↦ E) (M₁' := fun (i : Fin n) ↦ (i : Fin n) → E)
              (f.iteratedFDeriv (E₁ := fun (i : Fin n) ↦ E) n ((g : (a : E) → (i : Fin n) → E) x)) fun (x : Fin n) ↦ g :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        v :
      F)
    (∑ i : Perm (Fin n),
        (f : (a : (i : Fin n) → E) → F) fun (i_1 : Fin n) ↦
          v
            ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n)) i : Perm (Fin n)) : (a : Fin n) → Fin n)
              i_1) :
      F)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDeriv 𝕜 n
            (Function.comp (β := (i : Fin n) → E) (⇑f : (a : (i : Fin n) → E) → F) (⇑g : (a : E) → Fin n → E)) x :
          (a : (i : Fin n) → E) → F)
        v :
      F)
    (∑ i : Perm (Fin n),
        (f : (a : (i : Fin n) → E) → F) fun (i_1 : Fin n) ↦
          v
            ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n)) i : Perm (Fin n)) : (a : Fin n) → Fin n)
              i_1) :
      F)

Tactic:
rw [ContinuousLinearMap.iteratedFDeriv_comp_right _ f.contDiff _ le_rfl, f.iteratedFDeriv_eq]

Premises used: le_rfl, ContinuousMultilinearMap.contDiff, ContinuousMultilinearMap.iteratedFDeriv_eq, ContinuousLinearMap.iteratedFDeriv_comp_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
n : ℕ
f : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi (φ := fun (a : Fin n) ↦ E) fun (i : Fin n) ↦ ContinuousLinearMap.id 𝕜 E
simp :
  Eq.{u_3 + 1} (α := F)
    (∑ x_1 : Fin n ↪ Fin n,
      (f : (a : (i : Fin n) → E) → F) fun (j : Fin n) ↦
        if h : ∃ (y : Fin n), (x_1 : (a : Fin n) → Fin n) y = j then
          (g : (a : E) → (i : Fin n) → E)
            (v
              ((x_1.toEquivRange.symm : (a : (↑(range (⇑x_1 : (a : Fin n) → Fin n)) : Type)) → Fin n)
                (Subtype.mk (p := fun (x : Fin n) ↦
                  Membership.mem (γ := Set (Fin n)) (range (ι := Fin n) (⇑x_1 : (a : Fin n) → Fin n)) x) j ⋯)))
            j
        else (g : (a : E) → (i : Fin n) → E) x j)
    (∑ i : Perm (Fin n),
      (f : (a : (i : Fin n) → E) → F) fun (i_1 : Fin n) ↦
        v
          ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n)) i : Perm (Fin n)) : (a : Fin n) → Fin n)
            i_1))
⊢ Eq.{u_3 + 1} (α := F)
    (((compContinuousLinearMap (M₁ := fun (x : Fin n) ↦ E) (M₁' := fun (i : Fin n) ↦ (i : Fin n) → E)
              (f.iteratedFDeriv (E₁ := fun (i : Fin n) ↦ E) n ((g : (a : E) → (i : Fin n) → E) x)) fun (x : Fin n) ↦ g :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        v :
      F)
    (∑ i : Perm (Fin n),
        (f : (a : (i : Fin n) → E) → F) fun (i_1 : Fin n) ↦
          v
            ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n)) i : Perm (Fin n)) : (a : Fin n) → Fin n)
              i_1) :
      F)

Tactic:
simp only [ContinuousMultilinearMap.iteratedFDeriv,
    ContinuousMultilinearMap.compContinuousLinearMap_apply, ContinuousMultilinearMap.sum_apply,
    ContinuousMultilinearMap.iteratedFDerivComponent_apply, Set.mem_range, Pi.compRightL_apply]

Premises used: Set.mem_range, Pi.compRightL_apply, ContinuousMultilinearMap.sum_apply, ContinuousMultilinearMap.compContinuousLinearMap_apply, ContinuousMultilinearMap.iteratedFDerivComponent_apply, ContinuousMultilinearMap.iteratedFDeriv