equivalence of records based on fields

Stream: lean4

[Bhakti Shah]

mainly working off of this and this but I can't seem to find the right tactic for just going from equality of records to equality of their fields. I'm sure this is super obvious and written up somewhere (which, by the way, if you have a link would be super helpful) but how do i transform a part of my goal from
{ a := x } != { a:= y } to x != y? Specifically I want some form of a rewrite and not an entire application. I tried rw [congr] and congr but the former rightfully yells at me for trying to rewrite using a mv and the latter just doesn't make progress. i also tried congr' 1but that says congr' isn't recognized, and i think i saw it in the mathlib3 docs but not mathlib 4 so that makes sense, i just don't know what the right tactic is and none of the congruence ones listed on the page i linked seem like they'd work.
Thank you!

[Mario Carneiro]

if the structure has the @[ext] attribute, then rw [T.ext_iff] should work

[Bhakti Shah]

is there a way to reflect this to boolean equality? i guess i could just coerce my lemma into propositional inequality instead of boolean; that might be easier