case zero
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ ∑ i in Ico 1 zero, a / b ^ i ≤ a / (b - 1)

case succ
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i in Ico 1 (succ n), a / b ^ i ≤ a / (b - 1)
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i in Ico 1 n, a / b ^ i ≤ a / (b - 1)
cases' n with n
case succ
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i in Ico 1 (succ n), a / b ^ i ≤ a + a / (b - 1)
case succ
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i in Ico 1 (succ n), a / b ^ i ≤ a / (b - 1)
rw [← add_le_add_iff_left a]
no goals
case succ
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i in Ico 1 (succ n), a / b ^ i ≤ a + a / (b - 1)
calc
  (a + ∑ i : ℕ in Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i : ℕ in Ico 1 n.succ, a / b ^ i := by
    rw [pow_zero, Nat.div_one]
  _ = ∑ i in range n.succ, a / b ^ i := by
    rw [range_eq_Ico, ← Nat.Ico_insert_succ_left (Nat.succ_pos _), sum_insert]
    exact fun h => zero_lt_one.not_le (mem_Ico.1 h).1
  _ ≤ a * b / (b - 1) := Nat.geom_sum_le hb a _
  _ = (a * 1 + a * (b - 1)) / (b - 1) := by
    rw [← mul_add, add_tsub_cancel_of_le (one_le_two.trans hb)]
  _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
case zero
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a / (b - 1)
case zero
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ ∑ i in Ico 1 zero, a / b ^ i ≤ a / (b - 1)
rw [zero_eq, Ico_eq_empty_of_le (zero_le_one' ℕ), sum_empty]
no goals
case zero
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a / (b - 1)
exact Nat.zero_le _
no goals
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i in Ico 1 (succ n), a / b ^ i = a / b ^ 0 + ∑ i in Ico 1 (succ n), a / b ^ i
rw [pow_zero, Nat.div_one]
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ¬0 ∈ Ico (succ 0) (succ n)
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i in Ico 1 (succ n), a / b ^ i = ∑ i in range (succ n), a / b ^ i
rw [range_eq_Ico, ← Nat.Ico_insert_succ_left (Nat.succ_pos _), sum_insert]
no goals
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ¬0 ∈ Ico (succ 0) (succ n)
exact fun h => zero_lt_one.not_le (mem_Ico.1 h).1
no goals
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a * b / (b - 1) = (a * 1 + a * (b - 1)) / (b - 1)
rw [← mul_add, add_tsub_cancel_of_le (one_le_two.trans hb)]
no goals
α : Type u
β : Type ?u.223090
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (a * 1 + a * (b - 1)) / (b - 1) = a + a / (b - 1)
rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]