diff --git a/tests/lean/interactive/proof_state_info3.input b/tests/lean/interactive/proof_state_info3.input
new file mode 100644
index 0000000000..b4af4f92df
--- /dev/null
+++ b/tests/lean/interactive/proof_state_info3.input
@@ -0,0 +1,19 @@
+VISIT proof_state_info3.lean
+SYNC 11
+
+
+theorem tst (a b c : Prop) : a → b → a ∧ b :=
+begin
+  info,
+  intros (Ha, Hb),
+  info,
+  apply and.intro,
+  apply Ha,
+  apply Hb,
+end
+WAIT
+REPLACE 7
+  state,
+SHOW
+WAIT
+INFO 8 17
\ No newline at end of file
diff --git a/tests/lean/interactive/proof_state_info3.input.expected.out b/tests/lean/interactive/proof_state_info3.input.expected.out
new file mode 100644
index 0000000000..07524c2c65
--- /dev/null
+++ b/tests/lean/interactive/proof_state_info3.input.expected.out
@@ -0,0 +1,30 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINSHOW
+
+
+theorem tst (a b c : Prop) : a → b → a ∧ b :=
+begin
+  info,
+  intros (Ha, Hb),
+  state,
+  apply and.intro,
+  apply Ha,
+  apply Hb,
+end
+-- ENDSHOW
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- PROOF_STATE|8|17
+a b c : Prop,
+Ha : a,
+Hb : b
+⊢ a
+--
+a b c : Prop,
+Ha : a,
+Hb : b
+⊢ b
+-- ACK
+-- ENDINFO