# Documentation

Mathlib.Tactic.SwapVar

# Defines the swap_var tactic #

Swap the names of two hypotheses.

The parser for swap rules

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

swap_var swap_rule₁, swap_rule₂, ⋯⋯ applies swap_rule₁ then swap_rule₂ then ⋯⋯.

A swap_rule is of the form x y or x ↔ y↔ y, and "applying it" means swapping the variable name x by y and vice-versa on all hypotheses and the goal.

example {P Q : Prop} (q : P) (p : Q) : P ∧ Q := by
swap_var p ↔ q
exact ⟨p, q⟩
∧ Q := by
swap_var p ↔ q
exact ⟨p, q⟩
↔ q
exact ⟨p, q⟩

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