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) [] []

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₂)

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₁) []

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₂)
α : 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₂
induction' l₁ with a l₁ IH generalizing l₂ <;> cases' l₂ with b l₂
no goals
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) [] []
contradiction
no goals
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₂)
apply nil
no goals
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₁) []
exact (not_lt_of_ge H).elim (succ_pos _)
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₂)

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₂)
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₂)
by_cases ab : a = b
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₂)
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₂)
subst b
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₂
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₂)
apply cons
no goals
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₂
exact IH (le_of_succ_le_succ H) (mt (congr_arg _) h)
no goals
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₂)
exact rel ab