case mp
α : Type u
inst✝ : LinearOrder α
l l' : List α
h : lt l l'
⊢ Lex (fun x x_1 => x < x_1) l l'

case mpr
α : Type u
inst✝ : LinearOrder α
l l' : List α
h : Lex (fun x x_1 => x < x_1) l l'
⊢ lt l l'
α : Type u
inst✝ : LinearOrder α
l l' : List α
⊢ lt l l' ↔ Lex (fun x x_1 => x < x_1) l l'
constructor <;>
intro h
no goals
case mp
α : Type u
inst✝ : LinearOrder α
l l' : List α
h : lt l l'
⊢ Lex (fun x x_1 => x < x_1) l l'
induction h with
| nil b bs => exact Lex.nil
| @head a as b bs hab => apply Lex.rel; assumption
| @tail a as b bs hab hba _ ih =>
  have heq : a = b := _root_.le_antisymm (le_of_not_lt hba) (le_of_not_lt hab)
  subst b; apply Lex.cons; assumption
no goals
case mp.nil
α : Type u
inst✝ : LinearOrder α
l l' : List α
b : α
bs : List α
⊢ Lex (fun x x_1 => x < x_1) [] (b :: bs)
exact Lex.nil
case mp.head.h
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : a < b
⊢ a < b
case mp.head
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : a < b
⊢ Lex (fun x x_1 => x < x_1) (a :: as) (b :: bs)
apply Lex.rel
no goals
case mp.head.h
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : a < b
⊢ a < b
assumption
case mp.tail
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : ¬a < b
hba : ¬b < a
a✝ : lt as bs
ih : Lex (fun x x_1 => x < x_1) as bs
heq : a = b
⊢ Lex (fun x x_1 => x < x_1) (a :: as) (b :: bs)
case mp.tail
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : ¬a < b
hba : ¬b < a
a✝ : lt as bs
ih : Lex (fun x x_1 => x < x_1) as bs
⊢ Lex (fun x x_1 => x < x_1) (a :: as) (b :: bs)
have heq : a = b := _root_.le_antisymm (le_of_not_lt hba) (le_of_not_lt hab)
case mp.tail
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as bs : List α
a✝ : lt as bs
ih : Lex (fun x x_1 => x < x_1) as bs
hab hba : ¬a < a
⊢ Lex (fun x x_1 => x < x_1) (a :: as) (a :: bs)
case mp.tail
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : ¬a < b
hba : ¬b < a
a✝ : lt as bs
ih : Lex (fun x x_1 => x < x_1) as bs
heq : a = b
⊢ Lex (fun x x_1 => x < x_1) (a :: as) (b :: bs)
subst b
case mp.tail.h
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as bs : List α
a✝ : lt as bs
ih : Lex (fun x x_1 => x < x_1) as bs
hab hba : ¬a < a
⊢ Lex (fun x x_1 => x < x_1) as bs
case mp.tail
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as bs : List α
a✝ : lt as bs
ih : Lex (fun x x_1 => x < x_1) as bs
hab hba : ¬a < a
⊢ Lex (fun x x_1 => x < x_1) (a :: as) (a :: bs)
apply Lex.cons
no goals
case mp.tail.h
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as bs : List α
a✝ : lt as bs
ih : Lex (fun x x_1 => x < x_1) as bs
hab hba : ¬a < a
⊢ Lex (fun x x_1 => x < x_1) as bs
assumption
no goals
case mpr
α : Type u
inst✝ : LinearOrder α
l l' : List α
h : Lex (fun x x_1 => x < x_1) l l'
⊢ lt l l'
induction h with
| @nil a as => apply lt.nil
| @cons a as bs _ ih => apply lt.tail <;> simp [ih]
| @rel a as b bs h => apply lt.head; assumption
no goals
case mpr.nil
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
⊢ lt [] (a :: as)
apply lt.nil
no goals
case mpr.cons
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as bs : List α
h✝ : Lex (fun x x_1 => x < x_1) as bs
ih : lt as bs
⊢ lt (a :: as) (a :: bs)
apply lt.tail <;> simp [ih]
case mpr.rel.a
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
h : a < b
⊢ a < b
case mpr.rel
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
h : a < b
⊢ lt (a :: as) (b :: bs)
apply lt.head
no goals
case mpr.rel.a
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
h : a < b
⊢ a < b
assumption