Theorem: algebra.Order.lex_true_of_ble_lex_true (Diploma/Order/MonomialOrder.lean)

State before:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h : algebra.Order.ble_lex_impl v₁ v₂ = true
⊢ lex v₁ v₂
Tactic:
rename_i n
State after:
n : ℕ
v₁ v₂ : Vector ℕ n
h : algebra.Order.ble_lex_impl v₁ v₂ = true
⊢ lex v₁ v₂

State before:
n : ℕ
v₁ v₂ : Vector ℕ n
h : algebra.Order.ble_lex_impl v₁ v₂ = true
⊢ lex v₁ v₂
Tactic:
exact aux n v₁ v₂ h
State after:
no goals

State before:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
h : algebra.Order.ble_lex_impl a b = true
⊢ lex a b
Tactic:
rw [Order.lex]
State after:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
h : algebra.Order.ble_lex_impl a b = true
⊢ lex_impl a b

State before:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
h : algebra.Order.ble_lex_impl a b = true
⊢ lex_impl a b
Tactic:
rw [Order.lex_impl]
State after:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
h : algebra.Order.ble_lex_impl a b = true
⊢ match a, b with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
    if x = y then lex_impl (Vector.tail a) (Vector.tail b) else x ≤ y

State before:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
h : algebra.Order.ble_lex_impl a b = true
⊢ match a, b with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
    if x = y then lex_impl (Vector.tail a) (Vector.tail b) else x ≤ y
Tactic:
match a, b with
  | ⟨[], _⟩  , ⟨[], _⟩     => simp
  | ⟨x::xs, _⟩, ⟨y::ys, _⟩ => split
                              simp
                              split
                              rw [Order.ble_lex_impl] at h
                              simp at h
                              split at h
                              exact aux (m-1) (tail ⟨x::xs, _⟩) (tail ⟨y::ys, _⟩) h
                              simp at *
                              rename_i heq₁ hneq heq₂ heq₃
                              have eq₁ := heq₂.left
                              have eq₂ := heq₃.left
                              rw [eq₁, eq₂] at hneq
                              contradiction                                  
                              rename_i heq₁ heq₂ hneq₁ 
                              rw [Order.ble_lex_impl] at h
                              split at h
                              simp at *
                              split at h
                              rename_i heq₃ heq₄ hneq₂
                              simp at heq₁ heq₂ heq₃ heq₄ hneq₂
                              have eq₁ := heq₁.left
                              have eq₂ := heq₂.left
                              have eq₃ := heq₃.left
                              have eq₄ := heq₄.left
                              rw [eq₁] at eq₃
                              rw [eq₂] at eq₄
                              rw [eq₃, eq₄] at hneq₁
                              contradiction
                              simp at h
                              rename_i heq₁ heq₂ _ _ _ _ _ _ _ _ _ _ _ heq₃ heq₄ _ 
                              simp at heq₁ heq₂ heq₃ heq₄
                              have eq₁ := heq₁.left
                              have eq₂ := heq₂.left
                              have eq₃ := heq₃.left
                              have eq₄ := heq₄.left
                              rw [eq₁] at eq₃
                              rw [eq₂] at eq₄
                              rw [eq₃, eq₄]
                              exact h
State after:
no goals

State before:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
property✝¹ property✝ : List.length [] = m
h : algebra.Order.ble_lex_impl { val := [], property := property✝¹ } { val := [], property := property✝ } = true
⊢ match { val := [], property := property✝¹ }, { val := [], property := property✝ } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
    if x = y then
      lex_impl (Vector.tail { val := [], property := property✝¹ }) (Vector.tail { val := [], property := property✝ })
    else x ≤ y
Tactic:
simp
State after:
no goals

State before:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝ : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝¹ } { val := y :: ys, property := property✝ } = true
⊢ match { val := x :: xs, property := property✝¹ }, { val := y :: ys, property := property✝ } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x_1 :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x_1 = y_1 then
      lex_impl (Vector.tail { val := x :: xs, property := property✝¹ })
        (Vector.tail { val := y :: ys, property := property✝ })
    else x_1 ≤ y_1
Tactic:
split
State after:
case h_1
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := [], property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := [], property := property✝ }
⊢ True

case h_2
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then
    lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
  else x✝ ≤ y✝

State before:
case h_1
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := [], property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := [], property := property✝ }
⊢ True

case h_2
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then
    lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
  else x✝ ≤ y✝
Tactic:
simp
State after:
case h_2
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then
    lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
  else x✝ ≤ y✝

State before:
case h_2
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then
    lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
  else x✝ ≤ y✝
