α : Type ?u.147129
β : Type ?u.147132
ι : Type ?u.147135
K : Type u_1
inst✝ : NormedField K
ξ : K
h : Summable fun n => ξ ^ n
⊢ ‖ξ‖ < 1
α : Type ?u.147129
β : Type ?u.147132
ι : Type ?u.147135
K : Type u_1
inst✝ : NormedField K
ξ : K
⊢ (Summable fun n => ξ ^ n) ↔ ‖ξ‖ < 1
refine' ⟨fun h ↦ _, summable_geometric_of_norm_lt_1⟩
case intro
α : Type ?u.147129
β : Type ?u.147132
ι : Type ?u.147135
K : Type u_1
inst✝ : NormedField K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : dist (ξ ^ k) 0 < 1
⊢ ‖ξ‖ < 1
α : Type ?u.147129
β : Type ?u.147132
ι : Type ?u.147135
K : Type u_1
inst✝ : NormedField K
ξ : K
h : Summable fun n => ξ ^ n
⊢ ‖ξ‖ < 1
obtain ⟨k : ℕ, hk : dist (ξ ^ k) 0 < 1⟩ :=
  (h.tendsto_cofinite_zero.eventually (ball_mem_nhds _ zero_lt_one)).exists
case intro
α : Type ?u.147129
β : Type ?u.147132
ι : Type ?u.147135
K : Type u_1
inst✝ : NormedField K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1
⊢ ‖ξ‖ < 1
case intro
α : Type ?u.147129
β : Type ?u.147132
ι : Type ?u.147135
K : Type u_1
inst✝ : NormedField K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : dist (ξ ^ k) 0 < 1
⊢ ‖ξ‖ < 1
simp only [norm_pow, dist_zero_right] at hk
case intro
α : Type ?u.147129
β : Type ?u.147132
ι : Type ?u.147135
K : Type u_1
inst✝ : NormedField K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1 ^ k
⊢ ‖ξ‖ < 1
case intro
α : Type ?u.147129
β : Type ?u.147132
ι : Type ?u.147135
K : Type u_1
inst✝ : NormedField K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1
⊢ ‖ξ‖ < 1
rw [← one_pow k] at hk
no goals
case intro
α : Type ?u.147129
β : Type ?u.147132
ι : Type ?u.147135
K : Type u_1
inst✝ : NormedField K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1 ^ k
⊢ ‖ξ‖ < 1
exact lt_of_pow_lt_pow _ zero_le_one hk