α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ (¬lt a b ∧ lt b a) = lt b a
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ (cmpUsing lt a b = Ordering.gt) = lt b a
simp only [cmpUsing, Ordering.ite_eq_gt_distrib, if_false_right_eq_and, and_true,
  if_false_left_eq_and]
case a
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ ¬lt a b ∧ lt b a ↔ lt b a
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ (¬lt a b ∧ lt b a) = lt b a
apply propext
case a.mp
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ ¬lt a b ∧ lt b a → lt b a

case a.mpr
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ lt b a → ¬lt a b ∧ lt b a
case a
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ ¬lt a b ∧ lt b a ↔ lt b a
apply Iff.intro
no goals
case a.mp
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ ¬lt a b ∧ lt b a → lt b a
exact fun h => h.2
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
case a.mpr
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ lt b a → ¬lt a b ∧ lt b a
intro hba
case a.mpr.left
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
hba : lt b a
⊢ ¬lt a b

case a.mpr.right
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
hba : lt b a
⊢ lt b a
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
constructor
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
case a.mpr.left
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
hba : lt b a
⊢ ¬lt a b
intro hab
no goals
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
exact absurd (_root_.trans hab hba) (irrefl a)
no goals
case a.mpr.right
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
hba : lt b a
⊢ lt b a
assumption