-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem cons_le_cons_iff [DecidableEq α] [LT α] [DecidableLT α]
    [i₀ : Std.Irrefl (· < · : α → α → Prop)]
    [i₁ : Std.Asymm (· < · : α → α → Prop)]
    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
    {a b} {l₁ l₂ : List α} :
    (a :: l₁) ≤ (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ ≤ l₂

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
h₁ : ¬b < a
h₂ : ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁
h₃ : a < b
⊢ a < b ∨ a = b ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

Tactic:
exact .inl h₃

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
⊢ ¬Lex (fun x1 x2 => x1 < x2) (b :: l₂) (a :: l₁) ↔ a < b ∨ a = b ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

Tactic:
simp only [not_cons_lex_cons_iff, ne_eq]

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
⊢ ¬b < a ∧ ¬b = a ∨ ¬b < a ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁ ↔ a < b ∨ a = b ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

Proof state:
case mpr.inl.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
h : a < b
⊢ ¬b < a ∧ ¬b = a

Tactic:
exact ⟨i₁.asymm _ _ h, fun w => i₀.irrefl _ (w ▸ h)⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
⊢ ¬b < a ∧ ¬b = a ∨ ¬b < a ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁ → a < b ∨ a = b ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

Tactic:
rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)

Result:
case mp.inl.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
h₁ : ¬b < a
h₂ : ¬b = a
⊢ a < b ∨ a = b ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

case mp.inr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
h₁ : ¬b < a
h₂ : ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁
⊢ a < b ∨ a = b ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
h₁ : ¬b < a
h₂ : ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁
h₃ : ¬a < b
⊢ a < b ∨ a = b ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

Tactic:
right

Result:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
h₁ : ¬b < a
h₂ : ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁
h₃ : ¬a < b
⊢ a = b ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

Proof state:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
h₁ : ¬b < a
h₂ : ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁
h₃ : ¬a < b
⊢ a = b ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

Tactic:
exact ⟨i₂.antisymm _ _ h₃ h₁, h₂⟩

Result:
no goals