From 8a573b5d87a42bd19307522ee747aaed44d9d71c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 2 Dec 2022 10:04:01 -0800
Subject: [PATCH] fix: fixes #1900

---
 src/Lean/Elab/App.lean   | 6 ++++++
 tests/lean/run/1900.lean | 4 ++++
 2 files changed, 10 insertions(+)
 create mode 100644 tests/lean/run/1900.lean

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index f4f2306e97..3d93538354 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -682,6 +682,12 @@ end ElabAppArgs
 builtin_initialize elabAsElim : TagAttribute ←
   registerTagAttribute `elab_as_elim
     "instructs elaborator that the arguments of the function application should be elaborated as were an eliminator"
+    /-
+    We apply `elab_as_elim` after compilation because this kind of attribute is not applied to auxiliary declarations
+    created by the `WF` and `Structural` modules. This is an "indirect" fix for issue #1900. We should consider
+    having an explicit flag in attributes to indicate whether they should be copied to auxiliary declarations or not.
+    -/
+    (applicationTime := .afterCompilation)
     fun declName => do
       let go : MetaM Unit := do
         discard <| getElimInfo declName
diff --git a/tests/lean/run/1900.lean b/tests/lean/run/1900.lean
new file mode 100644
index 0000000000..8717912f23
--- /dev/null
+++ b/tests/lean/run/1900.lean
@@ -0,0 +1,4 @@
+@[elab_as_elim]
+def strongSubRecursion {P : Nat → Nat → Sort _} (H : ∀ a b, (∀ x y, x < a → y < b → P x y) → P a b) :
+    ∀ n m : Nat, P n m
+  | n, m => H n m fun x y _ _ => strongSubRecursion H x y