α : Type u_1
β✝ : Type ?u.20401
inst✝¹ : LinearOrder α
x y : α
β : Type u_2
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ ¬y < x ↔ ¬y' < x'
α : Type u_1
β✝ : Type ?u.20401
inst✝¹ : LinearOrder α
x y : α
β : Type u_2
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x ≤ y ↔ x' ≤ y'
rw [← not_lt, ← not_lt]
case h
α : Type u_1
β✝ : Type ?u.20401
inst✝¹ : LinearOrder α
x y : α
β : Type u_2
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ y < x ↔ y' < x'
α : Type u_1
β✝ : Type ?u.20401
inst✝¹ : LinearOrder α
x y : α
β : Type u_2
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ ¬y < x ↔ ¬y' < x'
apply not_congr
case h.h
α : Type u_1
β✝ : Type ?u.20401
inst✝¹ : LinearOrder α
x y : α
β : Type u_2
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'
case h
α : Type u_1
β✝ : Type ?u.20401
inst✝¹ : LinearOrder α
x y : α
β : Type u_2
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ y < x ↔ y' < x'
apply lt_iff_lt_of_cmp_eq_cmp
no goals
case h.h
α : Type u_1
β✝ : Type ?u.20401
inst✝¹ : LinearOrder α
x y : α
β : Type u_2
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'
rwa [cmp_eq_cmp_symm]