diff --git a/tests/lean/lean3RefineBug.lean b/tests/lean/lean3RefineBug.lean
new file mode 100644
index 0000000000..3b4452f4af
--- /dev/null
+++ b/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
diff --git a/tests/lean/lean3RefineBug.lean.expected.out b/tests/lean/lean3RefineBug.lean.expected.out
new file mode 100644
index 0000000000..f5d310438d
--- /dev/null
+++ b/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