using structural ext when there is a non-structural ext defi

Stream: new members

[llllvvuu]

Given a b : Array α, I want to transform the goal a = b into a.data = b.data, but docs#Array.ext and docs#Array.ext_iff mean a different thing. Is there a way to do this rewrite, without having to define something like the following?

theorem Array.eq_iff_data_eq {α} {a b : Array α} : a = b ↔ a.data = b.data := by
  cases a; cases b; simp

[Etienne Marion]

You can rewrite with Array.mk.injEq (which is what is used in your code when you write simp?).