Theorem: compareOfLE.symm (GMLInit/Data/OrdInstances.lean)

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
⊢ (compareOfLE x y).swap = compareOfLE y x
Tactic:
unfold compareOfLE
State after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
by_cases x ≤ y, y ≤ x with
| isTrue _, isTrue _ => split <;> rfl
| isTrue _, isFalse _ => split <;> rfl
| isFalse _, isTrue _ => split <;> rfl
| isFalse _, isFalse _ =>
  cases Total.total (r:=(.≤.)) x y with
  | inl hxy => absurd hxy; assumption
  | inr hyx => absurd hyx; assumption
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : x ≤ y
h✝ : y ≤ x
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
split <;> rfl
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : x ≤ y
h✝ : ¬y ≤ x
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
split <;> rfl
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : y ≤ x
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
split <;> rfl
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
cases Total.total (r:=(.≤.)) x y with
| inl hxy => absurd hxy; assumption
| inr hyx => absurd hyx; assumption
State after:
no goals

State before:
case inl
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
hxy : x ≤ y
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
absurd hxy
State after:
case inl
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
hxy : x ≤ y
⊢ ¬x ≤ y

State before:
case inl
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
hxy : x ≤ y
⊢ ¬x ≤ y
Tactic:
assumption
State after:
no goals

State before:
case inr
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
hyx : y ≤ x
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
absurd hyx
State after:
case inr
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
hyx : y ≤ x
⊢ ¬y ≤ x

State before:
case inr
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
hyx : y ≤ x
⊢ ¬y ≤ x
Tactic:
assumption
State after:
no goals