internlm/Lean-Github huggingface dataset:
Theorem: algebra.lex_le_total
Proof 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 *
Proof 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
Theorem: algebra.lex_le_total
Proof 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₂
Proof 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
Theorem: algebra.lex_le_total
Proof 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
Proof 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
Theorem: algebra.lex_le_total
Proof 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
Proof 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
Theorem: algebra.lex_le_total
Proof 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
Proof 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
Theorem: algebra.lex_le_total
Proof 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
Proof 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
Theorem: algebra.lex_le_total
Proof 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
Proof 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
Theorem: algebra.lex_le_total
Proof 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
Proof 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
Theorem: algebra.lex_le_total
Proof 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 *
Proof 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
Theorem: algebra.lex_le_total
Proof 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₂
Proof 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