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

State before:
⊢ ∀ (x : Ordering), lex x eq = x
Tactic:
intro x
State after:
x : Ordering
⊢ lex x eq = x

State before:
x : Ordering
⊢ lex x eq = x
Tactic:
cases x
State after:
case lt

⊢ lex lt eq = lt

case eq

⊢ lex eq eq = eq

case gt

⊢ lex gt eq = gt

State before:
case lt

⊢ lex lt eq = lt

case eq

⊢ lex eq eq = eq

case gt

⊢ lex gt eq = gt
Tactic:
{ rfl }
State after:
case eq

⊢ lex eq eq = eq

case gt

⊢ lex gt eq = gt

State before:
case eq

⊢ lex eq eq = eq

case gt

⊢ lex gt eq = gt
Tactic:
{ rfl }
State after:
case gt

⊢ lex gt eq = gt

State before:
case gt

⊢ lex gt eq = gt
Tactic:
{ rfl }
State after:
no goals

State before:
case lt

⊢ lex lt eq = lt
Tactic:
rfl
State after:
no goals

State before:
case eq

⊢ lex eq eq = eq
Tactic:
rfl
State after:
no goals

State before:
case gt

⊢ lex gt eq = gt
Tactic:
rfl
State after:
no goals