case refine'_1
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑n ^ (-b)

case refine'_2
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑(-↑n) ^ (-b)
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑n ^ (-b)
refine'
  summable_int_of_summable_nat (_ : Summable fun n : ℕ => |(n : ℝ)| ^ _)
    (_ : Summable fun n : ℕ => |((-n : ℤ) : ℝ)| ^ _)
case refine'_1
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑n ^ (-b)

case refine'_2
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑n ^ (-b)
case refine'_1
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑n ^ (-b)

case refine'_2
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑(-↑n) ^ (-b)
on_goal 2 => simp_rw [Int.cast_neg, Int.cast_ofNat, abs_neg]
no goals
case refine'_1
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑n ^ (-b)

case refine'_2
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑n ^ (-b)
all_goals
  simp_rw [fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]
  rwa [Real.summable_nat_rpow, neg_lt_neg_iff]
case refine'_2
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑n ^ (-b)
case refine'_2
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑(-↑n) ^ (-b)
simp_rw [Int.cast_neg, Int.cast_ofNat, abs_neg]
case refine'_2
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑n ^ (-b)
case refine'_2
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑(-↑n) ^ (-b)
simp_rw [Int.cast_neg, Int.cast_ofNat, abs_neg]
case refine'_2
b : ℝ
hb : 1 < b
⊢ Summable fun n => ↑n ^ (-b)
case refine'_2
b : ℝ
hb : 1 < b
⊢ Summable fun n => abs ↑n ^ (-b)
simp_rw [fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]
no goals
case refine'_2
b : ℝ
hb : 1 < b
⊢ Summable fun n => ↑n ^ (-b)
rwa [Real.summable_nat_rpow, neg_lt_neg_iff]