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

State before:
case h_2.inl.inr.h_2.inl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : x✝ = y✝
bc : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
(first | rename_i heq₁ heq₂ eq₁ neq₁ _ _ _ _ _ _ _ _ heq₃ heq₄ eq₂
         simp at heq₁ heq₂ heq₃ heq₄
         have x_cross_one_eq_x := Eq.symm (heq₁.left)
         have y_cross_one_eq_y := Eq.symm (heq₂.left)
         have x_cross_eq_x     := Eq.symm (heq₃.left)
         have y_cross_eq_x     := Eq.symm (heq₄.left)
         rw [x_cross_eq_x, y_cross_eq_x] at eq₂
         rw [x_cross_one_eq_x, y_cross_one_eq_y] at neq₁
         rw [eq₂] at neq₁
         contradiction
       | split at bc)
State after:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inl.inr.h_2.inl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : x✝ = y✝
bc : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
first | rename_i heq₁ heq₂ eq₁ neq₁ _ _ _ _ _ _ _ _ heq₃ heq₄ eq₂
        simp at heq₁ heq₂ heq₃ heq₄
        have x_cross_one_eq_x := Eq.symm (heq₁.left)
        have y_cross_one_eq_y := Eq.symm (heq₂.left)
        have x_cross_eq_x     := Eq.symm (heq₃.left)
        have y_cross_eq_x     := Eq.symm (heq₄.left)
        rw [x_cross_eq_x, y_cross_eq_x] at eq₂
        rw [x_cross_one_eq_x, y_cross_one_eq_y] at neq₁
        rw [eq₂] at neq₁
        contradiction
      | split at bc
State after:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
rename_i heq₁ heq₂ eq₁ neq₁ _ _ _ _ _ _ _ _ heq₃ heq₄ eq₂
State after:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
eq₁ : x = z
neq₁ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq₄ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
eq₂ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
eq₁ : x = z
neq₁ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq₄ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
eq₂ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
simp at heq₁ heq₂ heq₃ heq₄
State after:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
have x_cross_one_eq_x := Eq.symm (heq₁.left)
State after:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
have y_cross_one_eq_y := Eq.symm (heq₂.left)
State after:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
have x_cross_eq_x     := Eq.symm (heq₃.left)
State after:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
have y_cross_eq_x     := Eq.symm (heq₄.left)
State after:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
rw [x_cross_eq_x, y_cross_eq_x] at eq₂
State after:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq₂ : ¬y = z
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq₂ : ¬y = z
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
rw [x_cross_one_eq_x, y_cross_one_eq_y] at neq₁
State after:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x = y
ab : x✝¹ ≤ y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq₂ : ¬y = z
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inl.inr.h_2.inl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x = y
ab : x✝¹ ≤ y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq₂ : y = z
bc : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
rw [eq₂] at neq₁
State after:
case h_2.inl.inr.h_2.inl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x = z
ab : x✝¹ ≤ y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq₂ : y = z
bc : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inl.inr.h_2.inl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₁ : ¬x = z
ab : x✝¹ ≤ y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq₂ : y = z
bc : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
contradiction
State after:
case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inl.inr.h_2
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝¹ : x = z
h✝ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
bc :
  if x✝ = y✝ then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
  else x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z
Tactic:
split at bc
State after:
case h_2.inl.inr.h_2.inl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : x✝ = y✝
bc : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inl.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
ab :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x✝ ≤ y✝
h✝ : ¬x = z
⊢ x ≤ z

State before:
case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z
Tactic:
(first | simp at *
         rename_i neq₁ eq₁ _ _ _ _ _ _ _ _ eq₂ heq₁ heq₂ heq₃ heq₄
         have x_cross_one_eq_x := Eq.symm (heq₁.left)
         have y_cross_one_eq_y := Eq.symm (heq₂.left)
         have x_cross_eq_x     := Eq.symm (heq₃.left)
         have y_cross_eq_x     := Eq.symm (heq₄.left)
         rw [x_cross_one_eq_x, y_cross_one_eq_y] at eq₁
         rw [x_cross_eq_x, y_cross_eq_x] at bc
         rw [eq₁]
         exact bc
       | split at bc)
