-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α → Bool)
    (lt_irrefl : ∀ x y, x == y → lt x y = false)
    (lt_asymm : ∀ x y, lt x y = true → lt y x = false)
    (lt_antisymm : ∀ x y, lt x y = false → lt y x = false → x == y)
    {l₁ l₂ : Vector α n} :
    lex l₁ l₂ lt = false ↔
      (l₂.isEqv l₁ (· == ·)) ∨
        (∃ (i : Nat) (h : i < n),(∀ j, (hj : j < i) → l₁[j] == l₂[j]) ∧ lt l₂[i] l₁[i])

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
lt : α → α → Bool
lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false
lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false
lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true
l₁ : Array α
l₂ : Vector α l₁.size
⊢ { toArray := l₁, size_toArray := ⋯ }.lex l₂ lt = false ↔
    (l₂.isEqv { toArray := l₁, size_toArray := ⋯ } fun x1 x2 => x1 == x2) = true ∨
      ∃ i h,
        (∀ (j : Nat) (hj : j < i), ({ toArray := l₁, size_toArray := ⋯ }[j] == l₂[j]) = true) ∧
          lt l₂[i] { toArray := l₁, size_toArray := ⋯ }[i] = true

Tactic:
rcases l₂ with ⟨l₂, n₂⟩

Result:
case mk.mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
lt : α → α → Bool
lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false
lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false
lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true
l₁ l₂ : Array α
n₂ : l₂.size = l₁.size
⊢ { toArray := l₁, size_toArray := ⋯ }.lex { toArray := l₂, size_toArray := n₂ } lt = false ↔
    ({ toArray := l₂, size_toArray := n₂ }.isEqv { toArray := l₁, size_toArray := ⋯ } fun x1 x2 => x1 == x2) = true ∨
      ∃ i h,
        (∀ (j : Nat) (hj : j < i),
            ({ toArray := l₁, size_toArray := ⋯ }[j] == { toArray := l₂, size_toArray := n₂ }[j]) = true) ∧
          lt { toArray := l₂, size_toArray := n₂ }[i] { toArray := l₁, size_toArray := ⋯ }[i] = true

Proof state:
case mk.mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
lt : α → α → Bool
lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false
lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false
lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true
l₁ l₂ : Array α
n₂ : l₂.size = l₁.size
⊢ { toArray := l₁, size_toArray := ⋯ }.lex { toArray := l₂, size_toArray := n₂ } lt = false ↔
    ({ toArray := l₂, size_toArray := n₂ }.isEqv { toArray := l₁, size_toArray := ⋯ } fun x1 x2 => x1 == x2) = true ∨
      ∃ i h,
        (∀ (j : Nat) (hj : j < i),
            ({ toArray := l₁, size_toArray := ⋯ }[j] == { toArray := l₂, size_toArray := n₂ }[j]) = true) ∧
          lt { toArray := l₂, size_toArray := n₂ }[i] { toArray := l₁, size_toArray := ⋯ }[i] = true

Tactic:
simp_all [Array.lex_eq_false_iff_exists, n₂]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
lt : α → α → Bool
lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false
lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false
lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true
l₁ l₂ : Vector α n
⊢ l₁.lex l₂ lt = false ↔
    (l₂.isEqv l₁ fun x1 x2 => x1 == x2) = true ∨
      ∃ i h, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₂[i] l₁[i] = true

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
lt : α → α → Bool
lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false
lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false
lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true
l₁ : Array α
l₂ : Vector α l₁.size
⊢ { toArray := l₁, size_toArray := ⋯ }.lex l₂ lt = false ↔
    (l₂.isEqv { toArray := l₁, size_toArray := ⋯ } fun x1 x2 => x1 == x2) = true ∨
      ∃ i h,
        (∀ (j : Nat) (hj : j < i), ({ toArray := l₁, size_toArray := ⋯ }[j] == l₂[j]) = true) ∧
          lt l₂[i] { toArray := l₁, size_toArray := ⋯ }[i] = true