-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
    [Std.Irrefl (· < · : α → α → Prop)]
    [Std.Asymm (· < · : α → α → Prop)]
    [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : List α} :
    l₁ ≤ l₂ ↔
      (l₁ = l₂.take l₁.length) ∨
        (∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
          (∀ j, (hj : j < i) →
            l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i])

Proof state:
case lt_asymm
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ ∀ (x y : α), decide (x < y) = true → decide (y < x) = false

Tactic:
simpa using Std.Asymm.asymm

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ (l₁ = take l₁.length l₂ ∨ ∃ i h h_1, (∀ (j : Nat) (hj : j < i), l₂[j] = l₁[j]) ∧ l₁[i] < l₂[i]) ↔
    l₁ = take l₁.length l₂ ∨ ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

Tactic:
simp only [eq_comm]

Result:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ (l₁ = take l₁.length l₂ ∨ ∃ i h h_1, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]) ↔
    l₁ = take l₁.length l₂ ∨ ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

Proof state:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ ((l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₂[j] == l₁[j]) = true) ∧ decide (l₁[i] < l₂[i]) = true) ↔
    l₁ = take l₁.length l₂ ∨ ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

Tactic:
simp only [isEqv_eq, beq_iff_eq, decide_eq_true_eq]

Result:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ (l₁ = take l₁.length l₂ ∨ ∃ i h h_1, (∀ (j : Nat) (hj : j < i), l₂[j] = l₁[j]) ∧ l₁[i] < l₂[i]) ↔
    l₁ = take l₁.length l₂ ∨ ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

Proof state:
case lt_irrefl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ ∀ (x y : α), (x == y) = true → decide (x < y) = false

Tactic:
simpa using Std.Irrefl.irrefl

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ l₁ ≤ l₂ ↔ l₁ = take l₁.length l₂ ∨ ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

Tactic:
rw [← lex_eq_false_iff_ge, lex_eq_false_iff_exists]

Result:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ ((l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₂[j] == l₁[j]) = true) ∧ decide (l₁[i] < l₂[i]) = true) ↔
    l₁ = take l₁.length l₂ ∨ ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

case lt_irrefl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ ∀ (x y : α), (x == y) = true → decide (x < y) = false

case lt_asymm
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ ∀ (x y : α), decide (x < y) = true → decide (y < x) = false

case lt_antisymm
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ ∀ (x y : α), decide (x < y) = false → decide (y < x) = false → (x == y) = true

Proof state:
case lt_antisymm
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ ∀ (x y : α), decide (x < y) = false → decide (y < x) = false → (x == y) = true

Tactic:
simpa using Std.Antisymm.antisymm

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
⊢ (l₁ = take l₁.length l₂ ∨ ∃ i h h_1, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]) ↔
    l₁ = take l₁.length l₂ ∨ ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

Tactic:
conv => lhs; simp +singlePass [exists_comm]

Result:
no goals