Merge pull request #1048 from lean-ja/Seasawher/issue1047

`sorry` の舞台裏を説明する

LeanByExample/Reference/Tactic/Sorry.lean

@@ -1,6 +1,7 @@
 /- # sorry
 
 証明の細部を埋める前にコンパイルが通るようにしたいとき、証明で埋めるべき箇所に `sorry` と書くとコンパイルが通るようになります。ただし、`sorry` を使用しているという旨の警告が出ます。 -/
+import Lean --#
 
 -- Fermat の最終定理
 def FermatLastTheorem :=
@@ -9,3 +10,17 @@ def FermatLastTheorem :=
 #guard_msgs (drop warning) in --#
 theorem flt : FermatLastTheorem :=
   sorry
+
+/- ## 舞台裏
+`Lean.Elab.admitGoal` を使用することで `sorry` と同様のタクティクを作ることができます。
+-/
+
+open Lean Elab Tactic
+
+elab "my_sorry" : tactic => withMainContext do
+  let goal ← getMainGoal
+  admitGoal goal
+
+#guard_msgs (drop warning) in --#
+theorem flt' : FermatLastTheorem := by
+  my_sorry