Show equality of structures by fields

Stream: new members

[Jesse Slater]

I have a structure

structure SystemState where
  evenCount : Nat
  oddCount : Nat
deriving Repr

and I have defined

def emptyState : SystemState
  := {evenCount := 0, oddCount := 0}

I am writing a proof where I have a SystemState S, and have that S.evenCount = 0 and S.oddCount = 0. How do I show that S = emptyState?

[Kevin Buzzard]

Do cases on S and on emptyState, and then it should reduce to what you know. I don't know whether @[ext] has been ported to mathlib4 yet, but in Lean 3 + mathlib you could tag structures with @[ext] and then you could also use the ext tactic to reduce a goal S = emptyState to precisely what you have.

[Jesse Slater]

Thanks, ext seems to work