Possible to remove rename_i here?

Stream: mathlib4

[Arien Malec]

I have

private def decidable_good : DecidablePred (good p)
  | n => by cases' n with a a <;>
         unfold good <;> rename_i x <;> cases x <;> dsimp <;> infer_instance

x is introduced by the unfold. I don't think it's possible to name x during the unfold?

[Gabriel Ebner]

Can you post the definition of good as well? #mwe