`extract_goal` タクティクを紹介する

長い証明の途中で、ゴールを独立した定理に自動的にしてくれるタクティク。Zulip に投稿したいときとかに便利

    -- `x` と `m + n` はともに自然数なので、これは矛盾である。
    have : False := by
      replace left : x + 1 ≤ m + n := by
        norm_cast at left
      replace right : m + n ≤ x := by
        /-
        theorem extracted_1 (x m n : ℕ) (right : ↑m + ↑n < ↑x + 1) (left : x + 1 ≤ m + n) : m + n ≤ x := sorry
        -/
        extract_goal
        norm_cast at right
        omega
      omega
    contradiction

Start by locating the appropriate Japanese example or tactic-documentation page in the repository; this issue names no file or test. Use the supplied Lean snippet to explain what extract_goal does and when it is useful, then verify that the rendered documentation preserves the example and clearly introduces the tactic.