Theorem: algebra.lex_le_trans
Proof state before:
case h_1.h_2.inl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
property✝³ property✝² : List.length [] = m
heq✝³ : { val := x :: xs, property := p } = { val := [], property := property✝³ }
heq✝² : { val := y :: ys, property := q } = { val := [], property := property✝² }
ab : True
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := y :: ys, property := q } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := z :: zs, property := l } = { val := y✝ :: tail✝, property := property✝ }
h✝ : x✝ = y✝
bc : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
⊢ if x = z then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := z :: zs, property := l })
  else x ≤ z

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

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

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

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

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