syntax: why doesn't `.mp` work here?

Stream: new members

[rzeta0]

The following program works fine.

import Mathlib.Tactic

example {P Q : Prop} (h1 : P ↔ ¬ Q) (h2 : Q) : ¬ P := by
  intro h
  obtain ⟨ g1, g2 ⟩ := h1
  apply g1 at h
  contradiction

but if I try to shorten it and try to use h1.mp it doesn't

import Mathlib.Tactic

example {P Q : Prop} (h1 : P ↔ ¬ Q) (h2 : Q) : ¬ P := by
  intro h
  apply h1.mp at h
  contradiction

I don't understand as I thought .mp added to a bidirectional proposition selected the forward direction.

---

UPDATE: The second example actually works on live.lean-lang.org but not in the MoP environment.

So that means this question will not be of general interest, but if anyone does want to offer insights, I'd be grateful.

The error in the MoP environment is :

invalid use of field notation with `@` modifier

[Kyle Miller]

This sounds like a bug in apply at. Try apply (h1.mp) at h, or try have h1' := h1.mp followed by apply h1' at h.

[rzeta0]

interesting that apply (h1.mp) at h works.

must be a bug in an older version of Lean that MoP uses.

[Kyle Miller]

I'll spare you the details, but I'm pretty sure it's a bug in apply at that still exists, but there was a new feature added to Lean that helps obscure it (and accidentally help it do the right thing anyway!)