Documentation

Mathlib.Tactic.SwapVar

Defines the swap_var tactic #

Swap the names of two hypotheses.

The parser for swap rules

Equations
    Instances For

      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
        Instances For