-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem summable_powerSeries_of_norm_lt {w z : α}
    (h : CauchySeq fun n ↦ ∑ i ∈ range n, f i * w ^ i) (hz : ‖z‖ < ‖w‖) :
    Summable fun n ↦ f n * z ^ n

Proof state:
case intro
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
⊢ CauchySeq fun s => ∑ b ∈ s, f b * z ^ b

Tactic:
refine cauchySeq_finset_of_geometric_bound (r := ‖z‖ / ‖w‖) (C := C) ((div_lt_one hw).mpr hz)
  (fun n ↦ ?_)

Result:
case intro
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n * z ^ n‖ ≤ C * (‖z‖ / ‖w‖) ^ n

Proof state:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
⊢ Summable fun n => f n * z ^ n

Tactic:
have hw : 0 < ‖w‖ := (norm_nonneg z).trans_lt hz

Result:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
⊢ Summable fun n => f n * z ^ n

Proof state:
case intro
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n

Tactic:
conv at hC => enter [n]; rw [norm_mul, norm_pow, ← _root_.le_div_iff₀ (by positivity)]

Result:
case intro
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n
n : ℕ
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n

Proof state:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
⊢ Summable fun n => f n * z ^ n

Tactic:
obtain ⟨C, hC⟩ := exists_norm_le_of_cauchySeq h

Result:
case intro
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
⊢ Summable fun n => f n * z ^ n

Proof state:
case intro
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
⊢ Summable fun n => f n * z ^ n

Tactic:
rw [summable_iff_cauchySeq_finset]

Result:
case intro
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
⊢ CauchySeq fun s => ∑ b ∈ s, f b * z ^ b

Proof state:
case intro
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n
n : ℕ
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n

Tactic:
exact mul_le_mul_of_nonneg_right (hC n) (pow_nonneg (norm_nonneg z) n)

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n * z ^ n‖ ≤ C * (‖z‖ / ‖w‖) ^ n

Tactic:
rw [norm_mul, norm_pow, div_pow, ← mul_comm_div]

Result:
case intro
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n

Proof state:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n✝ n : ℕ
⊢ 0 < ‖w‖ ^ n

Tactic:
positivity

Result:
no goals