change

Summary

If your goal is ⊢ P, and if P and Q are definitionally equal, then change Q will change your goal to Q. You can use it on hypotheses too: change Q at h will change h : P to h : Q. Note: change can sometimes be omitted, as many tactics “see through” definitional equality.

Example

1. In Lean, ¬P is defined to mean P → false, so if your goal is ⊢ ¬P then change P → false will change it the goal to ⊢ P → false.

2. The rw tactic works up to syntactic equality, not definitional equality, so if your tactic state is

h : ¬P ↔ Q
⊢ P → false

then rw h doesn’t work, even though the left hand side of h is definitionally equal to the goal. However

change ¬P,
rw h

works, and changes the goal to Q.

3. change also works on hypotheses: if you have a hypothesis h : ¬P then change P → false at h will change h to h : P → false.

Details

Definitionally equal propositions are logically equivalent (indeed, they are equal!) so Lean allows you to change a goal P to a definitionally equal goal Q, because P is true if and only if Q is true.

Further notes

Many tactics work up to definitional equality, so sometimes change is not necessary. For example if your goal is ⊢ ¬P then intro h works fine anyway, as intro works up to definitional equality.

show does the same thing as change on the goal, but it doesn’t work on hypotheses.