Render the code snippet working

Author: YaelDillies

posts/how-to-write-a-simproc.md

@@ -336,7 +336,9 @@ Often, when applying a theorem, we may need to provide additional proof terms fo
 In the following example, we implement a simproc that simplifies expressions of the form `(a * b).factorization ` to `a.factorization + b.factorization` whenever a proof that `a` and `b` are both non-zero can be found by the discharger.
 
 ```lean
-open Qq
+import Mathlib
+
+open Qq Lean.Meta.Simp
 
 simproc_decl factorizationMul (Nat.factorization (_ * _)) := fun e => do
   let ⟨1, ~q(ℕ →₀ ℕ), ~q(Nat.factorization ($a * $b))⟩ ← inferTypeQ e | return .continue
@@ -353,14 +355,10 @@ simproc_decl factorizationMul (Nat.factorization (_ * _)) := fun e => do
   return .visit { expr := e', proof? := pf }
 
 set_option trace.Meta.Tactic.simp true in
-example : Nat.factorization (2 * 3) = Nat.factorization 2 + Nat.factorization 3 := by
-  /-
-  [Meta.Tactic.simp.rewrite] eq_self:1000:
-      Nat.factorization 2 + Nat.factorization 3 = Nat.factorization 2 + Nat.factorization 3
-    ==>
-      True
-  -/
+example : Nat.factorization (2 * 3) = fun₀ | 2 => 1 | 3 => 1 := by
   simp (disch := decide) only [factorizationMul]
+  guard_target = Nat.factorization 2 + Nat.factorization 3 = fun₀ | 2 => 1 | 3 => 1
+  sorry
 ```
 
 <span style="color:red">**TODO(Paul)**</span>