test: add test for Lean 3 refine bug reported on Zulip

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60refine.60.20bug.20.3F/near/278031110

tests/lean/lean3RefineBug.lean

@@ -0,0 +1,28 @@
+example (p q : Prop) : p ∧ q → p := by
+  refine fun ⟨a, b⟩ => a
+
+example (p q : Prop) : p ∧ q → p := by
+  refine fun a => ?hp
+  trace_state
+  exact a.1
+
+example (p q : Prop) : p ∧ q → p := by
+  refine fun ⟨a, b⟩ => a
+
+example (p q : Prop) : p ∧ q → p := by
+  refine fun ⟨a, b⟩ => ?hp
+  trace_state
+  exact a
+
+example (p q : Prop) : p ∧ q → p := by
+  refine fun a => ?hp
+  case hp => exact a.1
+
+example (p q : Prop) : p ∧ q → p := by
+  refine fun ⟨a, b⟩ => ?hp
+  case hp => exact a
+
+example (p q : Prop) : p ∧ q → p := by
+  refine λ ⟨a, b⟩ => ?hp
+  trace_state
+  exact a

tests/lean/lean3RefineBug.lean.expected.out

@@ -0,0 +1,16 @@
+case hp
+p q : Prop
+a : p ∧ q
+⊢ p
+case hp
+p q : Prop
+ : p ∧ q
+a : p
+b : q
+⊢ p
+case hp
+p q : Prop
+ : p ∧ q
+a : p
+b : q
+⊢ p