mathlib3 documentation

tactic.swap_var

Swap bound variable tactic #

This files defines a tactic swap_var whose main purpose is to be a weaker version of wlog that juggles bound names.

It is a helper around the core tactic rename.

example (P Q : Prop) (hp : P) (hq : Q) : P  Q :=
begin
  split,
  work_on_goal 1 { swap_var [P Q] },
  all_goals { exact P }
end

See also #

meta def tactic.interactive.swap_var (renames : interactive.parse swap_args_parser) :

swap_var [x y, P ↔ Q] swaps the names x and y, P and Q. Such a swapping can be used as a weak wlog if the tactic proofs use the same names.

example (P Q : Prop) (hp : P) (hq : Q) : P  Q :=
begin
  split,
  work_on_goal 1 { swap_var [P Q] },
  all_goals { exact P }
end

swap_var [x y, P ↔ Q] swaps the names x and y, P and Q. Such a swapping can be used as a weak wlog if the tactic proofs use the same names.

example (P Q : Prop) (hp : P) (hq : Q) : P  Q :=
begin
  split,
  work_on_goal 1 { swap_var [P Q] },
  all_goals { exact P }
end