-- 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:
case mp.inl.intro.h.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₂ : ¬b = a
h₃ : ¬a < b
⊢ False

Tactic:
apply h₂

Result:
case mp.inl.intro.h.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₂ : ¬b = a
h₃ : ¬a < b
⊢ b = a

Proof state:
case mp.inl.intro.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₂ : ¬b = a
⊢ a < b

Tactic:
apply Decidable.byContradiction

Result:
case mp.inl.intro.h.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₂ : ¬b = a
⊢ ¬a < b → False

Proof state:
case mpr
α : 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 α
⊢ a < b ∨ a = b ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁ → ¬b < a ∧ ¬b = a ∨ ¬b < a ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

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

Result:
case mpr.inl
α : 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 ∨ ¬b < a ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

case mpr.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₁ : a = b
h₂ : ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁
⊢ ¬b < a ∧ ¬b = a ∨ ¬b < a ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

Proof state:
case mpr.inr.intro.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
h₂ : ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁
⊢ ¬b < a ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

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

Result:
no goals

Proof state:
case mpr.inl
α : 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 ∨ ¬b < a ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

Tactic:
left

Result:
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

Proof state:
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₁

Tactic:
left

Result:
case mp.inl.intro.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₂ : ¬b = a
⊢ a < b

Proof state:
case mp.inl.intro.h.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₂ : ¬b = a
h₃ : ¬a < b
⊢ b = a

Tactic:
exact i₂.antisymm _ _ h₁ 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 α
⊢ ¬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:
constructor

Result:
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₁

case mpr
α : 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 α
⊢ a < b ∨ a = b ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁ → ¬b < a ∧ ¬b = a ∨ ¬b < a ∧ ¬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 α
⊢ a :: l₁ ≤ b :: l₂ ↔ a < b ∨ a = b ∧ l₁ ≤ l₂

Tactic:
dsimp only [instLE, instLT, List.le, List.lt]

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 α
⊢ ¬Lex (fun x1 x2 => x1 < x2) (b :: l₂) (a :: l₁) ↔ a < b ∨ a = b ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

Proof state:
case mp.inl.intro.h.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₂ : ¬b = a
⊢ ¬a < b → False

Tactic:
intro h₃

Result:
case mp.inl.intro.h.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₂ : ¬b = a
h₃ : ¬a < b
⊢ False

Proof state:
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₁

Tactic:
if h₃ : a < b then
  exact .inl h₃
else
  right
  exact ⟨i₂.antisymm _ _ h₃ h₁, h₂⟩

Result:
no goals

Proof state:
case mpr.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₁ : a = b
h₂ : ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁
⊢ ¬b < a ∧ ¬b = a ∨ ¬b < a ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁

Tactic:
right

Result:
case mpr.inr.intro.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
h₂ : ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁
⊢ ¬b < a ∧ ¬Lex (fun x1 x2 => x1 < x2) l₂ l₁