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

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₃
State after:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
⊢ Order.lex v₁ v₂ → Order.lex (Variables.mul v₁ v₃) (Variables.mul v₂ v₃)

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₃
State after:
no goals

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
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)

State before:
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)
Tactic:
match a, b, c with
 | ⟨[], _⟩, ⟨[], _⟩, ⟨[], _⟩          => rw [Order.lex_impl]
                                         split
                                         simp
                                         split
                                         repeat (rename_i prop₁ _ _ _ _ _ _ _ _ _ prop₄ _ _ _
                                                 simp at prop₁ prop₄
                                                 simp [Eq.symm prop₁] at prop₄)                                                                                  
 | ⟨x::xs, p₁⟩, ⟨y::ys, p₂⟩, ⟨z::zs, p₃⟩ => rw [Order.lex_impl]
                                            split
                                            simp
                                            split
                                            apply aux (m-1) (tail ⟨x::xs, p₁⟩) (tail ⟨y::ys, p₂⟩) (tail ⟨z::zs, p₃⟩)
                                            rw [Order.lex_impl] at h
                                            split at h
                                            rename_i prop₁ _ _ _ _ _ _ prop₂ _ _
                                            simp at prop₁ prop₂
                                            simp [Eq.symm prop₂] at prop₁
                                            split at h
                                            exact h
                                            simp at *
                                            rename_i var_mul₁ var_mul₂ _ _ _ _ _ _ _ _ eq neq heq₁ heq₂
                                            simp [map₂, Variables.mul, List.zipWith] at var_mul₁ var_mul₂
                                            have eq₁ := heq₁.left 
                                            have eq₂ := heq₂.left
                                            cases var_mul₁
                                            cases var_mul₂
                                            rename_i sum_eq _
                                            simp [eq₁, eq₂] at sum_eq
                                            contradiction
                                            rw [Order.lex_impl] at h
                                            split at h
                                            simp at *
                                            split at h
                                            rename_i var_mul₁ var_mul₂ _ _ _ _ _ _ _ _ _ heq₁ heq₂ eq
                                            simp [map₂, Variables.mul, List.zipWith] at var_mul₁ var_mul₂
                                            cases heq₁
                                            cases heq₂
                                            cases var_mul₁
                                            cases var_mul₂
                                            simp [eq]
                                            rename_i var_mul₁ var_mul₂ _ _ _ _ _ _ _ _ _ heq₁ heq₂ eq
                                            cases heq₁
                                            cases heq₂
                                            simp [map₂, Variables.mul, List.zipWith] at var_mul₁ var_mul₂
                                            cases var_mul₁ 
                                            cases var_mul₂
                                            simp at *
                                            exact h
State after:
no goals

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]
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

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
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✝

State before:
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✝
Tactic:
simp
State after:
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✝

State before:
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✝
Tactic:
split
State after:
case h_2.inl
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✝ }
h✝ : x✝ = y✝
⊢ Order.lex_impl (tail (Variables.mul { val := [], property := property✝⁴ } { val := [], property := property✝² }))
    (tail (Variables.mul { val := [], property := property✝³ } { val := [], property := property✝² }))

case h_2.inr
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✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inl
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✝ }
h✝ : x✝ = y✝
⊢ Order.lex_impl (tail (Variables.mul { val := [], property := property✝⁴ } { val := [], property := property✝² }))
    (tail (Variables.mul { val := [], property := property✝³ } { val := [], property := property✝² }))

case h_2.inr
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✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
repeat (rename_i prop₁ _ _ _ _ _ _ _ _ _ prop₄ _ _ _
        simp at prop₁ prop₄
        simp [Eq.symm prop₁] at prop₄)
State after:
no goals

State before:
case h_2.inr
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✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
(rename_i prop₁ _ _ _ _ _ _ _ _ _ prop₄ _ _ _
 simp at prop₁ prop₄
 simp [Eq.symm prop₁] at prop₄)
State after:
no goals

State before:
case h_2.inr
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✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
rename_i prop₁ _ _ _ _ _ _ _ _ _ prop₄ _ _ _
State after:
case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
prop₁ property✝² property✝¹ : List.length [] = m
h : Order.lex_impl { val := [], property := prop₁ } { val := [], property := property✝² }
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
prop₄ : List.length (y✝ :: tail✝) = m
heq✝¹ :
  Variables.mul { val := [], property := prop₁ } { val := [], property := property✝¹ } =
    { val := x✝ :: tail✝¹, property := property✝ }
