case inl
α : Type ?u.447120
β : Type ?u.447123
ι : Type ?u.447126
inst✝ : PseudoMetricSpace α
r : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ 0 * r ^ n
⊢ HasSum (fun n => 0 * r ^ n) (0 / (1 - r))

case inr.intro
α : Type ?u.447120
β : Type ?u.447123
ι : Type ?u.447126
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n => C * r ^ n) (C / (1 - r))
α : Type ?u.447120
β : Type ?u.447123
ι : Type ?u.447126
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ HasSum (fun n => C * r ^ n) (C / (1 - r))
rcases sign_cases_of_C_mul_pow_nonneg fun n => dist_nonneg.trans (hu n) with (rfl | ⟨_, r₀⟩)
no goals
case inl
α : Type ?u.447120
β : Type ?u.447123
ι : Type ?u.447126
inst✝ : PseudoMetricSpace α
r : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ 0 * r ^ n
⊢ HasSum (fun n => 0 * r ^ n) (0 / (1 - r))
simp [hasSum_zero]
case inr.intro
α : Type ?u.447120
β : Type ?u.447123
ι : Type ?u.447126
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n => r ^ n) (1 - r)⁻¹
case inr.intro
α : Type ?u.447120
β : Type ?u.447123
ι : Type ?u.447126
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n => C * r ^ n) (C / (1 - r))
refine' HasSum.mul_left C _
no goals
case inr.intro
α : Type ?u.447120
β : Type ?u.447123
ι : Type ?u.447126
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n => r ^ n) (1 - r)⁻¹
simpa using hasSum_geometric_of_lt_1 r₀ hr