looping in `simp` set

Stream: mathlib4

[Jireh Loreaux]

I found a fun problem while fixing !4#4182. We have a loop in our simp set (even prior to this file)

import Mathlib.Analysis.SpecialFunctions.Pow.NNReal

example {p : ℕ} : Summable (fun n => (n ^ p)⁻¹ : ℕ → ℝ) := by
  simp? (config := { singlePass := true }) -- Real.rpow_nat_cast, summable_unop
  simp? (config := { singlePass := true }) -- MulOpposite.op_inv, summable_op
  simp? (config := { singlePass := true }) -- MulOpposite.op_pow, MulOpposite.unop_inv, summable_unop
  simp? (config := { singlePass := true }) -- MulOpposite.op_natCast, MulOpposite.unop_pow, MulOpposite.op_inv, summable_op
  simp? (config := { singlePass := true }) -- MulOpposite.unop_natCast, MulOpposite.op_pow, MulOpposite.unop_inv, summable_unop
  -- now the last two simp calls just loop
  -- note: `simp` times out with `whnf`, it doesn't complain about maximum recursion depth, which is what I would have expected.

I'm especially confused at the first pass, which applies summable_unop. It seems to me that this lemma shouldn't be firing. I assume it has something to do with our new PreOpposite approach.

[Jireh Loreaux]

To be clear, the looping behavior may only be a symptom of this other problem about lemmas firing when they shouldn't.