Prove return value of functon

Stream: lean4

[Jesse Slater]

I am having trouble finishing this proof. What can I do to replace the sorry?

structure SystemState where
  evenCount : Nat
  oddCount : Nat
deriving Repr

def bar (S : SystemState) := S

def foo (S: SystemState): Option SystemState :=
  if S.oddCount ≥ 2 then Option.some (bar S)
  else Option.none

variable (x : SystemState)

variable (ge2 : x.oddCount ≥ 2)

theorem t : foo x = Option.some (bar x) :=
  by sorry

I have simplified it to retain only the relevant parts. This is part of a larger proof, where bar does something, and where I get x and ge2 from assumptions

[František Silváši 🦉]

To be as explicit as possible, one can first inspect the definition of foo and apply a lemma (if_pos) stating that if the boolean test is true, then we get the first branch. As such:

theorem t : foo x = Option.some (bar x) := by
  unfold foo
  rw [if_pos ge2]

[František Silváši 🦉]

Normally for proofs that have an obvious series of rewrites to reach the goal, you'll see something like by simp [foo, *].

[Jesse Slater]

Thank you!