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

State before:
n : ℕ
⊢ ∀ (a b : Variables n order.Lex), Order.lex a b ∨ Order.lex b a
Tactic:
intros v₁ v₂
State after:
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∨ Order.lex v₂ v₁

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∨ Order.lex v₂ v₁
Tactic:
exact aux n v₁ v₂
State after:
no goals

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
⊢ Order.lex_impl a b ∨ Order.lex_impl b a
Tactic:
match a, b with
  | ⟨[], p⟩, ⟨[], q⟩       => rw [Order.lex_impl]
                              split
                              simp
                              simp at *
  | ⟨x::xs, p⟩, ⟨y::ys, q⟩ => rw [Order.lex_impl]
                              simp [Or.comm]
                              rw [Order.lex_impl]
                              split
                              simp
                              split
                              split
                              simp [Or.comm]
                              apply aux (m-1) (tail ⟨x::xs, p⟩) (tail ⟨y::ys, q⟩)
                              simp at *
                              rename_i eq neq heq₁ heq₂
                              have s_eq := Eq.symm eq
                              have eq_1 := Eq.symm heq₁.left
                              have eq_2 := Eq.symm heq₂.left
                              rw [eq_1, eq_2] at s_eq
                              contradiction
                              split
                              simp at *
                              rename_i neq eq heq₁ heq₂
                              have s_eq := Eq.symm eq
                              have eq_1 := heq₁.left
                              have eq_2 := heq₂.left
                              rw [eq_1, eq_2] at s_eq
                              contradiction
                              simp at *
                              rename_i heq₁ heq₂
                              have eq_1 := heq₁.left
                              have eq_2 := heq₂.left
                              rw [eq_1, eq_2]
                              simp [Nat.le_total]
State after:
no goals

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
p q : List.length [] = m
⊢ Order.lex_impl { val := [], property := p } { val := [], property := q } ∨
    Order.lex_impl { val := [], property := q } { val := [], property := p }
Tactic:
rw [Order.lex_impl]
State after:
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
p q : List.length [] = m
⊢ (match { val := [], property := p }, { val := [], property := q } with
    | { val := [], property := property }, { val := [], property := property_1 } => True
    | { val := x :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
      if x = y then Order.lex_impl (Vector.tail { val := [], property := p }) (Vector.tail { val := [], property := q })
      else x ≤ y) ∨
    match { val := [], property := p }, { val := [], property := q } with
    | { val := [], property := property }, { val := [], property := property_1 } => True
    | { val := x :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
      if x = y then Order.lex_impl (Vector.tail { val := [], property := p }) (Vector.tail { val := [], property := q })
      else x ≤ y

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
p q : List.length [] = m
⊢ (match { val := [], property := p }, { val := [], property := q } with
    | { val := [], property := property }, { val := [], property := property_1 } => True
    | { val := x :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
      if x = y then Order.lex_impl (Vector.tail { val := [], property := p }) (Vector.tail { val := [], property := q })
      else x ≤ y) ∨
    match { val := [], property := p }, { val := [], property := q } with
    | { val := [], property := property }, { val := [], property := property_1 } => True
    | { val := x :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
      if x = y then Order.lex_impl (Vector.tail { val := [], property := p }) (Vector.tail { val := [], property := q })
      else x ≤ y
Tactic:
split
State after:
case h_1
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
p q : List.length [] = m
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := [], property := p } = { val := [], property := property✝¹ }
heq✝ : { val := [], property := q } = { val := [], property := property✝ }
⊢ True ∨ True

case h_2
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
p q : List.length [] = 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 := [], property := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := [], property := q } = { val := y✝ :: tail✝, property := property✝ }
⊢ (if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := q })
    else x✝ ≤ y✝) ∨
    if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := q }) else x✝ ≤ y✝

State before:
case h_1
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
p q : List.length [] = m
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := [], property := p } = { val := [], property := property✝¹ }
heq✝ : { val := [], property := q } = { val := [], property := property✝ }
⊢ True ∨ True

case h_2
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
p q : List.length [] = 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 := [], property := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := [], property := q } = { val := y✝ :: tail✝, property := property✝ }
⊢ (if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := q })
    else x✝ ≤ y✝) ∨
    if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := q }) else x✝ ≤ y✝
