Show two structs are equal when all fields are equal

Stream: new members

[Fingy Soupy]

I have two structs and I'd like to show that they are equal if all their fields are equal. I thought no_confusion might come into play here but I can't figure out how to use it.

structure thing :=
(a : nat)
(b : nat)

lemma things_eq (x y : thing) (q : x.a = y.a) (q2 : x.b = y.b) : x = y := begin
  sorry
end

[Eric Wieser]

cases x, cases y makes progress

[Eric Wieser]

Better yet, add @[ext] to the structure

[Eric Wieser]

Which generates precisely your lemma

[Fingy Soupy]

Thanks! :)