What does "unexpected syntax" mean?

Stream: mathlib4

[Arien Malec]

I have the line in a proof in mathlib4#1464

change (TProd.mk l f ∈ Set.TProd l t ↔ ∀ i : ι, i ∈ l → f i ∈ t i) at h

which gives unexpected syntax & I'm not exactly sure what that's supposed to mean?

[Kevin Buzzard]

What happens if you try let foo := TProd.mk l f...t i? Does that typecheck?

[Arien Malec]

First thing I tried & same issue :smiling_face_with_tear:

[Kyle Miller]

Does change _ at _ syntax exist yet?

[Kyle Miller]

The only change ... at ... in mathlib4 I've seen is in a porting note.

[Kyle Miller]

Here's a workaround. Change your have to

    have h : TProd.mk l f ∈ Set.TProd l t ↔ ∀ i : ι, i ∈ l → f i ∈ t i := by
      change f ∈ TProd.mk l ⁻¹' Set.TProd l t ↔ f ∈ { x | x ∈ l }.pi t
      rw [mk_preimage_tprod l t]