Sometimes in a proof it is useful to introduce a new variable to stand for some object that you want to talk about. To do this, select the gap in which you want to introduce the new variable (or select any given or goal in that gap) and give the Define command. A dialog box will open, asking you to fill in the blanks in the statement “Let ___ = ___”. Fill in the first blank with the new variable you want to introduce, and fill in the second blank with an expression naming the object you want the new variable to stand for. The variable you put in the first blank must not already be in use in the proof to stand for something else.
This command is especially useful when your goal has the form “x = ?”. If you select a goal of this form and give the Define command, then the first blank will already be filled in with the variable that needs to be defined (although you can change it to a different one if you want to). Defining this variable will achieve the goal, so if you define this variable then the gap will disappear and be replaced by the definition of the variable. Double clicking on a goal of the form “x = ?” is a shortcut for selecting the goal and giving the Define command.