try?の説明を丁寧にする

Author: Seasawher

LeanByExample/Tactic/TryQuestion.lean

@@ -17,7 +17,15 @@ example (as : List α) : (reverse as).head? = as.last? := by
   -- grind 単体では証明ができない
   fail_if_success grind
 
+  -- 帰納法を適当に使ってみてもダメ
+  fail_if_success induction as with grind
+  fail_if_success fun_induction last? <;> grind
+
   -- try? なら証明を見つけることができる
   try?
 
+example (as : List α) : (reverse as).head? = as.last? := by
+  -- 証明の一例
+  fun_induction last? <;> grind [= last?.eq_def]
+
 end List