heq✝ :
  Variables.mul { val := [], property := property✝² } { val := [], property := property✝¹ } =
    { val := y✝ :: tail✝, property := prop₄ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
prop₁ property✝² property✝¹ : List.length [] = m
h : Order.lex_impl { val := [], property := prop₁ } { val := [], property := property✝² }
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
prop₄ : List.length (y✝ :: tail✝) = m
heq✝¹ :
  Variables.mul { val := [], property := prop₁ } { val := [], property := property✝¹ } =
    { val := x✝ :: tail✝¹, property := property✝ }
heq✝ :
  Variables.mul { val := [], property := property✝² } { val := [], property := property✝¹ } =
    { val := y✝ :: tail✝, property := prop₄ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
simp at prop₁ prop₄
State after:
case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
prop₁ : 0 = m
property✝² property✝¹ : List.length [] = m
h : Order.lex_impl { val := [], property := prop₁ } { val := [], property := property✝² }
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 := [], property := prop₁ } { val := [], property := property✝¹ } =
    { val := x✝ :: tail✝¹, property := property✝ }
heq✝ :
  Variables.mul { val := [], property := property✝² } { val := [], property := property✝¹ } =
    { val := y✝ :: tail✝, property := prop₄ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝

State before:
case h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
prop₁ : 0 = m
property✝² property✝¹ : List.length [] = m
h : Order.lex_impl { val := [], property := prop₁ } { val := [], property := property✝² }
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 := [], property := prop₁ } { val := [], property := property✝¹ } =
    { val := x✝ :: tail✝¹, property := property✝ }
heq✝ :
  Variables.mul { val := [], property := property✝² } { val := [], property := property✝¹ } =
    { val := y✝ :: tail✝, property := prop₄ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
simp [Eq.symm prop₁] at prop₄
State after:
no goals

State before:
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₂ }
⊢ Order.lex_impl (Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ })
    (Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ })
Tactic:
rw [Order.lex_impl]
State after:
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₂ }
⊢ match Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ },
    Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, 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 (Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ }))
        (Vector.tail (Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ }))
    else x_1 ≤ y_1

State before:
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₂ }
⊢ match Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ },
    Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, 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 (Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ }))
        (Vector.tail (Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ }))
    else x_1 ≤ y_1
Tactic:
split
State after:
case 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
h : Order.lex_impl { val := x :: xs, property := p₁ } { val := y :: ys, property := p₂ }
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := [], property := property✝¹ }
heq✝ :
  Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ } =
    { val := [], property := property✝ }
⊢ True

case 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
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✝ }
⊢ if x✝ = y✝ then
    Order.lex_impl (tail (Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ }))
      (tail (Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ }))
  else x✝ ≤ y✝

State before:
case 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
h : Order.lex_impl { val := x :: xs, property := p₁ } { val := y :: ys, property := p₂ }
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := [], property := property✝¹ }
heq✝ :
  Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ } =
    { val := [], property := property✝ }
⊢ True

case 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
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✝ }
⊢ if x✝ = y✝ then
    Order.lex_impl (tail (Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ }))
      (tail (Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ }))
  else x✝ ≤ y✝
Tactic:
simp
State after:
case 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
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✝ }
⊢ if x✝ = y✝ then
    Order.lex_impl (tail (Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ }))
      (tail (Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ }))
  else x✝ ≤ y✝

State before:
case 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
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✝ }
⊢ if x✝ = y✝ then
    Order.lex_impl (tail (Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ }))
      (tail (Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ }))
  else x✝ ≤ y✝
