-- Mathlib/Data/List/Lex.lean
theorem _root_.Decidable.List.Lex.ne_iff [DecidableEq α] {l₁ l₂ : List α}
    (H : length l₁ ≤ length l₂) : Lex (· ≠ ·) l₁ l₂ ↔ l₁ ≠ l₂ :=
  ⟨to_ne, fun h => by
    induction' l₁ with a l₁ IH generalizing l₂ <;> rcases l₂ with - | ⟨b, l₂⟩
    · contradiction
    · apply nil
    · exact (not_lt_of_ge H).elim (succ_pos _)
    · by_cases ab : a = b
      · subst b
        apply cons
        exact IH (le_of_succ_le_succ H) (mt (congr_arg _) h)
      · exact rel ab ⟩

Proof state:
case nil.cons
α : Type u
inst✝ : DecidableEq α
b : α
l₂ : List α
H : [].length ≤ (b :: l₂).length
h : [] ≠ b :: l₂
⊢ Lex (fun x1 x2 => x1 ≠ x2) [] (b :: l₂)

Tactic:
apply nil

Result:
no goals

Proof state:
case cons.nil
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂
H : (a :: l₁).length ≤ [].length
h : a :: l₁ ≠ []
⊢ Lex (fun x1 x2 => x1 ≠ x2) (a :: l₁) []

Tactic:
exact (not_lt_of_ge H).elim (succ_pos _)

Result:
no goals

Proof state:
case nil.nil
α : Type u
inst✝ : DecidableEq α
H : [].length ≤ [].length
h : [] ≠ []
⊢ Lex (fun x1 x2 => x1 ≠ x2) [] []

Tactic:
contradiction

Result:
no goals

Proof state:
case cons.cons
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
⊢ Lex (fun x1 x2 => x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
by_cases ab : a = b

Result:
case pos
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : a = b
⊢ Lex (fun x1 x2 => x1 ≠ x2) (a :: l₁) (b :: l₂)

case neg
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : ¬a = b
⊢ Lex (fun x1 x2 => x1 ≠ x2) (a :: l₁) (b :: l₂)

Proof state:
case pos.h
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂
l₂ : List α
H : (a :: l₁).length ≤ (a :: l₂).length
h : a :: l₁ ≠ a :: l₂
⊢ Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂

Tactic:
exact IH (le_of_succ_le_succ H) (mt (congr_arg _) h)

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
h : l₁ ≠ l₂
⊢ Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂

Tactic:
induction' l₁ with a l₁ IH generalizing l₂ <;> rcases l₂ with - | ⟨b, l₂⟩

Result:
case nil.nil
α : Type u
inst✝ : DecidableEq α
H : [].length ≤ [].length
h : [] ≠ []
⊢ Lex (fun x1 x2 => x1 ≠ x2) [] []

case nil.cons
α : Type u
inst✝ : DecidableEq α
b : α
l₂ : List α
H : [].length ≤ (b :: l₂).length
h : [] ≠ b :: l₂
⊢ Lex (fun x1 x2 => x1 ≠ x2) [] (b :: l₂)

case cons.nil
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂
H : (a :: l₁).length ≤ [].length
h : a :: l₁ ≠ []
⊢ Lex (fun x1 x2 => x1 ≠ x2) (a :: l₁) []

case cons.cons
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
⊢ Lex (fun x1 x2 => x1 ≠ x2) (a :: l₁) (b :: l₂)

Proof state:
case neg
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : ¬a = b
⊢ Lex (fun x1 x2 => x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
exact rel ab

Result:
no goals

Proof state:
case pos
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂
l₂ : List α
H : (a :: l₁).length ≤ (a :: l₂).length
h : a :: l₁ ≠ a :: l₂
⊢ Lex (fun x1 x2 => x1 ≠ x2) (a :: l₁) (a :: l₂)

Tactic:
apply cons

Result:
case pos.h
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂
l₂ : List α
H : (a :: l₁).length ≤ (a :: l₂).length
h : a :: l₁ ≠ a :: l₂
⊢ Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂

Proof state:
case pos
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : a = b
⊢ Lex (fun x1 x2 => x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
subst b

Result:
case pos
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂
l₂ : List α
H : (a :: l₁).length ≤ (a :: l₂).length
h : a :: l₁ ≠ a :: l₂
⊢ Lex (fun x1 x2 => x1 ≠ x2) (a :: l₁) (a :: l₂)