Theorem: Ordering.lex_assoc'' (Katydid/Std/Ordering.lean)

State before:
a b c : Ordering
⊢ lex (lex a b) c = lex a (lex b c)
Tactic:
cases a with
| eq => rfl
| lt => rfl
| gt => rfl
State after:
no goals

State before:
case eq
b c : Ordering
⊢ lex (lex eq b) c = lex eq (lex b c)
Tactic:
rfl
State after:
no goals

State before:
case lt
b c : Ordering
⊢ lex (lex lt b) c = lex lt (lex b c)
Tactic:
rfl
State after:
no goals

State before:
case gt
b c : Ordering
⊢ lex (lex gt b) c = lex gt (lex b c)
Tactic:
rfl
State after:
no goals