[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : Lex r (a :: l₁) (a :: l₂)
⊢ Lex r l₁ l₂
[PROOFSTEP]
cases' h with _ _ _ _ _ h _ _ _ _ h
[GOAL]
case cons
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : Lex r l₁ l₂
⊢ Lex r l₁ l₂
case rel α : Type u r : α → α → Prop inst✝ : IsIrrefl α r a : α l₁ l₂ : List α h : r a a ⊢ Lex r l₁ l₂
[PROOFSTEP]
exacts [h, (irrefl_of r a h).elim]
[GOAL]
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : IsTrichotomous α r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
[PROOFSTEP]
rcases trichotomous_of r a b with (ab | rfl | ab)
[GOAL]
case inl
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : IsTrichotomous α r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r a b
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
[PROOFSTEP]
exact Or.inl (rel ab)
[GOAL]
case inr.inl
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : IsTrichotomous α r
a : α
l₁ l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (a :: l₂) ∨ Lex r (a :: l₂) (a :: l₃)
[PROOFSTEP]
exact (aux _ l₂ _ h).imp cons cons
[GOAL]
case inr.inr
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : IsTrichotomous α r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
[PROOFSTEP]
exact Or.inr (rel ab)
[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsTrichotomous α r
a : α
l₁ : List α
b : α
l₂ : List α
⊢ Lex r (a :: l₁) (b :: l₂) ∨ a :: l₁ = b :: l₂ ∨ Lex r (b :: l₂) (a :: l₁)
[PROOFSTEP]
rcases trichotomous_of r a b with (ab | rfl | ab)
[GOAL]
case inl
α : Type u
r : α → α → Prop
inst✝ : IsTrichotomous α r
a : α
l₁ : List α
b : α
l₂ : List α
ab : r a b
⊢ Lex r (a :: l₁) (b :: l₂) ∨ a :: l₁ = b :: l₂ ∨ Lex r (b :: l₂) (a :: l₁)
[PROOFSTEP]
exact Or.inl (rel ab)
[GOAL]
case inr.inl
α : Type u
r : α → α → Prop
inst✝ : IsTrichotomous α r
a : α
l₁ l₂ : List α
⊢ Lex r (a :: l₁) (a :: l₂) ∨ a :: l₁ = a :: l₂ ∨ Lex r (a :: l₂) (a :: l₁)
[PROOFSTEP]
exact (aux l₁ l₂).imp cons (Or.imp (congr_arg _) cons)
[GOAL]
case inr.inr
α : Type u
r : α → α → Prop
inst✝ : IsTrichotomous α r
a : α
l₁ : List α
b : α
l₂ : List α
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ a :: l₁ = b :: l₂ ∨ Lex r (b :: l₂) (a :: l₁)
[PROOFSTEP]
exact Or.inr (Or.inr (rel ab))
[GOAL]
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
l₁ : List α
h : Lex r l₁ []
⊢ False
[PROOFSTEP]
cases h
[GOAL]
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))
[PROOFSTEP]
haveI := decidableRel r l₁ l₂
[GOAL]
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))
[PROOFSTEP]
refine' decidable_of_iff (r a b ∨ a = b ∧ Lex r l₁ l₂) ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b ∨ a = b ∧ Lex r l₁ l₂
⊢ Lex r (a :: l₁) (b :: l₂)
[PROOFSTEP]
rcases h with (h | ⟨rfl, h⟩)
[GOAL]
case refine'_1.inl
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b
⊢ Lex r (a :: l₁) (b :: l₂)
[PROOFSTEP]
exact Lex.rel h
[GOAL]
case refine'_1.inr.intro
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ Lex r (a :: l₁) (a :: l₂)
[PROOFSTEP]
exact Lex.cons h
[GOAL]
case refine'_2
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r (a :: l₁) (b :: l₂)
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂
[PROOFSTEP]
rcases h with (_ | h | h)
[GOAL]
case refine'_2.cons
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ r a a ∨ a = a ∧ Lex r l₁ l₂
[PROOFSTEP]
exact Or.inr ⟨rfl, h⟩
[GOAL]
case refine'_2.rel
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂
[PROOFSTEP]
exact Or.inl h
[GOAL]
α : Type u
inst✝ : DecidableEq α
l₁ l₂ : List α
H : length l₁ ≤ length l₂
h : l₁ ≠ l₂
⊢ Lex (fun x x_1 => x ≠ x_1) l₁ l₂
[PROOFSTEP]
induction' l₁ with a l₁ IH generalizing l₂
[GOAL]
case nil
α : Type u
inst✝ : DecidableEq α
l₁ l₂✝ : List α
H✝ : length l₁ ≤ length l₂✝
h✝ : l₁ ≠ l₂✝
l₂ : List α
H : length [] ≤ length l₂
h : [] ≠ l₂
⊢ Lex (fun x x_1 => x ≠ x_1) [] l₂
[PROOFSTEP]
cases' l₂ with b l₂
[GOAL]
case cons
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : length l₁✝ ≤ length l₂✝
h✝ : l₁✝ ≠ l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
l₂ : List α
H : length (a :: l₁) ≤ length l₂
h : a :: l₁ ≠ l₂
⊢ Lex (fun x x_1 => x ≠ x_1) (a :: l₁) l₂
[PROOFSTEP]
cases' l₂ with b l₂
[GOAL]
case nil.nil
α : Type u
inst✝ : DecidableEq α
l₁ l₂ : List α
H✝ : length l₁ ≤ length l₂
h✝ : l₁ ≠ l₂
H : length [] ≤ length []
h : [] ≠ []
⊢ Lex (fun x x_1 => x ≠ x_1) [] []
[PROOFSTEP]
contradiction
[GOAL]
case nil.cons
α : Type u
inst✝ : DecidableEq α
l₁ l₂✝ : List α
H✝ : length l₁ ≤ length l₂✝
h✝ : l₁ ≠ l₂✝
b : α
l₂ : List α
H : length [] ≤ length (b :: l₂)
h : [] ≠ b :: l₂
⊢ Lex (fun x x_1 => x ≠ x_1) [] (b :: l₂)
[PROOFSTEP]
apply nil
[GOAL]
case cons.nil
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂ : List α
H✝ : length l₁✝ ≤ length l₂
h✝ : l₁✝ ≠ l₂
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
H : length (a :: l₁) ≤ length []
h : a :: l₁ ≠ []
⊢ Lex (fun x x_1 => x ≠ x_1) (a :: l₁) []
[PROOFSTEP]
exact (not_lt_of_ge H).elim (succ_pos _)
[GOAL]
case cons.cons
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : length l₁✝ ≤ length l₂✝
h✝ : l₁✝ ≠ l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
b : α
l₂ : List α
H : length (a :: l₁) ≤ length (b :: l₂)
h : a :: l₁ ≠ b :: l₂
⊢ Lex (fun x x_1 => x ≠ x_1) (a :: l₁) (b :: l₂)
[PROOFSTEP]
by_cases ab : a = b
[GOAL]
case pos
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : length l₁✝ ≤ length l₂✝
h✝ : l₁✝ ≠ l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
b : α
l₂ : List α
H : length (a :: l₁) ≤ length (b :: l₂)
h : a :: l₁ ≠ b :: l₂
ab : a = b
⊢ Lex (fun x x_1 => x ≠ x_1) (a :: l₁) (b :: l₂)
[PROOFSTEP]
subst b
[GOAL]
case pos
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : length l₁✝ ≤ length l₂✝
h✝ : l₁✝ ≠ l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
l₂ : List α
H : length (a :: l₁) ≤ length (a :: l₂)
h : a :: l₁ ≠ a :: l₂
⊢ Lex (fun x x_1 => x ≠ x_1) (a :: l₁) (a :: l₂)
[PROOFSTEP]
apply cons
[GOAL]
case pos.h
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : length l₁✝ ≤ length l₂✝
h✝ : l₁✝ ≠ l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
l₂ : List α
H : length (a :: l₁) ≤ length (a :: l₂)
h : a :: l₁ ≠ a :: l₂
⊢ Lex (fun x x_1 => x ≠ x_1) l₁ l₂
[PROOFSTEP]
exact IH (le_of_succ_le_succ H) (mt (congr_arg _) h)
[GOAL]
case neg
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : length l₁✝ ≤ length l₂✝
h✝ : l₁✝ ≠ l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
b : α
l₂ : List α
H : length (a :: l₁) ≤ length (b :: l₂)
h : a :: l₁ ≠ b :: l₂
ab : ¬a = b
⊢ Lex (fun x x_1 => x ≠ x_1) (a :: l₁) (b :: l₂)
[PROOFSTEP]
exact rel ab
[GOAL]
α : Type u
l₁ l₂ : List α
H : length l₁ ≤ length l₂
⊢ Lex (fun x x_1 => x ≠ x_1) l₁ l₂ ↔ l₁ ≠ l₂
[PROOFSTEP]
classical exact Decidable.List.Lex.ne_iff H
[GOAL]
α : Type u
l₁ l₂ : List α
H : length l₁ ≤ length l₂
⊢ Lex (fun x x_1 => x ≠ x_1) l₁ l₂ ↔ l₁ ≠ l₂
[PROOFSTEP]
exact Decidable.List.Lex.ne_iff H
[GOAL]
α : Type u
inst✝ : LinearOrder α
l l' : List α
⊢ lt l l' ↔ Lex (fun x x_1 => x < x_1) l l'
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
inst✝ : LinearOrder α
l l' : List α
⊢ lt l l' → Lex (fun x x_1 => x < x_1) l l'
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
inst✝ : LinearOrder α
l l' : List α
⊢ Lex (fun x x_1 => x < x_1) l l' → lt l l'
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
inst✝ : LinearOrder α
l l' : List α
h : lt l l'
⊢ Lex (fun x x_1 => x < x_1) l l'
[PROOFSTEP]
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
[GOAL]
case mp
α : Type u
inst✝ : LinearOrder α
l l' : List α
h : lt l l'
⊢ Lex (fun x x_1 => x < x_1) l l'
[PROOFSTEP]
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
[GOAL]
case mp.nil
α : Type u
inst✝ : LinearOrder α
l l' : List α
b : α
bs : List α
⊢ Lex (fun x x_1 => x < x_1) [] (b :: bs)
[PROOFSTEP]

