Documentation

Mathlib.Tactic.RenameBVar

The rename_bvar tactic #

This file defines the rename_bvar tactic, for renaming bound variables.

Renames a bound variable in a hypothesis.

Equations
    Instances For

      Renames a bound variable in the target.

      Equations
        Instances For
          • 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 := by
            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
          

          Note: name clashes are resolved automatically.

          Equations
            Instances For