-- Mathlib/Analysis/Calculus/SmoothSeries.lean
theorem contDiff_tsum_of_eventually (hf : ∀ i, ContDiff 𝕜 N (f i))
    (hv : ∀ k : ℕ, k ≤ N → Summable (v k))
    (h'f : ∀ k : ℕ, k ≤ N →
      ∀ᶠ i in (Filter.cofinite : Filter α), ∀ x : E, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) :
    ContDiff 𝕜 N fun x => ∑' i, f i x

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : t.Finite
T : Finset α := ht.toFinset
this : (fun x => ∑' (i : α), f i x) = (fun x => ∑ i ∈ T, f i x) + fun x => ∑' (i : { i // i ∉ T }), f (↑i) x
h'u : ∀ (k : ℕ), ↑k ≤ ↑m → Summable (v k ∘ Subtype.val)
⊢ ContDiff 𝕜 ↑m fun x => ∑' (i : { i // i ∉ T }), f (↑i) x

Tactic:
refine contDiff_tsum (fun i => (hf i).of_le (mod_cast hm)) h'u ?_

Result:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : t.Finite
T : Finset α := ht.toFinset
this : (fun x => ∑' (i : α), f i x) = (fun x => ∑ i ∈ T, f i x) + fun x => ∑' (i : { i // i ∉ T }), f (↑i) x
h'u : ∀ (k : ℕ), ↑k ≤ ↑m → Summable (v k ∘ Subtype.val)
⊢ ∀ (k : ℕ) (i : { i // i ∉ T }) (x : E), ↑k ≤ ↑m → ‖iteratedFDeriv 𝕜 k (f ↑i) x‖ ≤ (v k ∘ Subtype.val) i

Proof state:
case h
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : t.Finite
T : Finset α := ht.toFinset
x : E
i : α
hi : ∀ (x : E), ‖iteratedFDeriv 𝕜 0 (f i) x‖ ≤ v 0 i
⊢ ‖f i x‖ ≤ v 0 i

Tactic:
simpa only [norm_iteratedFDeriv_zero] using hi x

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
⊢ ContDiff 𝕜 ↑N fun x => ∑' (i : α), f i x

Tactic:
classical
  refine contDiff_iff_forall_nat_le.2 fun m hm => ?_
  let t : Set α :=
    { i : α | ¬∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i }
  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
  let T : Finset α := ht.toFinset
  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 (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
  rw [this]
  apply (ContDiff.sum fun i _ => (hf i).of_le (mod_cast hm)).add
  have h'u : ∀ k : ℕ, (k : ℕ∞) ≤ m → Summable (v k ∘ ((↑) : { i // i ∉ T } → α)) := fun k hk =>
    (hv k (hk.trans hm)).subtype _
  refine contDiff_tsum (fun i => (hf i).of_le (mod_cast hm)) h'u ?_
  rintro k ⟨i, hi⟩ x hk
  simp only [t, T, Finite.mem_toFinset, mem_setOf_eq, Finset.mem_range, not_forall, not_le,
    exists_prop, not_exists, not_and, not_lt] at hi
  exact hi k (Nat.lt_succ_iff.2 (WithTop.coe_le_coe.1 hk)) x

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
⊢ ∀ i ∈ Finset.range (m + 1), ∀ᶠ (x : α) in cofinite, ∀ (x_1 : E), ‖iteratedFDeriv 𝕜 i (f x) x_1‖ ≤ v i x

Tactic:
intro i hi

Result:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ∀ᶠ (x : α) in cofinite, ∀ (x_1 : E), ‖iteratedFDeriv 𝕜 i (f x) x_1‖ ≤ v i x

Proof state:
case mk
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : t.Finite
T : Finset α := ht.toFinset
this : (fun x => ∑' (i : α), f i x) = (fun x => ∑ i ∈ T, f i x) + fun x => ∑' (i : { i // i ∉ T }), f (↑i) x
h'u : ∀ (k : ℕ), ↑k ≤ ↑m → Summable (v k ∘ Subtype.val)
k : ℕ
i : α
hi✝ : i ∉ T
x : E
hk : ↑k ≤ ↑m
hi : ∀ x < m + 1, ∀ (x_1 : E), ‖iteratedFDeriv 𝕜 x (f i) x_1‖ ≤ v x i
⊢ ‖iteratedFDeriv 𝕜 k (f ↑⟨i, hi✝⟩) x‖ ≤ (v k ∘ Subtype.val) ⟨i, hi✝⟩

Tactic:
exact hi k (Nat.lt_succ_iff.2 (WithTop.coe_le_coe.1 hk)) x

Result:
no goals