Rename bound variable tactic
This files defines a tactic rename_var whose main purpose is to teach
renaming of bound variables.
rename_var old newrenames all bound variables namedoldtonewin the goal.rename_var old new at hdoes the same in hypothesish.
example (P : ℕ → ℕ → Prop) (h : ∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m :=
begin
rename_var n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
rename_var m n, -- goal is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
Tags
teaching, tactic
rename_var old new renames all bound variables named old to new in the goal.
rename_var old new at h does the same in hypothesis h.