Tactic:
split
State after:
case h_2.inl
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✝
⊢ Order.lex_impl (tail (Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ }))
    (tail (Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, 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✝

State before:
case h_2.inl
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✝
⊢ Order.lex_impl (tail (Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ }))
    (tail (Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, 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:
apply aux (m-1) (tail ⟨x::xs, p₁⟩) (tail ⟨y::ys, p₂⟩) (tail ⟨z::zs, p₃⟩)
State after:
case h_2.inl
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✝
⊢ 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✝

State before:
case h_2.inl
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✝
⊢ 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:
rw [Order.lex_impl] at h
State after:
case h_2.inl
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 :
  match { val := x :: xs, property := p₁ }, { val := y :: ys, 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 := x :: xs, property := p₁ }) (Vector.tail { val := y :: ys, property := p₂ })
    else x_1 ≤ 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✝¹ :
  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✝
⊢ 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✝

State before:
case h_2.inl
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 :
  match { val := x :: xs, property := p₁ }, { val := y :: ys, 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 := x :: xs, property := p₁ }) (Vector.tail { val := y :: ys, property := p₂ })
    else x_1 ≤ 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✝¹ :
  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✝
⊢ 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:
split at h
State after:
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 ℕ
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
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := x :: xs, property := p₁ } = { val := [], property := property✝¹ }
heq✝ : { val := y :: ys, property := p₂ } = { val := [], property := property✝ }
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✝

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 ℕ
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
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := x :: xs, property := p₁ } = { val := [], property := property✝¹ }
heq✝ : { val := y :: ys, property := p₂ } = { val := [], property := property✝ }
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:
rename_i prop₁ _ _ _ _ _ _ prop₂ _ _
State after:
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₁ : 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 := prop₁ }
h✝ : x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
property✝ prop₂ : List.length [] = 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✝

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₁ : 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 := prop₁ }
h✝ : x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
property✝ prop₂ : List.length [] = 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 at prop₁ prop₂
State after:
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✝

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₁
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✝

State before:
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:
split at h
State after:
case h_2.inl.h_2.inl
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✝ : x✝ = y✝
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
⊢ Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })

case h_2.inl.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
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✝ : ¬x✝ = y✝
h : 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✝

State before:
case h_2.inl.h_2.inl
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✝ : x✝ = y✝
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
⊢ Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })

case h_2.inl.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
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✝ : ¬x✝ = y✝
h : 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:
exact h
State after:
case h_2.inl.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
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✝ : ¬x✝ = y✝
h : 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✝

State before:
case h_2.inl.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
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✝ : ¬x✝ = y✝
h : 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 at *
State after:
case h_2.inl.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
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
h✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
heq✝¹ : x = x✝ ∧ xs = tail✝¹
heq✝ : y = y✝ ∧ ys = tail✝
⊢ 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✝

State before:
case h_2.inl.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
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
h✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
heq✝¹ : x = x✝ ∧ xs = tail✝¹
heq✝ : y = y✝ ∧ ys = tail✝
⊢ 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:
rename_i var_mul₁ var_mul₂ _ _ _ _ _ _ _ _ eq neq heq₁ heq₂
State after:
case h_2.inl.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
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝² : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝¹ : List.length (y✝¹ :: tail✝²) = m
var_mul₁ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝¹ :: tail✝³, property := property✝² }
var_mul₂ :
  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 ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
⊢ 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✝

State before:
case h_2.inl.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
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝² : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝¹ : List.length (y✝¹ :: tail✝²) = m
var_mul₁ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝¹ :: tail✝³, property := property✝² }
var_mul₂ :
  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 ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
⊢ 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 [map₂, Variables.mul, List.zipWith] at var_mul₁ var_mul₂
State after:
case h_2.inl.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
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝² : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝¹ : List.length (y✝¹ :: tail✝²) = m
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝¹ :: tail✝³, property := property✝² }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝¹ :: tail✝², property := property✝¹ }
h✝ : x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
⊢ 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✝

State before:
case h_2.inl.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
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝² : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝¹ : List.length (y✝¹ :: tail✝²) = m
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝¹ :: tail✝³, property := property✝² }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝¹ :: tail✝², property := property✝¹ }
h✝ : x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
⊢ 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:
have eq₁ := heq₁.left
State after:
case h_2.inl.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
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝² : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝¹ : List.length (y✝¹ :: tail✝²) = m
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝¹ :: tail✝³, property := property✝² }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝¹ :: tail✝², property := property✝¹ }
h✝ : x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
⊢ 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✝

State before:
case h_2.inl.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
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝² : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝¹ : List.length (y✝¹ :: tail✝²) = m
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝¹ :: tail✝³, property := property✝² }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝¹ :: tail✝², property := property✝¹ }
h✝ : x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
⊢ 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:
have eq₂ := heq₂.left
State after:
case h_2.inl.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
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝² : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝¹ : List.length (y✝¹ :: tail✝²) = m
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝¹ :: tail✝³, property := property✝² }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝¹ :: tail✝², property := property✝¹ }
h✝ : x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = 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✝

