-- Mathlib/Analysis/Calculus/SmoothSeries.lean
theorem summable_of_summable_hasDerivAt_of_isPreconnected (hu : Summable u) (ht : IsOpen t)
    (h't : IsPreconnected t) (hg : ∀ n y, y ∈ t → HasDerivAt (g n) (g' n y) y)
    (hg' : ∀ n y, y ∈ t → ‖g' n y‖ ≤ u n) (hy₀ : y₀ ∈ t) (hg0 : Summable (g · y₀))
    (hy : y ∈ t) : Summable fun n => g n y

Proof state:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun x => g x y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y
⊢ Summable fun n => g n y

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

Result:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun x => g x y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y
⊢ ∀ (n : α), ∀ x ∈ t, ‖ContinuousLinearMap.smulRight 1 (g' n x)‖ ≤ u n

Proof state:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen 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 fun x => g x y₀
hy : y ∈ t
⊢ Summable fun n => g n y

Tactic:
simp_rw [hasDerivAt_iff_hasFDerivAt] at hg

Result:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun x => g x y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y
⊢ Summable fun n => g n y

Proof state:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun x => g x y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y
⊢ ∀ (n : α), ∀ x ∈ t, ‖ContinuousLinearMap.smulRight 1 (g' n x)‖ ≤ u n

Tactic:
simpa only [ContinuousLinearMap.norm_smulRight_apply, norm_one, one_mul]

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun x => g x y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y
⊢ ∀ (n : α), ∀ x ∈ t, ‖ContinuousLinearMap.smulRight 1 (g' n x)‖ ≤ u n

Tactic:
simpa? says simpa only [ContinuousLinearMap.norm_smulRight_apply, norm_one, one_mul]

Result:
no goals