Improve introduction of tactics

IntroLean.qmd

@@ -211,7 +211,7 @@ No goals
 
 Congratulations!  You've written your first proof in tactic mode.  If you move your cursor around in the proof, you will see that Lean always displays in the Infoview the tactic state at the point in the proof where the cursor is located.  Try clicking on different lines of the proof to see how the tactic state changes over the course of the proof.  If you want to try another example, you could try typing in the first example in this chapter.  You will learn the most from this book if you continue to type the examples into Lean and see for yourself how the tactic state gets updated as the proof is written.
 
-We have now seen four tactics: `contrapos`, `assume`, `have`, and `show`.  If the goal is a conditional statement, the `contrapos` tactic replaces it with its contrapositive.  If `h` is a given that is a conditional statement, then `contrapos at h` will replace `h` with its contrapositive.  If the goal is a conditional statement `P → Q`, you can use the `assume` tactic to assume the antecedent `P`, and Lean will set the goal to be the consequent `Q`.  You can use the `have` tactic to make an inference from your givens, as long as you can justify the inference with a proof.  The `show` tactic is similar, but it is used to infer the goal, thus completing the proof.  And we have learned how to use one rule of inference in term mode: modus ponens.  In the rest of this book we will learn about other tactics and other term-mode rules.
+In each step of a tactic-mode proof, we invoke a *tactic*.  In the proofs above, we have used four tactics: `contrapos`, `assume`, `have`, and `show`.  If the goal is a conditional statement, the `contrapos` tactic replaces it with its contrapositive.  If `h` is a given that is a conditional statement, then `contrapos at h` will replace `h` with its contrapositive.  If the goal is a conditional statement `P → Q`, you can use the `assume` tactic to assume the antecedent `P`, and Lean will set the goal to be the consequent `Q`.  You can use the `have` tactic to make an inference from your givens, as long as you can justify the inference with a proof.  The `show` tactic is similar, but it is used to infer the goal, thus completing the proof.  And we have learned how to use one rule of inference in term mode: modus ponens.  In the rest of this book we will learn about other tactics and other term-mode rules.
 
 Before continuing, it might be useful to summarize how you type statements into Lean.  We have already told you how to type the symbols `→` and `¬`, but you will want to know how to type all of the logical connectives.  In each case, the command to produce the symbol must be followed by space or tab, but there is also a plain text alternative:
 

docs/IntroLean.html

@@ -391,7 +391,7 @@ <h2 class="anchored" data-anchor-id="tactic-mode">Tactic Mode</h2>
 </div>
 </div>
 <p>Congratulations! You’ve written your first proof in tactic mode. If you move your cursor around in the proof, you will see that Lean always displays in the Infoview the tactic state at the point in the proof where the cursor is located. Try clicking on different lines of the proof to see how the tactic state changes over the course of the proof. If you want to try another example, you could try typing in the first example in this chapter. You will learn the most from this book if you continue to type the examples into Lean and see for yourself how the tactic state gets updated as the proof is written.</p>
-<p>We have now seen four tactics: <code>contrapos</code>, <code>assume</code>, <code>have</code>, and <code>show</code>. If the goal is a conditional statement, the <code>contrapos</code> tactic replaces it with its contrapositive. If <code>h</code> is a given that is a conditional statement, then <code>contrapos at h</code> will replace <code>h</code> with its contrapositive. If the goal is a conditional statement <code>P → Q</code>, you can use the <code>assume</code> tactic to assume the antecedent <code>P</code>, and Lean will set the goal to be the consequent <code>Q</code>. You can use the <code>have</code> tactic to make an inference from your givens, as long as you can justify the inference with a proof. The <code>show</code> tactic is similar, but it is used to infer the goal, thus completing the proof. And we have learned how to use one rule of inference in term mode: modus ponens. In the rest of this book we will learn about other tactics and other term-mode rules.</p>
+<p>In each step of a tactic-mode proof, we invoke a <em>tactic</em>. In the proofs above, we have used four tactics: <code>contrapos</code>, <code>assume</code>, <code>have</code>, and <code>show</code>. If the goal is a conditional statement, the <code>contrapos</code> tactic replaces it with its contrapositive. If <code>h</code> is a given that is a conditional statement, then <code>contrapos at h</code> will replace <code>h</code> with its contrapositive. If the goal is a conditional statement <code>P → Q</code>, you can use the <code>assume</code> tactic to assume the antecedent <code>P</code>, and Lean will set the goal to be the consequent <code>Q</code>. You can use the <code>have</code> tactic to make an inference from your givens, as long as you can justify the inference with a proof. The <code>show</code> tactic is similar, but it is used to infer the goal, thus completing the proof. And we have learned how to use one rule of inference in term mode: modus ponens. In the rest of this book we will learn about other tactics and other term-mode rules.</p>
 <p>Before continuing, it might be useful to summarize how you type statements into Lean. We have already told you how to type the symbols <code>→</code> and <code>¬</code>, but you will want to know how to type all of the logical connectives. In each case, the command to produce the symbol must be followed by space or tab, but there is also a plain text alternative:</p>
 <div style="margin: 0% 10%">
 <table class="table">