Theorem: ThunkOrdering.lex_right_identity (Katydid/Std/ThunkOrdering.lean)

State before:
a : Thunk Ordering
⊢ lex a { fn := fun x => Ordering.eq } = a
Tactic:
unfold lex
State after:
a : Thunk Ordering
⊢ (match Thunk.get a with
    | Ordering.eq => { fn := fun x => Ordering.eq }
    | x => { fn := fun x => Thunk.get a }) =
    a

State before:
a : Thunk Ordering
⊢ (match Thunk.get a with
    | Ordering.eq => { fn := fun x => Ordering.eq }
    | x => { fn := fun x => Thunk.get a }) =
    a
Tactic:
cases h: a.get <;>
  simp only <;>
  rw [<-h] <;>
  rfl
State after:
no goals