conv left vs right puzzle

Stream: mathlib4

[Damiano Testa]

Dear All,

here is a puzzle, in the tradition of the Friday afternoon.

import Mathlib.Tactic.Conv

variable (a b : Nat) (h : a = b)

example : a ∈ [a] := by
  -- Which of the two `a` changes to `b`?
  conv_lhs => rw [h]
  sorry

[Matthew Ballard]

With or without set_option backward.isDefEq.respectTransparency false?

[Aaron Liu]

is it

my answer

the one in [a] because Membership.mem has its arguments reversed