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

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

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

State before:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
h : lex_impl a b
⊢ algebra.Order.ble_lex_impl a b = true
Tactic:
match a, b with
 | ⟨[], _⟩, ⟨[], _⟩       => rw [Order.ble_lex_impl]
 | ⟨x::xs, _⟩, ⟨y::ys, _⟩ => rw [Order.ble_lex_impl]
                             split;rfl
                             split
                             rw [lex_impl] at h
                             simp at h
                             split at h
                             apply Order.ble_eq_true_of_lex h
                             rename_i heq₁ heq₂ neq eq
                             simp at heq₁ heq₂
                             have eq₁ := heq₁.left
                             have eq₂ := heq₂.left
                             simp at neq
                             rw [eq₁, eq₂] at eq
                             contradiction
                             rw [lex_impl] at h
                             simp at h
                             split at h
                             rename_i heq₁ heq₂ neq eq
                             simp at heq₁ heq₂
                             have eq₁ := heq₁.left
                             have eq₂ := heq₂.left
                             simp at neq
                             rw [eq₁, eq₂] at eq
                             contradiction
                             simp
                             rename_i heq₁ heq₂ _ _
                             simp at heq₁ heq₂
                             have eq₁ := Eq.symm heq₁.left
                             have eq₂ := Eq.symm heq₂.left
                             rwa [eq₁, eq₂]
State after:
no goals

State before:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
property✝¹ property✝ : List.length [] = m
h : lex_impl { val := [], property := property✝¹ } { val := [], property := property✝ }
⊢ algebra.Order.ble_lex_impl { val := [], property := property✝¹ } { val := [], property := property✝ } = true
Tactic:
rw [Order.ble_lex_impl]
State after:
no goals

State before:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝ : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝¹ } { val := y :: ys, property := property✝ }
⊢ algebra.Order.ble_lex_impl { val := x :: xs, property := property✝¹ } { val := y :: ys, property := property✝ } = true
Tactic:
rw [Order.ble_lex_impl]
State after:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝ : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝¹ } { val := y :: ys, property := property✝ }
⊢ (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

State before:
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝ : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝¹ } { val := y :: ys, property := property✝ }
⊢ (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
Tactic:
split
State after:
case h_1
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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 = true

case h_2
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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✝) = true then
      algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
        (tail { val := y :: ys, property := property✝² })
    else decide (x✝ ≤ y✝)) =
    true

State before:
case h_1
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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 = true

case h_2
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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✝) = true then
      algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
        (tail { val := y :: ys, property := property✝² })
    else decide (x✝ ≤ y✝)) =
    true
Tactic:
rfl
State after:
case h_2
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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✝) = true then
      algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
        (tail { val := y :: ys, property := property✝² })
    else decide (x✝ ≤ y✝)) =
    true

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

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true

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

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

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
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 then
      lex_impl (Vector.tail { val := x :: xs, property := property✝³ })
        (Vector.tail { val := y :: ys, property := property✝² })
    else x_1 ≤ y_1
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
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

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

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true

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

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

case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inl.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true
Tactic:
apply Order.ble_eq_true_of_lex h
State after:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true
Tactic:
rename_i heq₁ heq₂ neq eq
State after:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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✝ }
neq : (x✝ == y✝) = true
eq : ¬x = y
h : x ≤ y
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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✝ }
neq : (x✝ == y✝) = true
eq : ¬x = y
h : x ≤ y
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

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

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
neq : (x✝ == y✝) = true
eq : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

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

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
neq : (x✝ == y✝) = true
eq : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

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

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
neq : (x✝ == y✝) = true
eq : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

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

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
eq : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
neq : x✝ = y✝
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

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

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
eq : ¬x✝ = y✝
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
neq : x✝ = y✝
⊢ algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true
Tactic:
contradiction
State after:
case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h : lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² }
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
⊢ decide (x✝ ≤ y✝) = true
Tactic:
rw [lex_impl] at h
State after:
case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
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 then
      lex_impl (Vector.tail { val := x :: xs, property := property✝³ })
        (Vector.tail { val := y :: ys, property := property✝² })
    else x_1 ≤ y_1
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
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
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 then
      lex_impl (Vector.tail { val := x :: xs, property := property✝³ })
        (Vector.tail { val := y :: ys, property := property✝² })
    else x_1 ≤ y_1
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
⊢ decide (x✝ ≤ y✝) = true
Tactic:
simp at h
State after:
case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  if x = y then
    lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
  else 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
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  if x = y then
    lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
  else 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
⊢ decide (x✝ ≤ y✝) = true
Tactic:
split at h
State after:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Tactic:
rename_i heq₁ heq₂ neq eq
State after:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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✝ }
neq : ¬(x✝ == y✝) = true
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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✝ }
neq : ¬(x✝ == y✝) = true
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Tactic:
simp at heq₁ heq₂
State after:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
neq : ¬(x✝ == y✝) = true
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
neq : ¬(x✝ == y✝) = true
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Tactic:
have eq₁ := heq₁.left
State after:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
neq : ¬(x✝ == y✝) = true
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
neq : ¬(x✝ == y✝) = true
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Tactic:
have eq₂ := heq₂.left
State after:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
neq : ¬(x✝ == y✝) = true
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
neq : ¬(x✝ == y✝) = true
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Tactic:
simp at neq
State after:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
neq : ¬x✝ = y✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
neq : ¬x✝ = y✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Tactic:
rw [eq₁, eq₂] at eq
State after:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
eq : x✝ = y✝
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
neq : ¬x✝ = y✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
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
eq : x✝ = y✝
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
neq : ¬x✝ = y✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Tactic:
contradiction
State after:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true

State before:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Tactic:
simp
State after:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ x✝ ≤ y✝

State before:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ x✝ ≤ y✝
Tactic:
rename_i heq₁ heq₂ _ _
State after:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ x✝ ≤ y✝

State before:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ x✝ ≤ y✝
Tactic:
simp at heq₁ heq₂
State after:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
⊢ x✝ ≤ y✝

State before:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
⊢ x✝ ≤ y✝
Tactic:
have eq₁ := Eq.symm heq₁.left
State after:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x✝ = x
⊢ x✝ ≤ y✝

State before:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x✝ = x
⊢ x✝ ≤ y✝
Tactic:
have eq₂ := Eq.symm heq₂.left
State after:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x✝ = x
eq₂ : y✝ = y
⊢ x✝ ≤ y✝

State before:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
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✝) = true
h✝ : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x✝ = x
eq₂ : y✝ = y
⊢ x✝ ≤ y✝
Tactic:
rwa [eq₁, eq₂]
State after:
no goals