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
State after:
case lt
b c : Ordering
⊢ lex (lex lt b) c = lex lt (lex b c)

case eq
b c : Ordering
⊢ lex (lex eq b) c = lex eq (lex b c)

case gt
b c : Ordering
⊢ lex (lex gt b) c = lex gt (lex b c)

State before:
case lt
b c : Ordering
⊢ lex (lex lt b) c = lex lt (lex b c)

case eq
b c : Ordering
⊢ lex (lex eq b) c = lex eq (lex b c)

case gt
b c : Ordering
⊢ lex (lex gt b) c = lex gt (lex b c)
Tactic:
{
  case lt => rfl
}
State after:
case eq
b c : Ordering
⊢ lex (lex eq b) c = lex eq (lex b c)

case gt
b c : Ordering
⊢ lex (lex gt b) c = lex gt (lex b c)

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

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

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

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

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

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