awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
hx : x ∈ s
A : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))
refine :
  ∀ (t : Finset α) (y : E) (hy : y ∈ s),
    HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∑ n ∈ t, f n x) (∑ n ∈ t, f' n y) y
⊢ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑' (n : α), f n y) (∑' (n : α), f' n x) x

Tactic:
refine hasFDerivAt_of_tendstoUniformlyOn hs (tendstoUniformlyOn_tsum hu hf')
      (fun t y hy => ?_) A hx

Premises used: tendstoUniformlyOn_tsum, hasFDerivAt_of_tendstoUniformlyOn
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
hx : x ∈ s
A : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))
t : Finset α
y : E
hy : y ∈ s
⊢ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∑ n ∈ t, f n x) (∑ n ∈ t, f' n y) y

Tactic:
HasFDerivAt.fun_sum fun n _ => hf n y hy

Premises used: HasFDerivAt.fun_sum
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
hx : x ∈ s
A : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))
t : Finset α
y : E
hy : y ∈ s
⊢ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∑ n ∈ t, f n x) (∑ n ∈ t, f' n y) y

Tactic:
exact HasFDerivAt.fun_sum fun n _ => hf n y hy

Premises used: HasFDerivAt.fun_sum
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
hx : x ∈ s
have : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))
have₁ :
  ∀ (A : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))),
    HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑' (n : α), f n y) (∑' (n : α), f' n x) x
have₂ : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))
have₃ have₄ :
  ∀ (A : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))),
    HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑' (n : α), f n y) (∑' (n : α), f' n x) x