State before:
case h_2.inl.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
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝² : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝¹ : List.length (y✝¹ :: tail✝²) = m
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝¹ :: tail✝³, property := property✝² }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝¹ :: tail✝², property := property✝¹ }
h✝ : x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = 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:
cases var_mul₁
State after:
case h_2.inl.h_2.inr.refl
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
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝¹ :: tail✝², property := property✝² }
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
h✝ : x + z = y✝¹
property✝ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
⊢ 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✝

State before:
case h_2.inl.h_2.inr.refl
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
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝¹ :: tail✝², property := property✝² }
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
h✝ : x + z = y✝¹
property✝ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
⊢ 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:
cases var_mul₂
State after:
case h_2.inl.h_2.inr.refl.refl
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₂✝¹ v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝² : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
property✝¹ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
h✝ : x + z = y + z
property✝ : List.length ((y + z) :: List.zipWith (fun x y => x + y) ys zs) = m
⊢ 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✝

State before:
case h_2.inl.h_2.inr.refl.refl
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₂✝¹ v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝² : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
property✝¹ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
h✝ : x + z = y + z
property✝ : List.length ((y + z) :: List.zipWith (fun x y => x + y) ys zs) = m
⊢ 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:
rename_i sum_eq _
State after:
case h_2.inl.h_2.inr.refl.refl
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₂✝¹ v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝² : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
property✝¹ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
sum_eq : x + z = y + z
property✝ : List.length ((y + z) :: List.zipWith (fun x y => x + y) ys zs) = m
⊢ 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✝

State before:
case h_2.inl.h_2.inr.refl.refl
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₂✝¹ v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝² : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
property✝¹ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
sum_eq : x + z = y + z
property✝ : List.length ((y + z) :: List.zipWith (fun x y => x + y) ys zs) = m
⊢ 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₁, eq₂] at sum_eq
State after:
case h_2.inl.h_2.inr.refl.refl
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₂✝¹ v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝² : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
property✝¹ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
property✝ : List.length ((y + z) :: List.zipWith (fun x y => x + y) ys zs) = m
sum_eq : 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✝

State before:
case h_2.inl.h_2.inr.refl.refl
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₂✝¹ v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝² : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
eq : List.length (y✝ :: tail✝) = m
neq : ¬x✝ = y✝
h : x✝ ≤ y✝
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
property✝¹ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
property✝ : List.length ((y + z) :: List.zipWith (fun x y => x + y) ys zs) = m
sum_eq : 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:
contradiction
State after:
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✝

State before:
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:
rw [Order.lex_impl] at h
State after:
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 :
  match { val := x :: xs, property := p₁ }, { val := y :: ys, 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 := x :: xs, property := p₁ }) (Vector.tail { val := y :: ys, property := p₂ })
    else x_1 ≤ 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✝¹ :
  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✝

State before:
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 :
  match { val := x :: xs, property := p₁ }, { val := y :: ys, 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 := x :: xs, property := p₁ }) (Vector.tail { val := y :: ys, property := p₂ })
    else x_1 ≤ 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✝¹ :
  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:
split at h
State after:
case h_2.inr.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 ℕ
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
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := x :: xs, property := p₁ } = { val := [], property := property✝¹ }
heq✝ : { val := y :: ys, property := p₂ } = { val := [], property := property✝ }
h : True
⊢ x✝ ≤ y✝

case h_2.inr.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✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.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 ℕ
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
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := x :: xs, property := p₁ } = { val := [], property := property✝¹ }
heq✝ : { val := y :: ys, property := p₂ } = { val := [], property := property✝ }
h : True
⊢ x✝ ≤ y✝

case h_2.inr.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✝
⊢ x✝¹ ≤ y✝¹
Tactic:
simp at *
State after:
case h_2.inr.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✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.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✝
⊢ x✝¹ ≤ y✝¹
Tactic:
split at h
State after:
case h_2.inr.h_2.inl
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✝ : x✝ = y✝
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
⊢ x✝¹ ≤ y✝¹

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
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✝ : x✝ = y✝
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
⊢ x✝¹ ≤ y✝¹

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
rename_i var_mul₁ var_mul₂ _ _ _ _ _ _ _ _ _ heq₁ heq₂ eq
State after:
case h_2.inr.h_2.inl
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
var_mul₁ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝¹ :: tail✝³, property := property✝³ }
var_mul₂ :
  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✝ }
