`Membership.mem` does not work in `calc` unless the calc lines are swapped

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

This occurred after #5020. The arguments of Membership.mem was swapped there, but calc has not adapted to this change, so expected proofs do not work.

Context

The discussion on the Lean Zulip.

Steps to Reproduce

Consider the following code:

example {G : Type} {P : Type} [Membership G P] (H : P) (a b : G)
    (h₁ : a = b) (h₂ : a ∈ H) : b ∈ H :=
  calc
    b = a := h₁.symm
    _ ∈ H := h₂

Expected behavior:

The proof works.

Actual behavior:

We get an error at the line _ ∈ H := h₂ with the following message:

invalid 'calc' step, left-hand-side is
  H : P
previous right-hand-side is
  a : G

Instead of the above proof, a proof with the swapped calc lines works:

/- Valid proof -/
example {G : Type} {P : Type} [Membership G P] (H : P) (a b : G)
    (h₁ : a = b) (h₂ : a ∈ H) : b ∈ H :=
  calc
    a ∈ H := h₂
    a = b := h₁

Versions

"4.15.0-nightly-2024-11-11"
(live.lean-lang.org.)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal reproducer in the issue and inspect the calc elaboration handling of Membership.mem, alongside the argument change from #5020. The fix is complete when the original calc proof typechecks without swapping its lines, while the existing swapped form continues to work.