def
Mathlib.Tactic.renameBVarHyp
(mvarId : Lean.MVarId)
(fvarId : Lean.FVarId)
(old : Lean.Name)
(new : Lean.Name)
:

Renames a bound variable in a hypothesis.

## Equations

- One or more equations did not get rendered due to their size.

Renames a bound variable in the target.

## Equations

- Mathlib.Tactic.renameBVarTarget mvarId old new = Mathlib.Tactic.modifyTarget mvarId fun e => Lean.Expr.renameBVar e old new

`rename_bvar old new`

renames all bound variables named`old`

to`new`

in the target.`rename_bvar old new at h`

does the same in hypothesis`h`

.

```
example (P : ℕ → ℕ → Prop) (h : ∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m :=
begin
rename_bvar n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
rename_bvar m n, -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
→ ℕ → Prop) (h : ∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m :=
begin
rename_bvar n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
rename_bvar m n, -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
→ Prop) (h : ∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m :=
begin
rename_bvar n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
rename_bvar m n, -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m :=
begin
rename_bvar n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
rename_bvar m n, -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
∃ m, P n m) : ∀ l, ∃ m, P l m :=
begin
rename_bvar n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
rename_bvar m n, -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
∀ l, ∃ m, P l m :=
begin
rename_bvar n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
rename_bvar m n, -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
∃ m, P l m :=
begin
rename_bvar n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
rename_bvar m n, -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
∀ (q : ℕ), ∃ (m : ℕ), P q m,
rename_bvar m n, -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
∃ (m : ℕ), P q m,
rename_bvar m n, -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
∀ (l : ℕ), ∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
∃ (n : ℕ), P k n,
exact h -- Lean does not care about those bound variable names
end
```

Note: name clashes are resolved automatically.

## Equations

- One or more equations did not get rendered due to their size.