eq : x✝ = y✝
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
⊢ x✝¹ ≤ y✝¹

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
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
var_mul₁ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝¹ :: tail✝³, property := property✝³ }
var_mul₂ :
  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✝ }
eq : x✝ = y✝
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
⊢ x✝¹ ≤ y✝¹

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
simp [map₂, Variables.mul, List.zipWith] at var_mul₁ var_mul₂
State after:
case h_2.inr.h_2.inl
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
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝¹ :: tail✝³, property := property✝³ }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { 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✝ }
eq : x✝ = y✝
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
⊢ x✝¹ ≤ y✝¹

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl
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
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝¹ :: tail✝³, property := property✝³ }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { 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✝ }
eq : x✝ = y✝
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
⊢ x✝¹ ≤ y✝¹

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
cases heq₁
State after:
case h_2.inr.h_2.inl.refl
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
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝ :: tail✝², property := property✝³ }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝¹ :: tail✝¹, property := property✝² }
h✝ : ¬x✝ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
y✝ : ℕ
tail✝ : List ℕ
property✝¹ : List.length (y✝ :: tail✝) = m
heq₂ : { val := y :: ys, property := p₂ } = { val := y✝ :: tail✝, property := property✝¹ }
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
eq : x = y✝
property✝ : List.length (x :: xs) = m
⊢ x✝ ≤ y✝¹

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl.refl
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
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝ :: tail✝², property := property✝³ }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝¹ :: tail✝¹, property := property✝² }
h✝ : ¬x✝ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
y✝ : ℕ
tail✝ : List ℕ
property✝¹ : List.length (y✝ :: tail✝) = m
heq₂ : { val := y :: ys, property := p₂ } = { val := y✝ :: tail✝, property := property✝¹ }
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
eq : x = y✝
property✝ : List.length (x :: xs) = m
⊢ x✝ ≤ y✝¹

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
cases heq₂
State after:
case h_2.inr.h_2.inl.refl.refl
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
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝ :: tail✝¹, property := property✝³ }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝ :: tail✝, property := property✝² }
h✝ : ¬x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
property✝¹ : List.length (x :: xs) = m
eq : x = y
property✝ : List.length (y :: ys) = m
⊢ x✝ ≤ y✝

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl.refl.refl
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
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝ :: tail✝¹, property := property✝³ }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝ :: tail✝, property := property✝² }
h✝ : ¬x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
property✝¹ : List.length (x :: xs) = m
eq : x = y
property✝ : List.length (y :: ys) = m
⊢ x✝ ≤ y✝

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
cases var_mul₁
State after:
case h_2.inr.h_2.inl.refl.refl.refl
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
y✝ : ℕ
tail✝ : List ℕ
property✝³ : List.length (y✝ :: tail✝) = m
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝ :: tail✝, property := property✝³ }
v₁✝ v₂✝ : Vector ℕ m
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
property✝² : List.length (x :: xs) = m
eq : x = y
property✝¹ : List.length (y :: ys) = m
h✝ : ¬x + z = y✝
property✝ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
⊢ x + z ≤ y✝

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl.refl.refl.refl
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
y✝ : ℕ
tail✝ : List ℕ
property✝³ : List.length (y✝ :: tail✝) = m
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝ :: tail✝, property := property✝³ }
v₁✝ v₂✝ : Vector ℕ m
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
property✝² : List.length (x :: xs) = m
eq : x = y
property✝¹ : List.length (y :: ys) = m
h✝ : ¬x + z = y✝
property✝ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
⊢ x + z ≤ y✝

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
cases var_mul₂
State after:
case h_2.inr.h_2.inl.refl.refl.refl.refl
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₂✝¹ v₁✝ v₂✝ : Vector ℕ m
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
property✝³ : List.length (x :: xs) = m
eq : x = y
property✝² : List.length (y :: ys) = m
property✝¹ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
h✝ : ¬x + z = y + z
property✝ : List.length ((y + z) :: List.zipWith (fun x y => x + y) ys zs) = m
⊢ x + z ≤ y + z

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.h_2.inl.refl.refl.refl.refl
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₂✝¹ v₁✝ v₂✝ : Vector ℕ m
h : Order.lex_impl (tail { val := x :: xs, property := p₁ }) (tail { val := y :: ys, property := p₂ })
property✝³ : List.length (x :: xs) = m
eq : x = y
property✝² : List.length (y :: ys) = m
property✝¹ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
h✝ : ¬x + z = y + z
property✝ : List.length ((y + z) :: List.zipWith (fun x y => x + y) ys zs) = m
⊢ x + z ≤ y + z

