Theorem: algebra.lex_add_le_add
Proof state before:
case h_2.inl.h_1
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p₁ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
p₂ : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
p₃ : List.length (z :: zs) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
prop₁ : succ (List.length tail✝) = m
heq✝³ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝² :
  Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ } =
    { val := y✝ :: tail✝, property := prop₁ }
h✝ : x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
property✝ : List.length [] = m
prop₂ : 0 = m
heq✝¹ : { val := x :: xs, property := p₁ } = { val := [], property := property✝ }
heq✝ : { val := y :: ys, property := p₂ } = { val := [], property := prop₂ }
h : True
⊢ Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })

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

case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p₁ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
p₂ : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
p₃ : List.length (z :: zs) = m
h : Order.lex_impl { val := x :: xs, property := p₁ } { val := y :: ys, property := p₂ }
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 := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ :
  Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ } =
    { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
simp [Eq.symm prop₂] at prop₁
Proof state after:
case h_2.inl.h_2
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p₁ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
p₂ : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
p₃ : List.length (z :: zs) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq✝³ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝¹ :: tail✝³, property := property✝³ }
heq✝² :
  Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ } =
    { val := y✝¹ :: tail✝², property := property✝² }
h✝ : x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := p₁ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := p₂ } = { val := y✝ :: tail✝, property := property✝ }
h :
  if x✝ = y✝ then Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
  else x✝ ≤ y✝
⊢ Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })

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