TFAE.out in rw

Stream: mathlib4

[Adam Topaz]

Here's a MWE:

import Mathlib.Data.List.TFAE

example (p q : Prop) (h : [p, q].TFAE) (hp : p) : q := by
  rw [h.out 0 1] at h

example (p q : Prop) (h : [p, q].TFAE) (hp : p) : q := by
  have := h.out 0 1
  rw [this] at h

The first example gives an error at the rewrite:

tactic 'rewrite' failed, pattern is a metavariable
  ?m.53
from equation
  ?m.53 = ?m.54

Is this expected?

[Adam Topaz]

The second example works as expected.