case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
simp [eq]
State after:
case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.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
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✝ : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
rename_i var_mul₁ var_mul₂ _ _ _ _ _ _ _ _ _ heq₁ heq₂ eq
State after:
case h_2.inr.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
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
var_mul₁ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝¹ :: tail✝³, property := property✝³ }
var_mul₂ :
  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✝ }
eq : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹

State before:
case h_2.inr.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
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
var_mul₁ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝¹ :: tail✝³, property := property✝³ }
var_mul₂ :
  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✝ }
eq : ¬x✝ = y✝
h : x✝ ≤ y✝
⊢ x✝¹ ≤ y✝¹
Tactic:
cases heq₁
State after:
case h_2.inr.h_2.inr.refl
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
var_mul₁ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝ :: tail✝², property := property✝³ }
var_mul₂ :
  Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ } =
    { val := y✝¹ :: tail✝¹, property := property✝² }
h✝ : ¬x✝ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
y✝ : ℕ
tail✝ : List ℕ
property✝¹ : List.length (y✝ :: tail✝) = m
heq₂ : { val := y :: ys, property := p₂ } = { val := y✝ :: tail✝, property := property✝¹ }
eq : ¬x = y✝
h : x ≤ y✝
property✝ : List.length (x :: xs) = m
⊢ x✝ ≤ y✝¹

State before:
case h_2.inr.h_2.inr.refl
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
var_mul₁ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝ :: tail✝², property := property✝³ }
var_mul₂ :
  Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ } =
    { val := y✝¹ :: tail✝¹, property := property✝² }
h✝ : ¬x✝ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
y✝ : ℕ
tail✝ : List ℕ
property✝¹ : List.length (y✝ :: tail✝) = m
heq₂ : { val := y :: ys, property := p₂ } = { val := y✝ :: tail✝, property := property✝¹ }
eq : ¬x = y✝
h : x ≤ y✝
property✝ : List.length (x :: xs) = m
⊢ x✝ ≤ y✝¹
Tactic:
cases heq₂
State after:
case h_2.inr.h_2.inr.refl.refl
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
var_mul₁ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝ :: tail✝¹, property := property✝³ }
var_mul₂ :
  Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ } =
    { val := y✝ :: tail✝, property := property✝² }
h✝ : ¬x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
property✝¹ : List.length (x :: xs) = m
eq : ¬x = y
h : x ≤ y
property✝ : List.length (y :: ys) = m
⊢ x✝ ≤ y✝

State before:
case h_2.inr.h_2.inr.refl.refl
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
var_mul₁ :
  Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ } =
    { val := x✝ :: tail✝¹, property := property✝³ }
var_mul₂ :
  Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ } =
    { val := y✝ :: tail✝, property := property✝² }
h✝ : ¬x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
property✝¹ : List.length (x :: xs) = m
eq : ¬x = y
h : x ≤ y
property✝ : List.length (y :: ys) = m
⊢ x✝ ≤ y✝
Tactic:
simp [map₂, Variables.mul, List.zipWith] at var_mul₁ var_mul₂
State after:
case h_2.inr.h_2.inr.refl.refl
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
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝ :: tail✝¹, property := property✝³ }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝ :: tail✝, property := property✝² }
h✝ : ¬x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
property✝¹ : List.length (x :: xs) = m
eq : ¬x = y
h : x ≤ y
property✝ : List.length (y :: ys) = m
⊢ x✝ ≤ y✝

