Suggest obtain for proof by cases

Appendix.qmd

@@ -67,7 +67,7 @@ We have mostly used these tactics to reexpress negative statements as more usefu
 
 * #### `by_cases on`
 
-If you have `h : P ∨ Q`, then you can break your proof into cases by using the tactic `cases' h with hP hQ`.  In case 1, `h : P ∨ Q` will be replaced by `hP : P`, and in case 2 it will be replaced by `hQ : Q`.  In both cases, you have to prove the original goal.  You may also want to learn about the tactics `cases` and `rcases`.
+If you have `h : P ∨ Q`, then you can break your proof into cases by using the tactic `obtain hP | hQ := h`.  In case 1, `h : P ∨ Q` will be replaced by `hP : P`, and in case 2 it will be replaced by `hQ : Q`.  In both cases, you have to prove the original goal.  You may also want to learn about the tactics `cases` and `rcases`.
 
 * #### `by_induc`, `by_strong_induc`
 
@@ -136,7 +136,7 @@ If your goal is `∃! (x : U), P x` and you think that `a` is the unique value o
 
 * #### `obtain`
 
-There is an `obtain` tactic in standard Lean, but it is slightly different from the one used in this book.  If you have `h : ∃ (x : U), P x`, then the tactic `obtain ⟨u, h1⟩ := h` will introduce both `u : U` and `h1 : P u` into the tactic state.  Note that `u` and `h1` must be enclosed in angle brackets, `⟨ ⟩`.  To enter those brackets, type `\<` and `\>`.
+If you have `h : ∃ (x : U), P x`, then the tactic `obtain ⟨u, h1⟩ := h` will introduce both `u : U` and `h1 : P u` into the tactic state.  Note that `u` and `h1` must be enclosed in angle brackets, `⟨ ⟩`.  To enter those brackets, type `\<` and `\>`.
 
 If you have `h : ∃! (x : U), P x`, then `obtain ⟨u, h1, h2⟩ := h` will also introduce `u : U` and `h1 : P u` into the tactic state.  In addition, it will introduce `h2` as an identifier for a statement that is equivalent to `∀ (y : U), P y → y = u`.  (Unfortunately, the statement introduced is more complicated.)
 

docs/Appendix.html

@@ -428,7 +428,7 @@ <h2 class="anchored" data-anchor-id="transitioning-to-standard-lean">Transitioni
 <ul>
 <li><h4 id="by_cases-on" class="anchored"><code>by_cases on</code></h4></li>
 </ul>
-<p>If you have <code>h : P ∨ Q</code>, then you can break your proof into cases by using the tactic <code>cases' h with hP hQ</code>. In case 1, <code>h : P ∨ Q</code> will be replaced by <code>hP : P</code>, and in case 2 it will be replaced by <code>hQ : Q</code>. In both cases, you have to prove the original goal. You may also want to learn about the tactics <code>cases</code> and <code>rcases</code>.</p>
+<p>If you have <code>h : P ∨ Q</code>, then you can break your proof into cases by using the tactic <code>obtain hP | hQ := h</code>. In case 1, <code>h : P ∨ Q</code> will be replaced by <code>hP : P</code>, and in case 2 it will be replaced by <code>hQ : Q</code>. In both cases, you have to prove the original goal. You may also want to learn about the tactics <code>cases</code> and <code>rcases</code>.</p>
 <ul>
 <li><h4 id="by_induc-by_strong_induc" class="anchored"><code>by_induc</code>, <code>by_strong_induc</code></h4></li>
 </ul>
@@ -480,7 +480,7 @@ <h2 class="anchored" data-anchor-id="transitioning-to-standard-lean">Transitioni
 <ul>
 <li><h4 id="obtain" class="anchored"><code>obtain</code></h4></li>
 </ul>
-<p>There is an <code>obtain</code> tactic in standard Lean, but it is slightly different from the one used in this book. If you have <code>h : ∃ (x : U), P x</code>, then the tactic <code>obtain ⟨u, h1⟩ := h</code> will introduce both <code>u : U</code> and <code>h1 : P u</code> into the tactic state. Note that <code>u</code> and <code>h1</code> must be enclosed in angle brackets, <code>⟨ ⟩</code>. To enter those brackets, type <code>\&lt;</code> and <code>\&gt;</code>.</p>
+<p>If you have <code>h : ∃ (x : U), P x</code>, then the tactic <code>obtain ⟨u, h1⟩ := h</code> will introduce both <code>u : U</code> and <code>h1 : P u</code> into the tactic state. Note that <code>u</code> and <code>h1</code> must be enclosed in angle brackets, <code>⟨ ⟩</code>. To enter those brackets, type <code>\&lt;</code> and <code>\&gt;</code>.</p>
 <p>If you have <code>h : ∃! (x : U), P x</code>, then <code>obtain ⟨u, h1, h2⟩ := h</code> will also introduce <code>u : U</code> and <code>h1 : P u</code> into the tactic state. In addition, it will introduce <code>h2</code> as an identifier for a statement that is equivalent to <code>∀ (y : U), P y → y = u</code>. (Unfortunately, the statement introduced is more complicated.)</p>
 <p>You may also find the theorems <code>ExistsUnique.exists</code> and <code>ExistsUnique.unique</code> useful:</p>
 <div class="ind">