Defines the swap_var tactic

Swap the names of two hypotheses.

def Mathlib.Tactic.swapRule : Lean.ParserDescr

The parser for swap rules

Equations

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

def Mathlib.Tactic.«tacticSwap_var__,,» : Lean.ParserDescr

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, 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⟩

Equations

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