c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
c : ℝ
hc : 1 < c
i : ℕ
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
have cpos : 0 < c := zero_lt_one.trans hc
case inl
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ 0 ≤ ↑⌊c ^ 0⌋₊

case inr
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i > 0
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
rcases Nat.eq_zero_or_pos i with (rfl | hi)
case inr
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i > 0
hident : 1 ≤ i
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
case inr
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i > 0
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
have hident : 1 ≤ i := hi
no goals
case inr
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i > 0
hident : 1 ≤ i
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
calc
  (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹ := by ring
  _ ≤ c ^ i - 1 := by
    simpa only [← div_eq_mul_inv, sub_le_sub_iff_left, one_le_div cpos, pow_one] using
      pow_le_pow hc.le hident
  _ ≤ ⌊c ^ i⌋₊ := (Nat.sub_one_lt_floor _).le
no goals
case inl
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ 0 ≤ ↑⌊c ^ 0⌋₊
simp only [pow_zero, Nat.floor_one, Nat.cast_one, mul_one, sub_le_self_iff, inv_nonneg, cpos.le]
no goals
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i > 0
hident : 1 ≤ i
⊢ (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹
ring
no goals
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i > 0
hident : 1 ≤ i
⊢ c ^ i - c ^ i * c⁻¹ ≤ c ^ i - 1
simpa only [← div_eq_mul_inv, sub_le_sub_iff_left, one_le_div cpos, pow_one] using
  pow_le_pow hc.le hident