α : Type ?u.462750
β : Type ?u.462753
ι : Type ?u.462756
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ (1 / m) ^ a
α : Type ?u.462750
β : Type ?u.462753
ι : Type ?u.462756
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
⊢ Summable fun i => 1 / m ^ f i
refine'
  summable_of_nonneg_of_le (fun a => one_div_nonneg.mpr (pow_nonneg (zero_le_one.trans hm.le) _))
    (fun a => _)
    (summable_geometric_of_lt_1 (one_div_nonneg.mpr (zero_le_one.trans hm.le))
      ((one_div_lt (zero_lt_one.trans hm) zero_lt_one).mpr (one_div_one.le.trans_lt hm)))
α : Type ?u.462750
β : Type ?u.462753
ι : Type ?u.462756
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ 1 / m ^ a
α : Type ?u.462750
β : Type ?u.462753
ι : Type ?u.462756
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ (1 / m) ^ a
rw [div_pow, one_pow]
no goals
α : Type ?u.462750
β : Type ?u.462753
ι : Type ?u.462756
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ 1 / m ^ a
refine' (one_div_le_one_div _ _).mpr (pow_le_pow hm.le (fi a)) <;>
  exact pow_pos (zero_lt_one.trans hm) _