diff --git a/tests/lean/run/do_match_else.lean b/tests/lean/run/do_match_else.lean
index f1a440b20e..0a7a99b20e 100644
--- a/tests/lean/run/do_match_else.lean
+++ b/tests/lean/run/do_match_else.lean
@@ -5,11 +5,25 @@ set_option pp.all true
 example (a b c x y : nat) (H : nat.add (nat.add x y) y = 0) : true :=
 by do
   a ← get_local "a", b ← get_local "b", c ← get_local "c",
+  H ← get_local "H" >>= infer_type,
+  (lhs, rhs) ← match_eq H,
   nat_add : expr ← mk_const ("nat" <.> "add"),
   p : pattern    ← mk_pattern [] [a, b] (nat_add a b) [nat_add b a, a, b],
   trace (pattern.output p),
-  H ← get_local "H" >>= infer_type,
-  lhs_rhs ← match_eq H,
-  [v₁, v₂, v₃] ← match_pattern p (prod.pr1 lhs_rhs) | failed,
-  trace v₁,
+  [v₁, v₂, v₃] ← match_pattern p lhs | failed,
+  trace v₁, trace v₂, trace v₃,
+  constructor
+
+print "------------------"
+
+example (f : nat → nat) (a b c x y : nat) (H : nat.add (nat.add (f (f x)) y) y = 0) : true :=
+by do
+  a ← get_local "a", b ← get_local "b", c ← get_local "c",
+  H ← get_local "H" >>= infer_type,
+  (lhs, rhs) ← match_eq H,
+  nat_add : expr ← mk_const ("nat" <.> "add"),
+  p : pattern    ← mk_pattern [] [a, b] (nat_add (nat_add a b) b) [nat_add (nat_add b b) (nat_add a a b), a, b],
+  trace (pattern.output p),
+  [v₁, v₂, v₃] ← match_pattern p lhs | failed,
+  trace v₁, trace v₂, trace v₃,
   constructor