| [[change-at-tactic\|change]] *new__equivalent_type* at *hypothesis_type* | If a hypothesis has type `P`, and <br>if `P` and `P_equivalentType` are [definitionally equal](https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#definitional-equality),<br>then **change** `P_equivalentType` **at** `hP` <br>changes `hP : P` to `hP : P_equivalentType`. <br> | | ------------------------------------------------------------------------ | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | Also, the goal type can be changed, up to [definitionally equality](https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#definitional-equality), with the [[change-tactic|change]] syntax:  **change** `P_equivalentType` changes `⊢ P` to `⊢  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