show struct equality

Stream: general

[Leonard Wiechmann]

sorry, this seems super simple, but I can't figure out how to show struct (prod) equality.
surely it's just field-wise equality. split doesn't work.
how do I split the goal from a = b into a.fst = b.fst ∧ a.snd = b.snd?

[Alex J. Best]

Normally we just use an (autogenerated) lemma for this, e.g. docs#prod.ext_iff

[Alex J. Best]

(ok maybe its not autogenerated as often as I thought!)

[Leonard Wiechmann]

I suspected that it might be prod.ext, but got an unknown identifier error.
adding import data.prod fixed it :face_palm:🏻‍♀️ thanks!

[Floris van Doorn]

tactic#ext is also useful.

[Floris van Doorn]

link that works: https://leanprover-community.github.io/mathlib_docs/tactics.html#ext1%20/%20ext