fix: apply ... at with field notation (#8911)

add a test to make sure `apply h.mp at` can be parsed and fix it.
leanprover-community · Dec 8, 2023 · cf68d15 · cf68d15
1 parent d76f152
commit cf68d15
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/Mathlib/Tactic/ApplyAt.lean b/Mathlib/Tactic/ApplyAt.lean
@@ -24,7 +24,7 @@ then replace the type of `i` with `αᵢ₊₁ → ⋯ → αₙ` by applying th
 original `i`.
 -/
 elab "apply" t:term "at" i:ident : tactic => withMainContext do
-  let f ← Term.elabTerm (← `(@$t)) none
+  let f ← elabTermForApply t
   let some ldecl := (← getLCtx).findFromUserName? i.getId
     | throwErrorAt i m!"Identifier {i} not found"
   let (mvs, bis, tp) ← forallMetaTelescopeReducingUntilDefEq (← inferType f) ldecl.type

diff --git a/test/ApplyAt.lean b/test/ApplyAt.lean
@@ -90,3 +90,9 @@ example {α β : Type*} (a : α) (b : β) : α × β := by
 example {α β : Type*} (a : α) (b : β) : α × β := by
   fail_if_success apply a at b
   exact (a, b)
+
+-- testing field notation
+example {A B : Prop} (h : A ↔ B) : A → B := by
+  intro hA
+  apply h.mp at hA
+  assumption