Tactic:
simp
State after:
case h_2
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
p q : List.length [] = 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 := [], property := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := [], property := q } = { val := y✝ :: tail✝, property := property✝ }
⊢ (if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := q })
    else x✝ ≤ y✝) ∨
    if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := q }) else x✝ ≤ y✝

State before:
case h_2
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
p q : List.length [] = 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 := [], property := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := [], property := q } = { val := y✝ :: tail✝, property := property✝ }
⊢ (if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := q })
    else x✝ ≤ y✝) ∨
    if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := q }) else x✝ ≤ y✝
Tactic:
simp at *
State after:
no goals

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
⊢ Order.lex_impl { val := x :: xs, property := p } { val := y :: ys, property := q } ∨
    Order.lex_impl { val := y :: ys, property := q } { val := x :: xs, property := p }
Tactic:
rw [Order.lex_impl]
State after:
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
⊢ (match { val := x :: xs, property := p }, { val := y :: ys, property := q } with
    | { val := [], property := property }, { val := [], property := property_1 } => True
    | { val := x_1 :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
      if x_1 = y_1 then
        Order.lex_impl (Vector.tail { val := x :: xs, property := p }) (Vector.tail { val := y :: ys, property := q })
      else x_1 ≤ y_1) ∨
    Order.lex_impl { val := y :: ys, property := q } { val := x :: xs, property := p }

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
⊢ (match { val := x :: xs, property := p }, { val := y :: ys, property := q } with
    | { val := [], property := property }, { val := [], property := property_1 } => True
    | { val := x_1 :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
      if x_1 = y_1 then
        Order.lex_impl (Vector.tail { val := x :: xs, property := p }) (Vector.tail { val := y :: ys, property := q })
      else x_1 ≤ y_1) ∨
    Order.lex_impl { val := y :: ys, property := q } { val := x :: xs, property := p }
Tactic:
simp [Or.comm]
State after:
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
⊢ Order.lex_impl { val := y :: ys, property := q } { val := x :: xs, property := p } ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
⊢ Order.lex_impl { val := y :: ys, property := q } { val := x :: xs, property := p } ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
rw [Order.lex_impl]
State after:
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
⊢ (match { val := y :: ys, property := q }, { val := x :: xs, property := p } with
    | { val := [], property := property }, { val := [], property := property_1 } => True
    | { val := x_1 :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
      if x_1 = y_1 then
        Order.lex_impl (Vector.tail { val := y :: ys, property := q }) (Vector.tail { val := x :: xs, property := p })
      else x_1 ≤ y_1) ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

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

case h_2
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
⊢ (if x✝ = y✝ then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
    else x✝ ≤ y✝) ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
case h_1
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := y :: ys, property := q } = { val := [], property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := [], property := property✝ }
⊢ True ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

case h_2
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
⊢ (if x✝ = y✝ then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
    else x✝ ≤ y✝) ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
simp
State after:
case h_2
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
⊢ (if x✝ = y✝ then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
    else x✝ ≤ y✝) ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

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

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
case h_2.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : x✝ = y✝
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
split
State after:
case h_2.inl.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : x = y
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨
    Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : ¬x = y
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
case h_2.inl.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : x = y
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨
    Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : ¬x = y
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
simp [Or.comm]
State after:
case h_2.inl.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : x = y
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q }) ∨
    Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })

case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : ¬x = y
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
case h_2.inl.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : x = y
⊢ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q }) ∨
    Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })

case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : ¬x = y
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
apply aux (m-1) (tail ⟨x::xs, p⟩) (tail ⟨y::ys, q⟩)
State after:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : ¬x = y
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : ¬x = y
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
simp at *
State after:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : x✝ = y✝
h✝ : ¬x = y
heq✝¹ : y = x✝ ∧ ys = tail✝¹
heq✝ : x = y✝ ∧ xs = tail✝
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : x✝ = y✝
h✝ : ¬x = y
heq✝¹ : y = x✝ ∧ ys = tail✝¹
heq✝ : x = y✝ ∧ xs = tail✝
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
rename_i eq neq heq₁ heq₂
State after:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
neq : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
neq : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
have s_eq := Eq.symm eq
State after:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
neq : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : y✝ = x✝
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
neq : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : y✝ = x✝
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
have eq_1 := Eq.symm heq₁.left
State after:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
neq : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : y✝ = x✝
eq_1 : x✝ = y
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
neq : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : y✝ = x✝
eq_1 : x✝ = y
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
have eq_2 := Eq.symm heq₂.left
State after:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
neq : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : y✝ = x✝
eq_1 : x✝ = y
eq_2 : y✝ = x
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
neq : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : y✝ = x✝
eq_1 : x✝ = y
eq_2 : y✝ = x
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
rw [eq_1, eq_2] at s_eq
State after:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
neq : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : x = y
eq_1 : x✝ = y
eq_2 : y✝ = x
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
case h_2.inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
neq : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : x = y
eq_1 : x✝ = y
eq_2 : y✝ = x
⊢ Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p }) ∨ x ≤ y

