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

Proof state:
case mpr.inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ < l₂
⊢ l₁ ≤ l₂

Tactic:
exact List.le_of_lt h

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ ≤ l₂
h' : ¬l₂ ≤ l₁
⊢ l₁ < l₂ ∨ l₁ = l₂

Tactic:
left

Result:
case neg.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ ≤ l₂
h' : ¬l₂ ≤ l₁
⊢ l₁ < l₂

Proof state:
case mp
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ ≤ l₂
⊢ l₁ < l₂ ∨ l₁ = l₂

Tactic:
by_cases h' : l₂ ≤ l₁

Result:
case pos
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ ≤ l₂
h' : l₂ ≤ l₁
⊢ l₁ < l₂ ∨ l₁ = l₂

case neg
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ ≤ l₂
h' : ¬l₂ ≤ l₁
⊢ l₁ < l₂ ∨ l₁ = l₂

Proof state:
case mp
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ l₁ ≤ l₂ → l₁ < l₂ ∨ l₁ = l₂

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ ≤ l₂
⊢ l₁ < l₂ ∨ l₁ = l₂

Proof state:
case mpr.inr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ : List α
⊢ l₁ ≤ l₁

Tactic:
exact List.le_refl l₁

Result:
no goals

Proof state:
case neg.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ ≤ l₂
h' : ¬l₂ ≤ l₁
⊢ l₁ < l₂

Tactic:
exact Decidable.not_not.mp h'

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ l₁ ≤ l₂ → l₁ < l₂ ∨ l₁ = l₂

case mpr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ l₁ < l₂ ∨ l₁ = l₂ → l₁ ≤ l₂

Proof state:
case mpr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ l₁ < l₂ ∨ l₁ = l₂ → l₁ ≤ l₂

Tactic:
rintro (h | rfl)

Result:
case mpr.inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ < l₂
⊢ l₁ ≤ l₂

case mpr.inr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ : List α
⊢ l₁ ≤ l₁

Proof state:
case pos
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ ≤ l₂
h' : l₂ ≤ l₁
⊢ l₁ < l₂ ∨ l₁ = l₂

Tactic:
right

Result:
case pos.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ ≤ l₂
h' : l₂ ≤ l₁
⊢ l₁ = l₂

Proof state:
case pos.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ ≤ l₂
h' : l₂ ≤ l₁
⊢ l₁ = l₂

Tactic:
apply List.le_antisymm h h'

Result:
no goals