-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem tsum_geometric_le_of_norm_lt_one (x : R) (h : ‖x‖ < 1) :
    ‖∑' n : ℕ, x ^ n‖ ≤ ‖(1 : R)‖ - 1 + (1 - ‖x‖)⁻¹

Proof state:
case neg
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n => x ^ n
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
nontriviality R

Result:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n => x ^ n
a✝ : Nontrivial R
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Proof state:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ HasSum (fun b => ‖x‖ ^ (b + 1)) ((1 - ‖x‖)⁻¹ - 1)

Tactic:
convert (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h)

Result:
case h.e'_6.h.e'_6
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ 1 = ∑ i ∈ Finset.range 1, ‖x‖ ^ i

Proof state:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n => x ^ n
a✝ : Nontrivial R
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
have : 1 ≤ ‖(1 : R)‖ := one_le_norm_one R

Result:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n => x ^ n
a✝ : Nontrivial R
this : 1 ≤ ‖1‖
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Proof state:
case neg
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n => x ^ n
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
simp [tsum_eq_zero_of_not_summable hx]

Result:
case neg
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n => x ^ n
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Proof state:
case pos
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ ‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
have : ‖∑' b : ℕ, (fun n ↦ x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1 := by
  refine tsum_of_norm_bounded ?_ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)
  convert (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h)
  simp

Result:
case pos
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
this : ‖∑' (b : ℕ), (fun n => x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1
⊢ ‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Proof state:
case pos
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ ‖1 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
refine le_trans (norm_add_le _ _) ?_

Result:
case pos
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ ‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Proof state:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n => x ^ n
a✝ : Nontrivial R
this : 1 ≤ ‖1‖
⊢ 0 ≤ 1 - ‖x‖

Tactic:
linarith

Result:
no goals

Proof state:
case h.e'_6.h.e'_6
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ 1 = ∑ i ∈ Finset.range 1, ‖x‖ ^ i

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
by_cases hx : Summable (fun n ↦ x ^ n)

Result:
case pos
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

case neg
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n => x ^ n
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Proof state:
case pos
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
rw [tsum_eq_zero_add hx]

Result:
case pos
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ ‖x ^ 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Proof state:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n => x ^ n
a✝ : Nontrivial R
this : 1 ≤ ‖1‖
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
have : 0 ≤ (1 - ‖x‖) ⁻¹ := inv_nonneg.2 (by linarith)

Result:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n => x ^ n
a✝ : Nontrivial R
this✝ : 1 ≤ ‖1‖
this : 0 ≤ (1 - ‖x‖)⁻¹
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Proof state:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n => x ^ n
a✝ : Nontrivial R
this✝ : 1 ≤ ‖1‖
this : 0 ≤ (1 - ‖x‖)⁻¹
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
linarith

Result:
no goals

Proof state:
case pos
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ ‖x ^ 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
simp only [_root_.pow_zero]

Result:
case pos
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ ‖1 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Proof state:
case pos
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
this : ‖∑' (b : ℕ), (fun n => x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1
⊢ ‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
linarith

Result:
no goals

Proof state:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ ‖∑' (b : ℕ), (fun n => x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1

Tactic:
refine tsum_of_norm_bounded ?_ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)

Result:
R : Type u_2
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n => x ^ n
⊢ HasSum (fun b => ‖x‖ ^ (b + 1)) ((1 - ‖x‖)⁻¹ - 1)