State after:
case h_2.inr.inr.h_1
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝ :: tail✝¹, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝² }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := y :: ys, property := q } = { val := [], property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := [], property := property✝ }
bc : True
⊢ x ≤ z

case h_2.inr.inr.h_2
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝¹ : ¬x = z
h✝ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
bc :
  if x✝ = y✝ then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
  else x✝ ≤ y✝
⊢ x ≤ z

State before:
case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z
Tactic:
first | simp at *
        rename_i neq₁ eq₁ _ _ _ _ _ _ _ _ eq₂ heq₁ heq₂ heq₃ heq₄
        have x_cross_one_eq_x := Eq.symm (heq₁.left)
        have y_cross_one_eq_y := Eq.symm (heq₂.left)
        have x_cross_eq_x     := Eq.symm (heq₃.left)
        have y_cross_eq_x     := Eq.symm (heq₄.left)
        rw [x_cross_one_eq_x, y_cross_one_eq_y] at eq₁
        rw [x_cross_eq_x, y_cross_eq_x] at bc
        rw [eq₁]
        exact bc
      | split at bc
State after:
case h_2.inr.inr.h_1
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝ :: tail✝¹, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝² }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := y :: ys, property := q } = { val := [], property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := [], property := property✝ }
bc : True
⊢ x ≤ z

case h_2.inr.inr.h_2
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝¹ : ¬x = z
h✝ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
bc :
  if x✝ = y✝ then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
  else x✝ ≤ y✝
⊢ x ≤ z

State before:
case h_2.inr.inr.h_2
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝¹ : ¬x = z
h✝ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
bc :
  if x✝ = y✝ then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
  else x✝ ≤ y✝
⊢ x ≤ z
Tactic:
rename_i neq₁ eq₁ _ _ _ _ _ _ _ _ eq₂ heq₁ heq₂ heq₃ heq₄
State after:
case h_2.inr.inr.h_2
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝² : List ℕ
property✝¹ : List.length (x✝¹ :: tail✝²) = m
y✝ : ℕ
tail✝¹ : List ℕ
neq₁ : List.length (y✝ :: tail✝¹) = m
eq₁ : { val := x :: xs, property := p } = { val := x✝¹ :: tail✝², property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝¹, property := neq₁ }
h✝¹ : ¬x = z
h✝ : ¬x✝¹ = y✝
ab : x✝¹ ≤ y✝
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (x✝ :: tail✝) = m
eq₂ : ℕ
heq₁ : List ℕ
heq₂ : List.length (eq₂ :: heq₁) = m
heq₃ : { val := y :: ys, property := q } = { val := x✝ :: tail✝, property := property✝ }
heq₄ : { val := z :: zs, property := l } = { val := eq₂ :: heq₁, property := heq₂ }
bc :
  if x✝ = eq₂ then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
  else x✝ ≤ eq₂
⊢ x ≤ z

State before:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x✝¹ = y✝¹
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z
Tactic:
have x_cross_one_eq_x := Eq.symm (heq₁.left)
State after:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x✝¹ = y✝¹
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z

State before:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x✝¹ = y✝¹
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z
Tactic:
have y_cross_one_eq_y := Eq.symm (heq₂.left)
State after:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x✝¹ = y✝¹
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z

State before:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x✝¹ = y✝¹
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z
Tactic:
have x_cross_eq_x     := Eq.symm (heq₃.left)
State after:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x✝¹ = y✝¹
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z

State before:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x✝¹ = y✝¹
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z
Tactic:
have y_cross_eq_x     := Eq.symm (heq₄.left)
State after:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x✝¹ = y✝¹
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z

