awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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) (iteratedFDerivWithin 𝕜 (k + 1) f s)
    (p.iteratedFDerivSeries (k + 1)) s x r
have 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
Tactic: rw [iteratedFDerivWithin_succ_eq_comp_left]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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
⊢ 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
have 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
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)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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
⊢ 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
have 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
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)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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
⊢ 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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (hypothesis)
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
⊢ 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)
have this : p n = 0
Tactic: have : p n = 0 := p.congr_zero rfl h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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
⊢ 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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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
⊢ p.iteratedFDerivSeries k n = 0
have 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
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))]
Cleared hypotheses: k, n, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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
⊢ p.iteratedFDerivSeries k n = 0
have 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
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))]
Cleared hypotheses: k, n, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (hypothesis)
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) 0
have 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)
Tactic: have : iteratedFDerivWithin 𝕜 n f s x = p.iteratedFDerivSeries n 0 (fun _ ↦ 0) :=
    ((h.iteratedFDerivWithin h' n hu hx).coeff_zero _).symm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x) 0
have 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
Tactic: rw [this, p.iteratedFDerivSeries_eq_zero (p.congr_zero (Nat.zero_add n).symm hn),
    ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x) 0
have 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
Tactic: rw [this, p.iteratedFDerivSeries_eq_zero (p.congr_zero (Nat.zero_add n).symm hn),
    ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x) 0
have rw₂ : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) 0 0
Tactic: rw [this, p.iteratedFDerivSeries_eq_zero (p.congr_zero (Nat.zero_add n).symm hn),
    ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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
⊢ 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)
have 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)
Tactic: rw [← sum_comp (Equiv.inv (Perm (Fin n)))]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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
⊢ 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)
have 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)
Tactic: change iteratedFDeriv 𝕜 n (f ∘ g) x v = _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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
⊢ 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)
have 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)
Tactic: rw [ContinuousLinearMap.iteratedFDeriv_comp_right _ f.contDiff _ le_rfl, f.iteratedFDeriv_eq]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
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
⊢ 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)
have 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 sorry)))
          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))
Tactic: simp only [ContinuousMultilinearMap.iteratedFDeriv,
    ContinuousMultilinearMap.compContinuousLinearMap_apply, ContinuousMultilinearMap.sum_apply,
    ContinuousMultilinearMap.iteratedFDerivComponent_apply, Set.mem_range, Pi.compRightL_apply]