[GOAL]
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt
[PROOFSTEP]
by_cases c
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt
[PROOFSTEP]
by_cases c
[GOAL]
case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h : c
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt
[PROOFSTEP]
simp [*]
[GOAL]
case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h : ¬c
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt
[PROOFSTEP]
simp [*]
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq
[PROOFSTEP]
by_cases c
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq
[PROOFSTEP]
by_cases c
[GOAL]
case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h : c
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq
[PROOFSTEP]
simp [*]
[GOAL]
case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h : ¬c
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq
[PROOFSTEP]
simp [*]
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt
[PROOFSTEP]
by_cases c
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt
[PROOFSTEP]
by_cases c
[GOAL]
case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h : c
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt
[PROOFSTEP]
simp [*]
[GOAL]
case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h : ¬c
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
lt : α → α → Prop
inst✝ : DecidableRel lt
a b : α
⊢ (cmpUsing lt a b = Ordering.lt) = lt a b
[PROOFSTEP]
simp
[GOAL]
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ (cmpUsing lt a b = Ordering.gt) = lt b a
[PROOFSTEP]
simp only [cmpUsing, Ordering.ite_eq_gt_distrib, if_false_right_eq_and, and_true, if_false_left_eq_and]
[GOAL]
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ (¬lt a b ∧ lt b a) = lt b a
[PROOFSTEP]
apply propext
[GOAL]
case a
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ ¬lt a b ∧ lt b a ↔ lt b a
[PROOFSTEP]
apply Iff.intro
[GOAL]
case a.mp
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ ¬lt a b ∧ lt b a → lt b a
[PROOFSTEP]
exact fun h => h.2
[GOAL]
case a.mpr
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ lt b a → ¬lt a b ∧ lt b a
[PROOFSTEP]
intro hba
[GOAL]
case a.mpr
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
hba : lt b a
⊢ ¬lt a b ∧ lt b a
[PROOFSTEP]
constructor
[GOAL]
case a.mpr.left
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
hba : lt b a
⊢ ¬lt a b
[PROOFSTEP]
intro hab
[GOAL]
case a.mpr.left
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
hba : lt b a
hab : lt a b
⊢ False
[PROOFSTEP]
exact absurd (_root_.trans hab hba) (irrefl a)
[GOAL]
case a.mpr.right
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
hba : lt b a
⊢ lt b a
[PROOFSTEP]
assumption
[GOAL]
α : Type u
lt : α → α → Prop
inst✝ : DecidableRel lt
a b : α
⊢ (cmpUsing lt a b = Ordering.eq) = (¬lt a b ∧ ¬lt b a)
[PROOFSTEP]
simp