case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
contradiction
State after:
case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y

State before:
case h_2.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝ ∨
    if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
    else x ≤ y
Tactic:
split
State after:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : x = y
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y

State before:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : x = y
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

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

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y

State before:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬x✝ = y✝
h✝ : x = y
heq✝¹ : y = x✝ ∧ ys = tail✝¹
heq✝ : x = y✝ ∧ xs = tail✝
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y
Tactic:
rename_i neq eq heq₁ heq₂
State after:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
eq : x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y

State before:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
eq : x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y
Tactic:
have s_eq := Eq.symm eq
State after:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
eq : x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : y = x
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y

State before:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
eq : x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : y = x
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y
Tactic:
have eq_1 := heq₁.left
State after:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
eq : x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : y = x
eq_1 : y = x✝
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y

State before:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
eq : x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : y = x
eq_1 : y = x✝
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y
Tactic:
have eq_2 := heq₂.left
State after:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
eq : x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : y = x
eq_1 : y = x✝
eq_2 : x = y✝
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y

State before:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
eq : x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : y = x
eq_1 : y = x✝
eq_2 : x = y✝
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y
Tactic:
rw [eq_1, eq_2] at s_eq
State after:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
eq : x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : x✝ = y✝
eq_1 : y = x✝
eq_2 : x = y✝
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y

State before:
case h_2.inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
eq : x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
s_eq : x✝ = y✝
eq_1 : y = x✝
eq_2 : x = y✝
⊢ x✝ ≤ y✝ ∨ Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })

case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y
Tactic:
contradiction
State after:
case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y

State before:
case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := p } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
⊢ x✝ ≤ y✝ ∨ x ≤ y
Tactic:
simp at *
State after:
case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
heq✝¹ : y = x✝ ∧ ys = tail✝¹
heq✝ : x = y✝ ∧ xs = tail✝
⊢ x✝ ≤ y✝ ∨ x ≤ y

State before:
case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
heq✝¹ : y = x✝ ∧ ys = tail✝¹
heq✝ : x = y✝ ∧ xs = tail✝
⊢ x✝ ≤ y✝ ∨ x ≤ y
Tactic:
rename_i heq₁ heq₂
State after:
case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
⊢ x✝ ≤ y✝ ∨ x ≤ y

State before:
case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
⊢ x✝ ≤ y✝ ∨ x ≤ y
Tactic:
have eq_1 := heq₁.left
State after:
case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
eq_1 : y = x✝
⊢ x✝ ≤ y✝ ∨ x ≤ y

State before:
case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
eq_1 : y = x✝
⊢ x✝ ≤ y✝ ∨ x ≤ y
Tactic:
have eq_2 := heq₂.left
State after:
case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
eq_1 : y = x✝
eq_2 : x = y✝
⊢ x✝ ≤ y✝ ∨ x ≤ y

State before:
case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
eq_1 : y = x✝
eq_2 : x = y✝
⊢ x✝ ≤ y✝ ∨ x ≤ y
Tactic:
rw [eq_1, eq_2]
State after:
case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
eq_1 : y = x✝
eq_2 : x = y✝
⊢ x✝ ≤ y✝ ∨ y✝ ≤ x✝

State before:
case h_2.inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬x✝ = y✝
h✝ : ¬x = y
heq₁ : y = x✝ ∧ ys = tail✝¹
heq₂ : x = y✝ ∧ xs = tail✝
eq_1 : y = x✝
eq_2 : x = y✝
⊢ x✝ ≤ y✝ ∨ y✝ ≤ x✝
Tactic:
simp [Nat.le_total]
State after:
no goals