-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem changeOrigin_eval (h : (‖x‖₊ + ‖y‖₊ : ℝ≥0∞) < p.radius) :
    (p.changeOrigin x).sum y = p.sum (x + y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
radius_pos : 0 < p.radius
x_mem_ball : x ∈ EMetric.ball 0 p.radius
y_mem_ball : y ∈ EMetric.ball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ EMetric.ball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
hsf : Summable f
⊢ HasSum f ((p.changeOrigin x).sum y)

Tactic:
refine HasSum.sigma_of_hasSum ((p.changeOrigin x).summable y_mem_ball).hasSum (fun k => ?_) hsf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
radius_pos : 0 < p.radius
x_mem_ball : x ∈ EMetric.ball 0 p.radius
y_mem_ball : y ∈ EMetric.ball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ EMetric.ball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
hsf : Summable f
k : ℕ
⊢ HasSum (fun c => f ⟨k, c⟩) ((p.changeOrigin x k) fun x => y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
radius_pos : 0 < p.radius
x_mem_ball : x ∈ EMetric.ball 0 p.radius
y_mem_ball : y ∈ EMetric.ball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ EMetric.ball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
hsf : Summable f
hf : HasSum f ((p.changeOrigin x).sum y)
⊢ HasSum (f ∘ ⇑changeOriginIndexEquiv.symm) (p.sum (x + y))

Tactic:
refine HasSum.sigma_of_hasSum
  (p.hasSum x_add_y_mem_ball) (fun n => ?_) (changeOriginIndexEquiv.symm.summable_iff.2 hsf)

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
radius_pos : 0 < p.radius
x_mem_ball : x ∈ EMetric.ball 0 p.radius
y_mem_ball : y ∈ EMetric.ball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ EMetric.ball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
hsf : Summable f
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
⊢ HasSum (fun c => (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩) ((p n) fun x_1 => x + y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
radius_pos : 0 < p.radius
x_mem_ball : x ∈ EMetric.ball 0 p.radius
⊢ ‖y‖ₑ < p.radius - ↑‖x‖₊

Tactic:
rwa [lt_tsub_iff_right, add_comm]

Result:
no goals

Proof state:
case mk.mk.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
radius_pos : 0 < p.radius
x_mem_ball : x ∈ EMetric.ball 0 p.radius
y_mem_ball : y ∈ EMetric.ball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ EMetric.ball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
⊢ ‖f ⟨k, ⟨l, ⟨s, hs⟩⟩⟩‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k

Tactic:
exact p.nnnorm_changeOriginSeriesTerm_apply_le _ _ _ _ _ _

Result:
no goals