awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
⊢ HasFDerivAt.{u_3, u_3, u_5} (𝕜 := 𝕜) (F := F) (fun (z : 𝕜) ↦ ∑' (n : α), g n z)
    (ContinuousLinearMap.toSpanSingleton 𝕜 (∑' (n : α), g' n y)) y
have h : Eq.{u_3 + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup →
  HEq.{u_3 + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜) →
    Eq (α := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (∑' (n : α), g' n y))
      (∑' (n : α), ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y))
Tactic: convert! hasFDerivAt_tsum_of_isPreconnected hu ht h't hg ?_ hy₀ hg0 hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
h :
  Eq.{u_3 + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq.{u_3 + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜) →
      Eq (α := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (∑' (n : α), g' n y))
        (∑' (n : α), ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y))
⊢ HasFDerivAt.{u_3, u_3, u_5} (𝕜 := 𝕜) (F := F) (fun (z : 𝕜) ↦ ∑' (n : α), g n z)
    (ContinuousLinearMap.toSpanSingleton 𝕜 (∑' (n : α), g' n y)) y
have convert! : ∀ (n : α), ∀ x ∈ t, norm (E := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n x)) ≤ u n
Tactic: convert! hasFDerivAt_tsum_of_isPreconnected hu ht h't hg ?_ hy₀ hg0 hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
⊢ Differentiable.{u_3, u_4, u_5} 𝕜 (F := F) fun (y : E) ↦ ∑' (n : α), f n y
have pos : ∀ (h : ∃ (x₀ : E), Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀),
  Differentiable.{u_3, u_4, u_5} 𝕜 (F := F) fun (y : E) ↦ ∑' (n : α), f n y
Tactic: by_cases! h : ∃ x₀, Summable fun n => f n x₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
pos :
  ∀ (h : ∃ (x₀ : E), Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀),
    Differentiable.{u_3, u_4, u_5} 𝕜 (F := F) fun (y : E) ↦ ∑' (n : α), f n y
⊢ Differentiable.{u_3, u_4, u_5} 𝕜 (F := F) fun (y : E) ↦ ∑' (n : α), f n y
have neg : ∀ (h : ∀ (x₀ : E), ¬Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀),
  Differentiable.{u_3, u_4, u_5} 𝕜 (F := F) fun (y : E) ↦ ∑' (n : α), f n y
Tactic: by_cases! h : ∃ x₀, Summable fun n => f n x₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∃ (x₀ : E), Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
⊢ Differentiable.{u_3, u_4, u_5} 𝕜 (F := F) fun (y : E) ↦ ∑' (n : α), f n y
have pos : ∀ (x₀ : E) (hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀),
  Differentiable.{u_3, u_4, u_5} 𝕜 (F := F) fun (y : E) ↦ ∑' (n : α), f n y
Tactic: rcases h with ⟨x₀, hf0⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
⊢ Eq (α := (x : E) → F) (fun (x : E) ↦ ∑' (n : α), f n x) 0
have h₁ : ∀ (x : E), Eq.{u_5 + 1} (α := F) (∑' (n : α), f n x) (0 x)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
⊢ Differentiable.{u_3, u_4, u_5} 𝕜 (F := F) fun (y : E) ↦ ∑' (n : α), f n y
have this : Eq (α := (x : E) → F) (fun (x : E) ↦ ∑' (n : α), f n x) 0
Tactic: have : (fun x => ∑' n, f n x) = 0 := by ext1 x; exact tsum_eq_zero_of_not_summable (h x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
this : Eq (α := (x : E) → F) (fun (x : E) ↦ ∑' (n : α), f n x) 0
⊢ Differentiable.{u_3, u_4, u_5} 𝕜 (F := F) fun (y : E) ↦ ∑' (n : α), f n y
have neg : Differentiable.{u_3, u_4, u_5} 𝕜 (E := E) (F := F) 0
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
⊢ Differentiable.{u_3, u_3, u_5} 𝕜 (F := F) fun (z : 𝕜) ↦ ∑' (n : α), g n z
have hg₁ : ∀ (n : α) (y : 𝕜), HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
Tactic: simp_rw [hasDerivAt_iff_hasFDerivAt] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
⊢ Differentiable.{u_3, u_3, u_5} 𝕜 (F := F) fun (z : 𝕜) ↦ ∑' (n : α), g n z
have refine : ∀ (n : α) (x : 𝕜), norm (E := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n x)) ≤ u n
Tactic: refine differentiable_tsum hu hg ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
x₀ : E
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), norm (E := E →L[𝕜] F) (fderiv 𝕜 (f n) x) ≤ u n
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderiv 𝕜 fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), fderiv 𝕜 (f n) x
have h : ∀ (x : E), Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (y : E) ↦ ∑' (n : α), f n y) x) (∑' (n : α), fderiv 𝕜 (f n) x)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α), Differentiable 𝕜 (g n)
hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n
hg0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y₀
⊢ Eq (α := (x : 𝕜) → F) (deriv fun (y : 𝕜) ↦ ∑' (n : α), g n y) fun (y : 𝕜) ↦ ∑' (n : α), deriv (g n) y
have h : ∀ (x : 𝕜), Eq.{u_5 + 1} (α := F) (deriv (fun (y : 𝕜) ↦ ∑' (n : α), g n y) x) (∑' (n : α), deriv (g n) x)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
hk : (↑0 : ℕ∞) ≤ N
⊢ Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDeriv 𝕜 0 fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 0 (f n) x
have zero : ∀ (x : E),
  Eq (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDeriv 𝕜 0 (fun (y : E) ↦ ∑' (n : α), f n y) x) (∑' (n : α), iteratedFDeriv 𝕜 0 (f n) x)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
k : ℕ
IH :
  ∀ (hk : (↑k : ℕ∞) ≤ N),
    Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (iteratedFDeriv 𝕜 k fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : (↑(k + 1) : ℕ∞) ≤ N
⊢ Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
    (iteratedFDeriv 𝕜 (k + 1) fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦
    ∑' (n : α), iteratedFDeriv 𝕜 (k + 1) (f n) x
have h'k : (↑k : ℕ∞) < N
Tactic: have h'k : (k : ℕ∞) < N := lt_of_lt_of_le (WithTop.coe_lt_coe.2 (Nat.lt_succ_self _)) hk
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
k : ℕ
IH :
  ∀ (hk : (↑k : ℕ∞) ≤ N),
    Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (iteratedFDeriv 𝕜 k fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : (↑(k + 1) : ℕ∞) ≤ N
h'k : (↑k : ℕ∞) < N
⊢ Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
    (iteratedFDeriv 𝕜 (k + 1) fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦
    ∑' (n : α), iteratedFDeriv 𝕜 (k + 1) (f n) x
have A : Summable (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) fun (n : α) ↦
  iteratedFDeriv 𝕜 k (f n) 0
Tactic: have A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0 :=
      .of_norm_bounded (hv k h'k.le) fun n ↦ h'f k n 0 h'k.le
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
k : ℕ
IH :
  ∀ (hk : (↑k : ℕ∞) ≤ N),
    Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (iteratedFDeriv 𝕜 k fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : (↑(k + 1) : ℕ∞) ≤ N
h'k : (↑k : ℕ∞) < N
A :
  Summable (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) fun (n : α) ↦
    iteratedFDeriv 𝕜 k (f n) 0
⊢ Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
    (iteratedFDeriv 𝕜 (k + 1) fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦
    ∑' (n : α), iteratedFDeriv 𝕜 (k + 1) (f n) x
have succ : Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
  (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
    (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) ≃ₗᵢ[𝕜]
            ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (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)
    (fderiv 𝕜 fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x))
  fun (x : E) ↦
  ∑' (n : α),
    comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (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)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 k (f n))) x
Tactic: simp_rw [iteratedFDeriv_succ_eq_comp_left, IH h'k.le]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
k : ℕ
hk : (↑k : ℕ∞) ≤ N
⊢ Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
    (iteratedFDeriv 𝕜 k fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
have zero : ∀ (hk : (↑0 : ℕ∞) ≤ N),
  Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDeriv 𝕜 0 fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 0 (f n) x
Tactic: induction k with
  | zero =>
    ext1 x
    simp_rw [iteratedFDeriv_zero_eq_comp]
    exact (continuousMultilinearCurryFin0 𝕜 E F).symm.toContinuousLinearEquiv.map_tsum
  | succ k IH =>
    have h'k : (k : ℕ∞) < N := lt_of_lt_of_le (WithTop.coe_lt_coe.2 (Nat.lt_succ_self _)) hk
    have A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0 :=
      .of_norm_bounded (hv k h'k.le) fun n ↦ h'f k n 0 h'k.le
    simp_rw [iteratedFDeriv_succ_eq_comp_left, IH h'k.le]
    rw [fderiv_tsum (hv _ hk) (fun n => (hf n).differentiable_iteratedFDeriv
        (mod_cast h'k)) _ A]
    · ext1 x
      exact (continuousMultilinearCurryLeftEquiv 𝕜
        (fun _ : Fin (k + 1) => E) F).symm.toContinuousLinearEquiv.map_tsum
    · intro n x
      simpa only [iteratedFDeriv_succ_eq_comp_left, LinearIsometryEquiv.norm_map, comp_apply]
        using h'f k.succ n x hk
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
k : ℕ
hk : (↑k : ℕ∞) ≤ N
zero :
  ∀ (hk : (↑0 : ℕ∞) ≤ N),
    Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (iteratedFDeriv 𝕜 0 fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 0 (f n) x
⊢ Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
    (iteratedFDeriv 𝕜 k fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
have succ : ∀ (k : ℕ)
  (IH :
    ∀ (hk : (↑k : ℕ∞) ≤ N),
      Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
        (iteratedFDeriv 𝕜 k fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x)
  (hk : (↑(k + 1) : ℕ∞) ≤ N),
  Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
    (iteratedFDeriv 𝕜 (k + 1) fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦
    ∑' (n : α), iteratedFDeriv 𝕜 (k + 1) (f n) x
Tactic: induction k with
  | zero =>
    ext1 x
    simp_rw [iteratedFDeriv_zero_eq_comp]
    exact (continuousMultilinearCurryFin0 𝕜 E F).symm.toContinuousLinearEquiv.map_tsum
  | succ k IH =>
    have h'k : (k : ℕ∞) < N := lt_of_lt_of_le (WithTop.coe_lt_coe.2 (Nat.lt_succ_self _)) hk
    have A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0 :=
      .of_norm_bounded (hv k h'k.le) fun n ↦ h'f k n 0 h'k.le
    simp_rw [iteratedFDeriv_succ_eq_comp_left, IH h'k.le]
    rw [fderiv_tsum (hv _ hk) (fun n => (hf n).differentiable_iteratedFDeriv
        (mod_cast h'k)) _ A]
    · ext1 x
      exact (continuousMultilinearCurryLeftEquiv 𝕜
        (fun _ : Fin (k + 1) => E) F).symm.toContinuousLinearEquiv.map_tsum
    · intro n x
      simpa only [iteratedFDeriv_succ_eq_comp_left, LinearIsometryEquiv.norm_map, comp_apply]
        using h'f k.succ n x hk
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
k : ℕ
hk : (↑k : ℕ∞) ≤ N
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
    (iteratedFDeriv 𝕜 k (fun (y : E) ↦ ∑' (n : α), f n y) x) (∑' (n : α), iteratedFDeriv 𝕜 k (f n) x)
have rw : Eq (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
  ((fun (x : E) ↦
      (∑' (n : α), iteratedFDeriv 𝕜 k (f n) x : ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F))
    x)
  (∑' (n : α), iteratedFDeriv 𝕜 k (f n) x)
Tactic: rw [iteratedFDeriv_tsum hf hv h'f hk]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑N : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
have rw : (∀ (m : ℕ),
    (↑m : ℕ∞) ≤ N →
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦
        iteratedFDeriv 𝕜 m (fun (x : E) ↦ ∑' (i : α), f i x) x) ∧
  ∀ (m : ℕ),
    (↑m : ℕ∞) < N →
      Differentiable 𝕜 (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
        iteratedFDeriv 𝕜 m (fun (x : E) ↦ ∑' (i : α), f i x) x
Tactic: rw [contDiff_iff_continuous_differentiable]