[GOAL]
α : Type u
inst✝ : LinearOrder α
⊢ IsTotalPreorder α fun x x_1 => x ≤ x_1
[PROOFSTEP]
infer_instance
  -- porting note: added
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b
[PROOFSTEP]
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.lt ↔ a < b
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ Ordering.lt = Ordering.lt ↔ a < b
[PROOFSTEP]
simp only [*, lt_irrefl]
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ False ↔ a < b
[PROOFSTEP]
simp only [*, lt_irrefl]
[GOAL]
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a < b
[PROOFSTEP]
simp only [*, lt_irrefl]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b
[PROOFSTEP]
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.gt ↔ a > b
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ False ↔ a > b
[PROOFSTEP]
simp only [*, lt_irrefl, not_lt_of_gt]
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ False ↔ a > b
[PROOFSTEP]
simp only [*, lt_irrefl, not_lt_of_gt]
[GOAL]
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt ↔ a > b
[PROOFSTEP]
simp only [*, lt_irrefl, not_lt_of_gt]
[GOAL]
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ True ↔ a > b
[PROOFSTEP]
case _ h₁ h₂ =>
  have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂
  exact true_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
⊢ True ↔ a > b
[PROOFSTEP]
case _ h₁ h₂ =>
  have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂
  exact true_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
⊢ True ↔ a > b
[PROOFSTEP]
have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
h : b < a
⊢ True ↔ a > b
[PROOFSTEP]
exact true_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b
[PROOFSTEP]
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.eq ↔ a = b
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ False ↔ a = b
[PROOFSTEP]
try simp only []
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ False ↔ a = b
[PROOFSTEP]
simp only []
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq ↔ a = b
[PROOFSTEP]
try simp only []
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq ↔ a = b
[PROOFSTEP]
simp only []
[GOAL]
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b
[PROOFSTEP]
try simp only []
[GOAL]
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b
[PROOFSTEP]
simp only []
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ False ↔ a = b
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b
case neg α : Type u inst✝ : LinearOrder α a b : α h✝¹ : ¬a < b h✝ : ¬a = b ⊢ False ↔ a = b
[PROOFSTEP]
case _ h => exact false_iff_iff.2 <| ne_iff_lt_or_gt.2 <| .inl h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ False ↔ a = b
[PROOFSTEP]
case _ h => exact false_iff_iff.2 <| ne_iff_lt_or_gt.2 <| .inl h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ False ↔ a = b
[PROOFSTEP]
exact false_iff_iff.2 <| ne_iff_lt_or_gt.2 <| .inl h
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b
case neg α : Type u inst✝ : LinearOrder α a b : α h✝¹ : ¬a < b h✝ : ¬a = b ⊢ False ↔ a = b
[PROOFSTEP]
case _ _ h => exact true_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : ¬a < b
h : a = b
⊢ True ↔ a = b
[PROOFSTEP]
case _ _ h => exact true_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : ¬a < b
h : a = b
⊢ True ↔ a = b
[PROOFSTEP]
exact true_iff_iff.2 h
[GOAL]
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b
[PROOFSTEP]
case _ _ h => exact false_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : ¬a < b
h : ¬a = b
⊢ False ↔ a = b
[PROOFSTEP]
case _ _ h => exact false_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : ¬a < b
h : ¬a = b
⊢ False ↔ a = b
[PROOFSTEP]
exact false_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.gt ↔ a ≤ b
[PROOFSTEP]
cases h : compare a b
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.gt ↔ a ≤ b
[PROOFSTEP]
simp only []
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.gt ↔ a ≤ b
[PROOFSTEP]
simp only []
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.gt ↔ a ≤ b
[PROOFSTEP]
simp only []
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ True ↔ a ≤ b
[PROOFSTEP]
exact true_iff_iff.2 <| le_of_lt <| compare_lt_iff_lt.1 h
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ True ↔ a ≤ b
[PROOFSTEP]
exact true_iff_iff.2 <| le_of_eq <| compare_eq_iff_eq.1 h
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ False ↔ a ≤ b
[PROOFSTEP]
exact false_iff_iff.2 <| not_le_of_gt <| compare_gt_iff_gt.1 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.lt ↔ a ≥ b
[PROOFSTEP]
cases h : compare a b
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.lt ↔ a ≥ b
[PROOFSTEP]
simp only []
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.lt ↔ a ≥ b
[PROOFSTEP]
simp only []
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.lt ↔ a ≥ b
[PROOFSTEP]
simp only []
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ False ↔ a ≥ b
[PROOFSTEP]
exact false_iff_iff.2 <| (lt_iff_not_ge a b).1 <| compare_lt_iff_lt.1 h
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ True ↔ a ≥ b
[PROOFSTEP]
exact true_iff_iff.2 <| le_of_eq <| (·.symm) <| compare_eq_iff_eq.1 h
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ True ↔ a ≥ b
[PROOFSTEP]
exact true_iff_iff.2 <| le_of_lt <| compare_gt_iff_gt.1 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
o : Ordering
⊢ compare a b = o ↔ Ordering.toRel o a b
[PROOFSTEP]
cases o
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ Ordering.toRel Ordering.lt a b
[PROOFSTEP]
simp only [Ordering.toRel]
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ Ordering.toRel Ordering.eq a b
[PROOFSTEP]
simp only [Ordering.toRel]
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ Ordering.toRel Ordering.gt a b
[PROOFSTEP]
simp only [Ordering.toRel]
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b
[PROOFSTEP]
exact compare_lt_iff_lt
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b
[PROOFSTEP]
exact compare_eq_iff_eq
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b
[PROOFSTEP]
exact compare_gt_iff_gt
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ Ordering.swap (compare a b) = compare b a
[PROOFSTEP]
cases h : compare a b
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.swap Ordering.lt = compare b a
[PROOFSTEP]
simp only [Ordering.swap]
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.swap Ordering.eq = compare b a
[PROOFSTEP]
simp only [Ordering.swap]
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.swap Ordering.gt = compare b a
[PROOFSTEP]
simp only [Ordering.swap]
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.gt = compare b a
[PROOFSTEP]
symm
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq = compare b a
[PROOFSTEP]
symm
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.lt = compare b a
[PROOFSTEP]
symm
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ compare b a = Ordering.gt
[PROOFSTEP]
exact compare_gt_iff_gt.2 <| compare_lt_iff_lt.1 h
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ compare b a = Ordering.eq
[PROOFSTEP]
exact compare_eq_iff_eq.2 <| compare_eq_iff_eq.1 h |>.symm
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ compare b a = Ordering.lt
[PROOFSTEP]
exact compare_lt_iff_lt.2 <| compare_gt_iff_gt.1 h
