abel idempotence

Stream: general

[Johan Commelin]

Should abel be idempotent?

import analysis.specific_limits

example {α : Type u_1} [normed_group α] {r C : ℝ} (n : ℕ)
  {f : ℕ → α} (hf : ∀ (n : ℕ), ∥f n∥ ≤ C * r ^ n) :
  -((∑ (i : ℕ) in range n, f i) - (f n + ∑ (x : ℕ) in range n, f x)) = f n :=
begin
  abel, -- does not close the goal
  abel, -- closes the goal
end

[Kevin Buzzard]

I saw this once with ring and what was happening was that there was some metavariable goal

[Kevin Buzzard]

#mwe

[Reid Barton]

I just deleted {ring, ring} from my project today!

[Rob Lewis]

@Bryan Gin-ge Chen I hope the banana means that I'm not the only one with Raffi stuck in my head now.

[Bryan Gin-ge Chen]

Yes! Though I've never much minded having songs stuck in my head.

Slightly more on topic, is there a way to cook up examples which require {ring, ring, ring} (or even more)?