| nil b bs => exact Lex.nil
[GOAL]
case mp.nil
α : Type u
inst✝ : LinearOrder α
l l' : List α
b : α
bs : List α
⊢ Lex (fun x x_1 => x < x_1) [] (b :: bs)
[PROOFSTEP]
exact Lex.nil
[GOAL]
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)
[PROOFSTEP]

| @head a as b bs hab => apply Lex.rel; assumption
[GOAL]
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)
[PROOFSTEP]
apply Lex.rel
[GOAL]
case mp.head.h
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : a < b
⊢ a < b
[PROOFSTEP]
assumption
[GOAL]
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)
[PROOFSTEP]

|
  @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
[GOAL]
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)
[PROOFSTEP]
have heq : a = b := _root_.le_antisymm (le_of_not_lt hba) (le_of_not_lt hab)
[GOAL]
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)
[PROOFSTEP]
subst b
[GOAL]
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)
[PROOFSTEP]
apply Lex.cons
[GOAL]
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
[PROOFSTEP]
assumption
[GOAL]
case mpr
α : Type u
inst✝ : LinearOrder α
l l' : List α
h : Lex (fun x x_1 => x < x_1) l l'
⊢ lt l l'
[PROOFSTEP]
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
[GOAL]
case mpr
α : Type u
inst✝ : LinearOrder α
l l' : List α
h : Lex (fun x x_1 => x < x_1) l l'
⊢ lt l l'
[PROOFSTEP]
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
[GOAL]
case mpr.nil
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
⊢ lt [] (a :: as)
[PROOFSTEP]

| @nil a as => apply lt.nil
[GOAL]
case mpr.nil
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
⊢ lt [] (a :: as)
[PROOFSTEP]
apply lt.nil
[GOAL]
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)
[PROOFSTEP]

| @cons a as bs _ ih => apply lt.tail <;> simp [ih]
[GOAL]
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)
[PROOFSTEP]
apply lt.tail
[GOAL]
case mpr.cons.a
α : 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
⊢ ¬a < a
[PROOFSTEP]
simp [ih]
[GOAL]
case mpr.cons.a
α : 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
⊢ ¬a < a
[PROOFSTEP]
simp [ih]
[GOAL]
case mpr.cons.a
α : 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 as bs
[PROOFSTEP]
simp [ih]
[GOAL]
case mpr.rel
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
h : a < b
⊢ lt (a :: as) (b :: bs)
[PROOFSTEP]

| @rel a as b bs h => apply lt.head; assumption
[GOAL]
case mpr.rel
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
h : a < b
⊢ lt (a :: as) (b :: bs)
[PROOFSTEP]
apply lt.head
[GOAL]
case mpr.rel.a
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
h : a < b
⊢ a < b
[PROOFSTEP]
assumption
