Theorem: Ordering.eq_opp_iff_opp_eq (GMLInit/Data/Basic.lean)

State before:
x y : Ordering
⊢ x.opp = y ↔ x = y.opp
Tactic:
constructor
State after:
case mp
x y : Ordering
⊢ x.opp = y → x = y.opp

case mpr
x y : Ordering
⊢ x = y.opp → x.opp = y

State before:
case mp
x y : Ordering
⊢ x.opp = y → x = y.opp
Tactic:
intro h
State after:
case mp
x y : Ordering
h : x.opp = y
⊢ x = y.opp

State before:
case mp
x y : Ordering
h : x.opp = y
⊢ x = y.opp
Tactic:
rw [←h, opp_opp]
State after:
no goals

State before:
case mpr
x y : Ordering
⊢ x = y.opp → x.opp = y
Tactic:
intro h
State after:
case mpr
x y : Ordering
h : x = y.opp
⊢ x.opp = y

State before:
case mpr
x y : Ordering
h : x = y.opp
⊢ x.opp = y
Tactic:
rw [h, opp_opp]
State after:
no goals