avoiding `rename_i`

Stream: new members

[Arien Malec]

Is there a way to avoid rename_i here?

The Lean 3 proof named x; over in Lean 4, ext leaves x with a hygenic name

-- TODO: eliminate `rename_i`
theorem core_res (f : α → β) (s : Set α) (t : Set β) : (res f s).core t = sᶜ ∪ f ⁻¹' t := by
  ext
  rename_i x
  rw [mem_core_res]
  by_cases h : x ∈ s <;> simp [h]

[Arien Malec]

Its in mathlib4#1179 if you want to play with the actual code.

[Mario Carneiro]

ext x?