internlm/Lean-Github huggingface dataset:
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
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
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✝
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
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
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
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✝
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
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
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
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✝
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
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
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
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✝
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
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
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
Proof 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
Theorem: algebra.lex_le_total
Proof 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 *
Proof 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
Theorem: algebra.lex_le_total
Proof 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₂
Proof 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
Theorem: algebra.lex_le_total
Proof 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
Proof 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
Theorem: algebra.lex_le_total
Proof 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
Proof 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
Theorem: algebra.lex_le_total
Proof 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]
Proof 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✝
Theorem: algebra.lex_le_total
Proof 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]
Proof state after:
no goals
Theorem: algebra.lex_lt_iff_le_not_le
Proof state before:
n : ℕ
⊢ ∀ (a b : Variables n order.Lex), Order.lex_lt a b ↔ Order.lex a b ∧ ¬Order.lex b a
Tactic:
intros v₁ v₂
Proof state after:
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex_lt v₁ v₂ ↔ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁
Theorem: algebra.lex_lt_iff_le_not_le
Proof state before:
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex_lt v₁ v₂ ↔ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁
Tactic:
apply Iff.intro
Proof state after:
case mp
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex_lt v₁ v₂ → Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁

case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex_lt v₁ v₂
Theorem: algebra.lex_lt_iff_le_not_le
Proof state before:
case mp
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex_lt v₁ v₂ → Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁

case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex_lt v₁ v₂
Tactic:
repeat (
  rw [Order.lex_lt]
  simp
)
Proof state after:
no goals
Theorem: algebra.lex_lt_iff_le_not_le
Proof state before:
case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex_lt v₁ v₂
Tactic:
(
rw [Order.lex_lt]
simp
)
Proof state after:
no goals
Theorem: algebra.lex_lt_iff_le_not_le
Proof state before:
case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex_lt v₁ v₂
Tactic:
rw [Order.lex_lt]
Proof state after:
case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁
Theorem: algebra.lex_lt_iff_le_not_le
Proof state before:
case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁
Tactic:
simp
Proof state after:
no goals
Theorem: algebra.lex_add_le_add
Proof state before:
n : ℕ
⊢ ∀ (a b c : Variables n order.Lex), Order.lex a b → Order.lex (Variables.mul a c) (Variables.mul b c)
Tactic:
intros v₁ v₂ v₃
Proof state after:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
⊢ Order.lex v₁ v₂ → Order.lex (Variables.mul v₁ v₃) (Variables.mul v₂ v₃)
Theorem: algebra.lex_add_le_add
Proof state before:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
⊢ Order.lex v₁ v₂ → Order.lex (Variables.mul v₁ v₃) (Variables.mul v₂ v₃)
Tactic:
apply aux n v₁ v₂ v₃
Proof state after:
no goals
Theorem: algebra.lex_add_le_add
Proof state before:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
⊢ Order.lex_impl a b → Order.lex_impl (Variables.mul a c) (Variables.mul b c)
Tactic:
intros h
Proof state after:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
h : Order.lex_impl a b
⊢ Order.lex_impl (Variables.mul a c) (Variables.mul b c)
Theorem: algebra.lex_add_le_add
Proof state before:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
property✝² property✝¹ property✝ : List.length [] = m
h : Order.lex_impl { val := [], property := property✝² } { val := [], property := property✝¹ }
⊢ Order.lex_impl (Variables.mul { val := [], property := property✝² } { val := [], property := property✝ })
    (Variables.mul { val := [], property := property✝¹ } { val := [], property := property✝ })
Tactic:
rw [Order.lex_impl]
Proof state after:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
property✝² property✝¹ property✝ : List.length [] = m
h : Order.lex_impl { val := [], property := property✝² } { val := [], property := property✝¹ }
⊢ match Variables.mul { val := [], property := property✝² } { val := [], property := property✝ },
    Variables.mul { val := [], property := property✝¹ } { val := [], property := property✝ } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
    if x = y then
      Order.lex_impl
        (Vector.tail (Variables.mul { val := [], property := property✝² } { val := [], property := property✝ }))
        (Vector.tail (Variables.mul { val := [], property := property✝¹ } { val := [], property := property✝ }))
    else x ≤ y
Theorem: algebra.lex_add_le_add
Proof state before:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
property✝² property✝¹ property✝ : List.length [] = m
h : Order.lex_impl { val := [], property := property✝² } { val := [], property := property✝¹ }
⊢ match Variables.mul { val := [], property := property✝² } { val := [], property := property✝ },
    Variables.mul { val := [], property := property✝¹ } { val := [], property := property✝ } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
    if x = y then
      Order.lex_impl
        (Vector.tail (Variables.mul { val := [], property := property✝² } { val := [], property := property✝ }))
        (Vector.tail (Variables.mul { val := [], property := property✝¹ } { val := [], property := property✝ }))
    else x ≤ y
Tactic:
split
Proof state after:
case h_1
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
property✝⁴ property✝³ property✝² : List.length [] = m
h : Order.lex_impl { val := [], property := property✝⁴ } { val := [], property := property✝³ }
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ :
  Variables.mul { val := [], property := property✝⁴ } { val := [], property := property✝² } =
    { val := [], property := property✝¹ }
heq✝ :
  Variables.mul { val := [], property := property✝³ } { val := [], property := property✝² } =
    { val := [], property := property✝ }
⊢ True

case h_2
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
property✝⁴ property✝³ property✝² : List.length [] = m
h : Order.lex_impl { val := [], property := property✝⁴ } { val := [], property := property✝³ }
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ :
  Variables.mul { val := [], property := property✝⁴ } { val := [], property := property✝² } =
    { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ :
  Variables.mul { val := [], property := property✝³ } { val := [], property := property✝² } =
    { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then
    Order.lex_impl (tail (Variables.mul { val := [], property := property✝⁴ } { val := [], property := property✝² }))
      (tail (Variables.mul { val := [], property := property✝³ } { val := [], property := property✝² }))
  else x✝ ≤ y✝