State before:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x✝¹ = y✝¹
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z
Tactic:
rw [x_cross_one_eq_x, y_cross_one_eq_y] at eq₁
State after:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z

State before:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z
Tactic:
rw [x_cross_eq_x, y_cross_eq_x] at bc
State after:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : y ≤ z
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z

State before:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : y ≤ z
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ x ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z
Tactic:
rw [eq₁]
State after:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : y ≤ z
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ y ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z

State before:
case h_2.inr.inl.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
eq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
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✝
bc : y ≤ z
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ y ≤ z

case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z
Tactic:
exact bc
State after:
case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z

State before:
case h_2.inr.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
bc :
  match { val := y :: ys, property := q }, { val := z :: zs, property := l } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x = y_1 then
      Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := z :: zs, property := l })
    else x ≤ 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 := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
⊢ x ≤ z
Tactic:
split at bc
State after:
case h_2.inr.inr.h_1
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝ :: tail✝¹, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝ :: tail✝, property := property✝² }
h✝¹ : ¬x = z
h✝ : ¬x✝ = y✝
ab : x✝ ≤ y✝
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := y :: ys, property := q } = { val := [], property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := [], property := property✝ }
bc : True
⊢ x ≤ z

case h_2.inr.inr.h_2
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝¹ : ¬x = z
h✝ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
bc :
  if x✝ = y✝ then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
  else x✝ ≤ y✝
⊢ x ≤ z

State before:
case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 := p } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := y✝¹ :: tail✝², property := property✝² }
h✝² : ¬x = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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 := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
⊢ x ≤ z
Tactic:
simp at *
State after:
case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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✝
bc : x✝ ≤ y✝
heq✝³ : x = x✝¹ ∧ xs = tail✝³
heq✝² : y = y✝¹ ∧ ys = tail✝²
heq✝¹ : y = x✝ ∧ ys = tail✝¹
heq✝ : z = y✝ ∧ zs = tail✝
⊢ x ≤ z

State before:
case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
h✝¹ : ¬x✝¹ = y✝¹
ab : 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✝
bc : x✝ ≤ y✝
heq✝³ : x = x✝¹ ∧ xs = tail✝³
heq✝² : y = y✝¹ ∧ ys = tail✝²
heq✝¹ : y = x✝ ∧ ys = tail✝¹
heq✝ : z = y✝ ∧ zs = tail✝
⊢ x ≤ z
Tactic:
rename_i neq₁ neq₂ _ _ _ _ _ _ _ _ _ heq₁ heq₂ heq₃ heq₄
State after:
case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₂ : ¬x✝¹ = y✝¹
ab : 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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
⊢ x ≤ z

State before:
case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₂ : ¬x✝¹ = y✝¹
ab : 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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
⊢ x ≤ z
Tactic:
have x_cross_one_eq_x := Eq.symm (heq₁.left)
State after:
case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₂ : ¬x✝¹ = y✝¹
ab : 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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
⊢ x ≤ z

State before:
case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₂ : ¬x✝¹ = y✝¹
ab : 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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
⊢ x ≤ z
Tactic:
have y_cross_one_eq_y := Eq.symm (heq₂.left)
State after:
case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₂ : ¬x✝¹ = y✝¹
ab : 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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
⊢ x ≤ z

State before:
case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₂ : ¬x✝¹ = y✝¹
ab : 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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
⊢ x ≤ z
Tactic:
have x_cross_eq_x     := Eq.symm (heq₃.left)
State after:
case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₂ : ¬x✝¹ = y✝¹
ab : 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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
⊢ x ≤ z

State before:
case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₂ : ¬x✝¹ = y✝¹
ab : 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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
⊢ x ≤ z
Tactic:
have y_cross_eq_x     := Eq.symm (heq₄.left)
State after:
case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = 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 = z
neq₂ : ¬x✝¹ = y✝¹
ab : 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✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ x ≤ z