awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (∀ (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
have left : ∀ (m : ℕ),
  (↑m : ℕ∞) ≤ N →
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦
      iteratedFDeriv 𝕜 m (fun (x : E) ↦ ∑' (i : α), f i x) x
Tactic: constructor
-- 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
left :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ N →
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦
        iteratedFDeriv 𝕜 m (fun (x : E) ↦ ∑' (i : α), f i x) x
⊢ (∀ (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
have right : ∀ (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: constructor
-- 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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦
    (fun (x : E) ↦
        (∑' (n : α), iteratedFDeriv 𝕜 m (f n) x :
          ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F))
      x
have left : ∀ (i : α), Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (iteratedFDeriv 𝕜 m (f i))
Tactic: refine continuous_tsum ?_ (hv m hm) ?_
-- 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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
left : ∀ (i : α), Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (iteratedFDeriv 𝕜 m (f i))
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦
    (fun (x : E) ↦
        (∑' (n : α), iteratedFDeriv 𝕜 m (f n) x :
          ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F))
      x
have left₁ : ∀ (n : α) (x : E),
  norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m (f n) x) ≤ v m n
Tactic: refine continuous_tsum ?_ (hv m hm) ?_
-- 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
m : ℕ
hm : (↑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
have h'm : (↑(m + 1) : ℕ∞) ≤ N
Tactic: have h'm : ((m + 1 : ℕ) : ℕ∞) ≤ N := by
      simpa only [ENat.coe_add, ENat.coe_one] using Order.add_one_le_of_lt hm
-- 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
m : ℕ
hm : (↑m : ℕ∞) < N
h'm : (↑(m + 1) : ℕ∞) ≤ 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
have right : Differentiable 𝕜 (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
  (fun (x : E) ↦
      (∑' (n : α), iteratedFDeriv 𝕜 m (f n) x : ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F))
    x
Tactic: rw [iteratedFDeriv_tsum hf hv h'f hm.le]
-- 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
m : ℕ
hm : (↑m : ℕ∞) < N
h'm : (↑(m + 1) : ℕ∞) ≤ N
⊢ Differentiable 𝕜 (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
    (fun (x : E) ↦
        (∑' (n : α), iteratedFDeriv 𝕜 m (f n) x :
          ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F))
      x
have A : ∀ (n : α) (x : E),
  HasFDerivAt (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m (f n))
    (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x
Tactic: have A n x : HasFDerivAt (iteratedFDeriv 𝕜 m (f n)) (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x :=
      (ContDiff.differentiable_iteratedFDeriv (mod_cast hm)
        (hf n)).differentiableAt.hasFDerivAt
-- 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
m : ℕ
hm : (↑m : ℕ∞) < N
h'm : (↑(m + 1) : ℕ∞) ≤ N
A :
  ∀ (n : α) (x : E),
    HasFDerivAt (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m (f n))
      (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x
⊢ Differentiable 𝕜 (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
    (fun (x : E) ↦
        (∑' (n : α), iteratedFDeriv 𝕜 m (f n) x :
          ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F))
      x
have right : ∀ (n : α) (x : E),
  norm (E := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) ≤
    v (m + 1) n
Tactic: refine differentiable_tsum (hv _ h'm) A fun 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
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
m : ℕ
hm : (↑m : ℕ∞) < N
h'm : (↑(m + 1) : ℕ∞) ≤ N
A :
  ∀ (n : α) (x : E),
    HasFDerivAt (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m (f n))
      (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x
n : α
x : E
⊢ norm (E := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) ≤
    v (m + 1) n
have right : norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (x : Fin (m + 1)) ↦ E) F)
    (iteratedFDeriv 𝕜 (m + 1) (f n) x) ≤
  v (m + 1) n
Tactic: rw [fderiv_iteratedFDeriv, comp_apply, LinearIsometryEquiv.norm_map]
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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 refine : ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N), ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
Tactic: refine contDiff_iff_forall_nat_le.2 fun m hm => ?_
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
⊢ ∀ᶠ (i : α) in cofinite,
    ∀ k ∈ Finset.range (m + 1),
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
          v k i
have rw : ∀ i ∈ Finset.range (m + 1),
  ∀ᶠ (x : α) in cofinite,
    ∀ (x_1 : E),
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i (f x) x_1) ≤
        v i x
Tactic: rw [eventually_all_finset]
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ∀ᶠ (x : α) in cofinite,
    ∀ (x_1 : E),
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i (f x) x_1) ≤
        v i x
have a : (↑i : ℕ∞) ≤ N
Tactic: apply h'f
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ (↑i : ℕ∞) ≤ N
have hi₁ : i ≤ m
Tactic: simp only [Finset.mem_range_succ_iff] at hi
Cleared hypotheses: hi
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          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) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
have ht : t.Finite
Tactic: have ht : Set.Finite t :=
      haveI A :
        ∀ᶠ i in (Filter.cofinite : Filter α),
          ∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x : E, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i := by
        rw [eventually_all_finset]
        intro i hi
        apply h'f
        simp only [Finset.mem_range_succ_iff] at hi
        exact (WithTop.coe_le_coe.2 hi).trans hm
      eventually_cofinite.2 A
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
⊢ (fun (x : E) ↦ ∑' (i : α), f i x) =
    HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
have h : ∀ (x : E),
  ∑' (i : α), f i x =
    HAdd.hAdd (α := (x : E) → F) (β := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x)
      (fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x) 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
x : E
⊢ ∑' (i : α), f i x =
    HAdd.hAdd (α := (x : E) → F) (β := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x)
      (fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x) x
have h : Summable.{u_5, u_1} (α := F) fun (i : α) ↦ f i x
Tactic: refine (Summable.sum_add_tsum_subtype_compl ?_ T).symm
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
x : E
⊢ Summable.{u_5, u_1} (α := F) fun (i : α) ↦ f i x
have h : ∀ᶠ (i : α) in cofinite, ‖f i x‖ ≤ v 0 i
Tactic: refine .of_norm_bounded_eventually (hv 0 zero_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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
x : E
⊢ ∀ᶠ (i : α) in cofinite, ‖f i x‖ ≤ v 0 i
have h : ∀ (i : α)
  (hi :
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 (f i) x) ≤
        v 0 i),
  ‖f i x‖ ≤ v 0 i
Tactic: filter_upwards [h'f 0 zero_le] with i hi
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
m : ℕ
hm : (↑m : ℕ∞) ≤ N
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
have this : (fun (x : E) ↦ ∑' (i : α), f i x) =
  HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
Tactic: have : (fun x => ∑' i, f i x) = (fun x => ∑ i ∈ T, f i x) +
        fun x => ∑' i : { i // i ∉ T }, f i x := by
      ext1 x
      refine (Summable.sum_add_tsum_subtype_compl ?_ T).symm
      refine .of_norm_bounded_eventually (hv 0 zero_le) ?_
      filter_upwards [h'f 0 zero_le] with i hi
      simpa only [norm_iteratedFDeriv_zero] using hi x