change bound variable name

Stream: new members

[Horatiu Cheval]

Can I change the name of a bound variable in a hypothesis? For example to rename the x inside of forall to y in the following

example (h : ∀ x : ℕ, x = x) : true :=
begin
/-
h : ∀ (x : ℕ), x = x
⊢ true
-/
-- change h to
-- h : ∀ (y : ℕ), y = y
end

[Kevin Buzzard]

Did you try the change tactic?

[Adam Topaz]

You can be lazy with change too, e.g.

example (h : ∀ x : ℕ, x = x) : true :=
begin
  change ∀ y, _ at h,

end

[Horatiu Cheval]

Oh, right, I get it. I was confused reading in the documentations of change that it needs two definitionally equal terms while I had no term x so that I may have something defeq to it. It didn't occur to me that I could see the whole hypothesis as a term defeq to the one I wanted. Thanks!