Tactic:
split
State after:
case h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : x✝ = y✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : x✝ = y✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
rw [Order.ble_lex_impl] at h
State after:
case h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  (match { val := x :: xs, property := property✝³ }, { val := y :: ys, property := property✝² } with
    | { val := [], property := property }, { val := [], property := property_1 } => true
    | { val := x_1 :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
      if (x_1 == y_1) = true then
        algebra.Order.ble_lex_impl (Vector.tail { val := x :: xs, property := property✝³ })
          (Vector.tail { val := y :: ys, property := property✝² })
      else decide (x_1 ≤ y_1)) =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : x✝ = y✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  (match { val := x :: xs, property := property✝³ }, { val := y :: ys, property := property✝² } with
    | { val := [], property := property }, { val := [], property := property_1 } => true
    | { val := x_1 :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
      if (x_1 == y_1) = true then
        algebra.Order.ble_lex_impl (Vector.tail { val := x :: xs, property := property✝³ })
          (Vector.tail { val := y :: ys, property := property✝² })
      else decide (x_1 ≤ y_1)) =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : x✝ = y✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
simp at h
State after:
case h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : x✝ = y✝
h :
  if x = y then
    algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
        (tail { val := y :: ys, property := property✝² }) =
      true
  else x ≤ y
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : x✝ = y✝
h :
  if x = y then
    algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
        (tail { val := y :: ys, property := property✝² }) =
      true
  else x ≤ y
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
split at h
State after:
case h_2.inl.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : x = y
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : ¬x = y
h : x ≤ y
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inl.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : x = y
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : ¬x = y
h : x ≤ y
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
exact aux (m-1) (tail ⟨x::xs, _⟩) (tail ⟨y::ys, _⟩) h
State after:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : ¬x = y
h : x ≤ y
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : ¬x = y
h : x ≤ y
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
simp at *
State after:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : x✝ = y✝
h✝ : ¬x = y
h : x ≤ y
heq✝¹ : x = x✝ ∧ xs = tail✝¹
heq✝ : y = y✝ ∧ ys = tail✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : x✝ = y✝
h✝ : ¬x = y
h : x ≤ y
heq✝¹ : x = x✝ ∧ xs = tail✝¹
heq✝ : y = y✝ ∧ ys = tail✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
rename_i heq₁ hneq heq₂ heq₃
State after:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₁ : x✝ = y✝
hneq : ¬x = y
h : x ≤ y
heq₂ : x = x✝ ∧ xs = tail✝¹
heq₃ : y = y✝ ∧ ys = tail✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₁ : x✝ = y✝
hneq : ¬x = y
h : x ≤ y
heq₂ : x = x✝ ∧ xs = tail✝¹
heq₃ : y = y✝ ∧ ys = tail✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
have eq₁ := heq₂.left
State after:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₁ : x✝ = y✝
hneq : ¬x = y
h : x ≤ y
heq₂ : x = x✝ ∧ xs = tail✝¹
heq₃ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₁ : x✝ = y✝
hneq : ¬x = y
h : x ≤ y
heq₂ : x = x✝ ∧ xs = tail✝¹
heq₃ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
have eq₂ := heq₃.left
State after:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₁ : x✝ = y✝
hneq : ¬x = y
h : x ≤ y
heq₂ : x = x✝ ∧ xs = tail✝¹
heq₃ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₁ : x✝ = y✝
hneq : ¬x = y
h : x ≤ y
heq₂ : x = x✝ ∧ xs = tail✝¹
heq₃ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
rw [eq₁, eq₂] at hneq
State after:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₁ : x✝ = y✝
hneq : ¬x✝ = y✝
h : x ≤ y
heq₂ : x = x✝ ∧ xs = tail✝¹
heq₃ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₁ : x✝ = y✝
hneq : ¬x✝ = y✝
h : x ≤ y
heq₂ : x = x✝ ∧ xs = tail✝¹
heq₃ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
contradiction
State after:
case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
rename_i heq₁ heq₂ hneq₁
State after:
case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₁ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq₂ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
hneq₁ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₁ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq₂ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
hneq₁ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
rw [Order.ble_lex_impl] at h
State after:
case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  (match { val := x :: xs, property := property✝³ }, { val := y :: ys, property := property✝² } with
    | { val := [], property := property }, { val := [], property := property_1 } => true
    | { val := x_1 :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
      if (x_1 == y_1) = true then
        algebra.Order.ble_lex_impl (Vector.tail { val := x :: xs, property := property✝³ })
          (Vector.tail { val := y :: ys, property := property✝² })
      else decide (x_1 ≤ y_1)) =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₁ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq₂ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
hneq₁ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  (match { val := x :: xs, property := property✝³ }, { val := y :: ys, property := property✝² } with
    | { val := [], property := property }, { val := [], property := property_1 } => true
    | { val := x_1 :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
      if (x_1 == y_1) = true then
        algebra.Order.ble_lex_impl (Vector.tail { val := x :: xs, property := property✝³ })
          (Vector.tail { val := y :: ys, property := property✝² })
      else decide (x_1 ≤ y_1)) =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₁ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq₂ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
hneq₁ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
split at h
State after:
case h_2.inr.h_1
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝³ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝² : List.length (y✝ :: tail✝) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝² }
hneq₁ : ¬x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := [], property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := [], property := property✝ }
h : true = true
⊢ x✝ ≤ y✝

case h_2.inr.h_2
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h :
  (if (x✝ == y✝) = true then
      algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
        (tail { val := y :: ys, property := property✝⁴ })
    else decide (x✝ ≤ y✝)) =
    true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_1
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝³ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝² : List.length (y✝ :: tail✝) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝² }
hneq₁ : ¬x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := [], property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := [], property := property✝ }
h : true = true
⊢ x✝ ≤ y✝

