From ef33882e2fad6c90e4b2cc8aa22123b656ca4fd8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 6 Mar 2024 13:19:53 -0800
Subject: [PATCH] test: issue #2835

closes #2835
---
 tests/lean/run/2835.lean | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 tests/lean/run/2835.lean

diff --git a/tests/lean/run/2835.lean b/tests/lean/run/2835.lean
new file mode 100644
index 0000000000..9b55245c54
--- /dev/null
+++ b/tests/lean/run/2835.lean
@@ -0,0 +1,6 @@
+@[simp] theorem imp_self' {a : Prop} : (a → a) ↔ True := ⟨fun _ => trivial, fun _ => id⟩
+
+example {P : Prop} : P → P := by simp only [imp_self']
+
+example {α : Prop} {P : α → Prop} {f : ∀ {a}, P a → α} {a : α} : (h : P a) → P (f h) := by
+  simp only [imp_self']