State before:
case h_2.inr.h_2.inr.refl.refl
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
var_mul₁ :
  { val := (x + z) :: List.zipWith (fun x y => x + y) xs zs,
      property := (_ : (fun l => List.length l = m) ((x + z) :: List.zipWith (fun x y => x + y) xs zs)) } =
    { val := x✝ :: tail✝¹, property := property✝³ }
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝ :: tail✝, property := property✝² }
h✝ : ¬x✝ = y✝
v₁✝ v₂✝ : Vector ℕ m
property✝¹ : List.length (x :: xs) = m
eq : ¬x = y
h : x ≤ y
property✝ : List.length (y :: ys) = m
⊢ x✝ ≤ y✝
Tactic:
cases var_mul₁
State after:
case h_2.inr.h_2.inr.refl.refl.refl
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
y✝ : ℕ
tail✝ : List ℕ
property✝³ : List.length (y✝ :: tail✝) = m
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝ :: tail✝, property := property✝³ }
v₁✝ v₂✝ : Vector ℕ m
property✝² : List.length (x :: xs) = m
eq : ¬x = y
h : x ≤ y
property✝¹ : List.length (y :: ys) = m
h✝ : ¬x + z = y✝
property✝ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
⊢ x + z ≤ y✝

State before:
case h_2.inr.h_2.inr.refl.refl.refl
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
y✝ : ℕ
tail✝ : List ℕ
property✝³ : List.length (y✝ :: tail✝) = m
var_mul₂ :
  { val := (y + z) :: List.zipWith (fun x y => x + y) ys zs,
      property := (_ : (fun l => List.length l = m) ((y + z) :: List.zipWith (fun x y => x + y) ys zs)) } =
    { val := y✝ :: tail✝, property := property✝³ }
v₁✝ v₂✝ : Vector ℕ m
property✝² : List.length (x :: xs) = m
eq : ¬x = y
h : x ≤ y
property✝¹ : List.length (y :: ys) = m
h✝ : ¬x + z = y✝
property✝ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
⊢ x + z ≤ y✝
Tactic:
cases var_mul₂
State after:
case h_2.inr.h_2.inr.refl.refl.refl.refl
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₂✝¹ v₁✝ v₂✝ : Vector ℕ m
property✝³ : List.length (x :: xs) = m
eq : ¬x = y
h : x ≤ y
property✝² : List.length (y :: ys) = m
property✝¹ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
h✝ : ¬x + z = y + z
property✝ : List.length ((y + z) :: List.zipWith (fun x y => x + y) ys zs) = m
⊢ x + z ≤ y + z

State before:
case h_2.inr.h_2.inr.refl.refl.refl.refl
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₂✝¹ v₁✝ v₂✝ : Vector ℕ m
property✝³ : List.length (x :: xs) = m
eq : ¬x = y
h : x ≤ y
property✝² : List.length (y :: ys) = m
property✝¹ : List.length ((x + z) :: List.zipWith (fun x y => x + y) xs zs) = m
h✝ : ¬x + z = y + z
property✝ : List.length ((y + z) :: List.zipWith (fun x y => x + y) ys zs) = m
⊢ x + z ≤ y + z
Tactic:
simp at *
State after:
case h_2.inr.h_2.inr.refl.refl.refl.refl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p₁ : succ (List.length xs) = m
y : ℕ
ys : List ℕ
p₂ : succ (List.length ys) = m
z : ℕ
zs : List ℕ
p₃ : succ (List.length zs) = m
v₁✝¹ v₂✝¹ v₁✝ v₂✝ : Vector ℕ m
property✝³ : succ (List.length xs) = m
eq : ¬x = y
h : x ≤ y
property✝² : succ (List.length ys) = m
property✝¹ : succ (min (List.length xs) (List.length zs)) = m
h✝ : ¬x = y
property✝ : succ (min (List.length ys) (List.length zs)) = m
⊢ x ≤ y

State before:
case h_2.inr.h_2.inr.refl.refl.refl.refl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p₁ : succ (List.length xs) = m
y : ℕ
ys : List ℕ
p₂ : succ (List.length ys) = m
z : ℕ
zs : List ℕ
p₃ : succ (List.length zs) = m
v₁✝¹ v₂✝¹ v₁✝ v₂✝ : Vector ℕ m
property✝³ : succ (List.length xs) = m
eq : ¬x = y
h : x ≤ y
property✝² : succ (List.length ys) = m
property✝¹ : succ (min (List.length xs) (List.length zs)) = m
h✝ : ¬x = y
property✝ : succ (min (List.length ys) (List.length zs)) = m
⊢ x ≤ y
Tactic:
exact h
State after:
no goals