How does one avoid `rename_i` here?

Stream: mathlib4

[Arien Malec]

I have

      match c₁, c₂, h with
      -- TODO: eliminate `rename_i`
      | _, _, Or.inl (Eq.refl _) => by rename_i c; cases' destruct c with b cb <;> simp

where the original Lean 3 was:

    exact match c₁, c₂, h with
    | _, _, or.inl (eq.refl c) := begin cases destruct c with b cb; simp end

But Lean 4 complains unknown identifier 'c'