have₅ :
  ∀ (A : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x)))
    (t : Finset α) (y : E) (hy : y ∈ s),
    HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∑ n ∈ t, f n x) (∑ n ∈ t, f' n y) y
⊢ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑' (n : α), f n y) (∑' (n : α), f' n x) x

Tactic:
classical
    have A :
      ∀ x : E, x ∈ s → Tendsto (fun t : Finset α => ∑ n ∈ t, f n x) atTop (𝓝 (∑' n, f n x)) := by
      intro y hy
      apply Summable.hasSum
      exact summable_of_summable_hasFDerivAt_of_isPreconnected hu hs h's hf hf' hx₀ hf0 hy
    refine hasFDerivAt_of_tendstoUniformlyOn hs (tendstoUniformlyOn_tsum hu hf')
      (fun t y hy => ?_) A hx
    exact HasFDerivAt.fun_sum fun n _ => hf n y hy
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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, HasDerivAt (g n) (g' n y) y
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
⊢ ∀ (n : α), ∀ y ∈ t, HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y

Tactic:
simp_rw [hasDerivAt_iff_hasFDerivAt] at hg ⊢

Premises used: hasDerivAt_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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 (y : 𝕜) ↦ ∑' (n : α), g n y)
    (∑' (n : α), ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y

Tactic:
hasFDerivAt_tsum_of_isPreconnected hu ht h't hg ?_ hy₀ hg0 hy

Premises used: hasFDerivAt_tsum_of_isPreconnected
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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))
convert! : ∀ (n : α), ∀ x ∈ t, norm (E := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n x)) ≤ u n
⊢ HasFDerivAt.{u_3, u_3, u_5} (𝕜 := 𝕜) (F := F) (fun (z : 𝕜) ↦ ∑' (n : α), g n z)
    (ContinuousLinearMap.toSpanSingleton 𝕜 (∑' (n : α), g' n y)) y

Tactic:
convert! hasFDerivAt_tsum_of_isPreconnected hu ht h't hg ?_ hy₀ hg0 hy

Premises used: hasFDerivAt_tsum_of_isPreconnected
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
e_4 : Eq.{u_3 + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : 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:
(ContinuousLinearMap.smulRightL 𝕜 𝕜 F 1).map_tsum <|
      .of_norm_bounded hu fun n ↦ hg' n y hy

Premises used: ContinuousLinearMap.smulRight, ContinuousLinearMap.map_tsum, ContinuousLinearMap.smulRightL, ContinuousLinearMap.toSpanSingleton, Summable.of_norm_bounded, OfNat.ofNat, DFunLike.coe, LinearMap.toSpanSingleton
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
e_4 : Eq.{u_3 + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : 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:
exact (ContinuousLinearMap.smulRightL 𝕜 𝕜 F 1).map_tsum <|
      .of_norm_bounded hu fun n ↦ hg' n y hy

Premises used: ContinuousLinearMap.map_tsum, ContinuousLinearMap.smulRightL, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
⊢ ∀ (n : α), ∀ x ∈ t, norm (E := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n x)) ≤ u n

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
x₀ : E
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
x : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_1 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x

Tactic:
summable_of_summable_hasFDerivAt_of_isPreconnected hu isOpen_univ isPreconnected_univ
    (fun n x _ => hf n x) (fun n x _ => hf' n x) (mem_univ _) hf0 (mem_univ _)

Premises used: isOpen_univ, Set.mem_univ, PreconnectedSpace.isPreconnected_univ, summable_of_summable_hasFDerivAt_of_isPreconnected
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
x₀ : E
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
x : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_1 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x

Tactic:
exact summable_of_summable_hasFDerivAt_of_isPreconnected hu isOpen_univ isPreconnected_univ
    (fun n x _ => hf n x) (fun n x _ => hf' n x) (mem_univ _) hf0 (mem_univ _)

Premises used: isOpen_univ, Set.mem_univ, PreconnectedSpace.isPreconnected_univ, summable_of_summable_hasFDerivAt_of_isPreconnected
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y₀
y : 𝕜
⊢ Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y

Tactic:
summable_of_summable_hasDerivAt_of_isPreconnected hu isOpen_univ isPreconnected_univ
    (fun n x _ => hg n x) (fun n x _ => hg' n x) (mem_univ _) hg0 (mem_univ _)

Premises used: isOpen_univ, summable_of_summable_hasDerivAt_of_isPreconnected, Set.mem_univ, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y₀
y : 𝕜
⊢ Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y

Tactic:
exact summable_of_summable_hasDerivAt_of_isPreconnected hu isOpen_univ isPreconnected_univ
    (fun n x _ => hg n x) (fun n x _ => hg' n x) (mem_univ _) hg0 (mem_univ _)

Premises used: isOpen_univ, summable_of_summable_hasDerivAt_of_isPreconnected, Set.mem_univ, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
x₀ : E
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
x : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑' (n : α), f n y) (∑' (n : α), f' n x) x

Tactic:
hasFDerivAt_tsum_of_isPreconnected hu isOpen_univ isPreconnected_univ
    (fun n x _ => hf n x) (fun n x _ => hf' n x) (mem_univ _) hf0 (mem_univ _)

Premises used: isOpen_univ, Set.mem_univ, PreconnectedSpace.isPreconnected_univ, hasFDerivAt_tsum_of_isPreconnected
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
x₀ : E
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
x : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑' (n : α), f n y) (∑' (n : α), f' n x) x

Tactic:
exact hasFDerivAt_tsum_of_isPreconnected hu isOpen_univ isPreconnected_univ
    (fun n x _ => hf n x) (fun n x _ => hf' n x) (mem_univ _) hf0 (mem_univ _)

Premises used: isOpen_univ, Set.mem_univ, PreconnectedSpace.isPreconnected_univ, hasFDerivAt_tsum_of_isPreconnected
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y₀
y : 𝕜
⊢ HasDerivAt.{u_3, u_5} (F := F) (fun (z : 𝕜) ↦ ∑' (n : α), g n z) (∑' (n : α), g' n y) y

Tactic:
hasDerivAt_tsum_of_isPreconnected hu isOpen_univ isPreconnected_univ
    (fun n y _ => hg n y) (fun n y _ => hg' n y) (mem_univ _) hg0 (mem_univ _)

Premises used: hasDerivAt_tsum_of_isPreconnected, isOpen_univ, Set.mem_univ, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y₀
y : 𝕜
⊢ HasDerivAt.{u_3, u_5} (F := F) (fun (z : 𝕜) ↦ ∑' (n : α), g n z) (∑' (n : α), g' n y) y

Tactic:
exact hasDerivAt_tsum_of_isPreconnected hu isOpen_univ isPreconnected_univ
    (fun n y _ => hg n y) (fun n y _ => hg' n y) (mem_univ _) hg0 (mem_univ _)

Premises used: hasDerivAt_tsum_of_isPreconnected, isOpen_univ, Set.mem_univ, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
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
⊢ 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₀
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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₀
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
⊢ Differentiable.{u_3, u_4, u_5} 𝕜 (F := F) fun (y : E) ↦ ∑' (n : α), f n y

Tactic:
rcases h with ⟨x₀, hf0⟩
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
x₀ : E
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
x : E
⊢ DifferentiableAt.{u_3, u_4, u_5} 𝕜 (F := F) (fun (y : E) ↦ ∑' (n : α), f n y) x

Tactic:
(hasFDerivAt_tsum hu hf hf' hf0 x).differentiableAt

Premises used: HasFDerivAt.differentiableAt, hasFDerivAt_tsum
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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
x₀ : E
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
x : E
⊢ DifferentiableAt.{u_3, u_4, u_5} 𝕜 (F := F) (fun (y : E) ↦ ∑' (n : α), f n y) x

Tactic:
exact (hasFDerivAt_tsum hu hf hf' hf0 x).differentiableAt

Premises used: HasFDerivAt.differentiableAt, hasFDerivAt_tsum
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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₀
h₁ : ∀ (x : E), Eq.{u_5 + 1} (α := F) (∑' (n : α), f n x) (0 x)
⊢ Eq (α := (x : E) → F) (fun (x : E) ↦ ∑' (n : α), f n x) 0

Tactic:
ext1 x
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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₀
x : E
⊢ Eq.{u_5 + 1} (α := F) (∑' (n : α), f n x) (0 x)

Tactic:
tsum_eq_zero_of_not_summable (h x)

Premises used: tsum_eq_zero_of_not_summable
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
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₀
x : E
⊢ Eq.{u_5 + 1} (α := F) (∑' (n : α), f n x) (0 x)

Tactic:
exact tsum_eq_zero_of_not_summable (h x)

Premises used: tsum_eq_zero_of_not_summable