case h_2.inr.h_2
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h :
  (if (x✝ == y✝) = true then
      algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
        (tail { val := y :: ys, property := property✝⁴ })
    else decide (x✝ ≤ y✝)) =
    true
⊢ x✝¹ ≤ y✝¹
Tactic:
simp at *
State after:
case h_2.inr.h_2
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h :
  (if (x✝ == y✝) = true then
      algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
        (tail { val := y :: ys, property := property✝⁴ })
    else decide (x✝ ≤ y✝)) =
    true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h :
  (if (x✝ == y✝) = true then
      algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
        (tail { val := y :: ys, property := property✝⁴ })
    else decide (x✝ ≤ y✝)) =
    true
⊢ x✝¹ ≤ y✝¹
Tactic:
split at h
State after:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : (x✝ == y✝) = true
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : (x✝ == y✝) = true
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹
Tactic:
rename_i heq₃ heq₄ hneq₂
State after:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₃ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq₄ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
hneq₂ : (x✝ == y✝) = true
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₃ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq₄ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
hneq₂ : (x✝ == y✝) = true
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹
Tactic:
simp at heq₁ heq₂ heq₃ heq₄ hneq₂
State after:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹
Tactic:
have eq₁ := heq₁.left
State after:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹
Tactic:
have eq₂ := heq₂.left
State after:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹
Tactic:
have eq₃ := heq₃.left
State after:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x = x✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x = x✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹
Tactic:
have eq₄ := heq₄.left
State after:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x = x✝
eq₄ : y = y✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x = x✝
eq₄ : y = y✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹
Tactic:
rw [eq₁] at eq₃
State after:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y = y✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y = y✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹
Tactic:
rw [eq₂] at eq₄
State after:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y✝¹ = y✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y✝¹ = y✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹
Tactic:
rw [eq₃, eq₄] at hneq₁
State after:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
hneq₁ : ¬x✝ = y✝
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y✝¹ = y✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
hneq₁ : ¬x✝ = y✝
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y✝¹ = y✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹
Tactic:
contradiction
State after:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹
Tactic:
simp at h
State after:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
rename_i heq₁ heq₂ _ _ _ _ _ _ _ _ _ _ _ heq₃ heq₄ _
State after:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁴ } = { val := x✝¹ :: heq₁✝, property := heq₂✝ }
heq₂ : { val := y :: ys, property := property✝³ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₃ : { val := x :: xs, property := property✝⁴ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq₄ : { val := y :: ys, property := property✝³ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁴ } = { val := x✝¹ :: heq₁✝, property := heq₂✝ }
heq₂ : { val := y :: ys, property := property✝³ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq₃ : { val := x :: xs, property := property✝⁴ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq₄ : { val := y :: ys, property := property✝³ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
simp at heq₁ heq₂ heq₃ heq₄
State after:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
⊢ x✝¹ ≤ y✝¹
Tactic:
have eq₁ := heq₁.left
State after:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
⊢ x✝¹ ≤ y✝¹
Tactic:
have eq₂ := heq₂.left
State after:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
⊢ x✝¹ ≤ y✝¹
Tactic:
have eq₃ := heq₃.left
State after:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x = x✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x = x✝
⊢ x✝¹ ≤ y✝¹
Tactic:
have eq₄ := heq₄.left
State after:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x = x✝
eq₄ : y = y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x = x✝
eq₄ : y = y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
rw [eq₁] at eq₃
State after:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y = y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y = y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
rw [eq₂] at eq₄
State after:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y✝¹ = y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y✝¹ = y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
rw [eq₃, eq₄]
State after:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y✝¹ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁴ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝³ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
heq₁✝ : List ℕ
heq₂✝ : List.length (x✝¹ :: heq₁✝) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝ : ¬(x✝ == y✝) = true
h : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = heq₁✝
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y✝¹ = y✝
⊢ x✝ ≤ y✝
Tactic:
exact h
State after:
no goals