| [[change-tactic\|change]] *new_goal_equivalent* | If the goal is `⊢ P`, and if `P` and `P_equivalent` are [definitionally equal](https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#definitional-equality),<br>then **change** `P_equivalent` will change the goal to `P_equivalent`.<br> | | | ----------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --- | Also, a hypothesis type can be changed, up to [definitionally equality](https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#definitional-equality), using the [[change-at-tactic|change-at]] syntax:  **change** `P_equivalentType` **at** `hP` changes `hP : P` to `hP : P_equivalentType`. ## See also **Cheatsheet:** [change — Formalising Mathematics 0.1 documentation](https://b-mehta.github.io/formalising-mathematics-notes/Part_2/tactics/change.html) --- **`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date:`** 2026-08-19