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

State before:
n : ℕ
⊢ ∀ (a b : Variables n order.Lex), Order.lex a b → Order.lex b a → a = b
Tactic:
intros v₁ v₂ h₁ h₂
State after:
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
⊢ v₁ = v₂

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
⊢ v₁ = v₂
Tactic:
exact aux n v₁ v₂ h₁ h₂
State after:
no goals

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
ab : Order.lex_impl a b
ba : Order.lex_impl b a
⊢ a = b
Tactic:
match a, b with
  | ⟨[], p⟩, ⟨[], q⟩       => simp 
  | ⟨x::xs, p⟩, ⟨y::ys, q⟩ => rw [Order.lex_impl] at ab ba
                              simp at *
                              split at ab
                              split at ba
                              rename_i heq₁ heq₂
                              simp [Vector]
                              constructor
                              exact heq₁ 
                              have eq := aux (m-1) (tail ⟨x::xs, p⟩) (tail ⟨y::ys, q⟩) ab ba
                              simp [tail, Vector] at eq
                              exact eq
                              rename_i eq neq
                              have eq_symm := Eq.symm eq
                              contradiction
                              split at ba
                              rename_i neq eq
                              have eq_symm := Eq.symm eq
                              contradiction
                              rename_i neq₁ neq₂
                              have eq := Nat.le_antisymm ab ba
                              contradiction
State after:
no goals

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
p q : List.length [] = m
ab : Order.lex_impl { val := [], property := p } { val := [], property := q }
ba : Order.lex_impl { val := [], property := q } { val := [], property := p }
⊢ { val := [], property := p } = { val := [], property := q }
Tactic:
simp
State after:
no goals

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ab : Order.lex_impl { val := x :: xs, property := p } { val := y :: ys, property := q }
ba : Order.lex_impl { val := y :: ys, property := q } { val := x :: xs, property := p }
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
rw [Order.lex_impl] at ab ba
State after:
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ab :
  match { val := x :: xs, property := p }, { val := y :: ys, property := q } 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 := q })
    else x_1 ≤ y_1
ba :
  match { val := y :: ys, property := q }, { val := x :: xs, 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 := y :: ys, property := q }) (Vector.tail { val := x :: xs, property := p })
    else x_1 ≤ y_1
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ab :
  match { val := x :: xs, property := p }, { val := y :: ys, property := q } 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 := q })
    else x_1 ≤ y_1
ba :
  match { val := y :: ys, property := q }, { val := x :: xs, 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 := y :: ys, property := q }) (Vector.tail { val := x :: xs, property := p })
    else x_1 ≤ y_1
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
simp at *
State after:
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ab :
  if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x ≤ y
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ab :
  if x = y then Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
  else x ≤ y
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
split at ab
State after:
case inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
split at ba
State after:
case inl.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inl.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
rename_i heq₁ heq₂
State after:
case inl.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inl.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
simp [Vector]
State after:
case inl.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ x = y ∧ xs = ys

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inl.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ x = y ∧ xs = ys

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
constructor
State after:
case inl.inl.left
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ x = y

case inl.inl.right
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ xs = ys

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inl.inl.left
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ x = y

case inl.inl.right
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ xs = ys

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
exact heq₁
State after:
case inl.inl.right
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ xs = ys

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inl.inl.right
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ xs = ys

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
have eq := aux (m-1) (tail ⟨x::xs, p⟩) (tail ⟨y::ys, q⟩) ab ba
State after:
case inl.inl.right
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
eq : tail { val := x :: xs, property := p } = tail { val := y :: ys, property := q }
⊢ xs = ys

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inl.inl.right
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
eq : tail { val := x :: xs, property := p } = tail { val := y :: ys, property := q }
⊢ xs = ys

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
simp [tail, Vector] at eq
State after:
case inl.inl.right
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
eq : xs = ys
⊢ xs = ys

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inl.inl.right
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
heq₁ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
heq₂ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
eq : xs = ys
⊢ xs = ys

case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
exact eq
State after:
case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
rename_i eq neq
State after:
case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
eq : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
neq : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
eq : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
neq : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
have eq_symm := Eq.symm eq
State after:
case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
eq : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
neq : ¬y = x
ba : y ≤ x
eq_symm : y = x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inl.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
eq : x = y
ab : Order.lex_impl (tail { val := x :: xs, property := p }) (tail { val := y :: ys, property := q })
neq : ¬y = x
ba : y ≤ x
eq_symm : y = x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
contradiction
State after:
case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
ba :
  if y = x then Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
  else y ≤ x
h✝ : ¬x = y
ab : x ≤ y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
split at ba
State after:
case inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : ¬x = y
ab : x ≤ y
h✝ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : ¬x = y
ab : x ≤ y
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : ¬x = y
ab : x ≤ y
h✝ : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : ¬x = y
ab : x ≤ y
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
rename_i neq eq
State after:
case inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
neq : ¬x = y
ab : x ≤ y
eq : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : ¬x = y
ab : x ≤ y
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
neq : ¬x = y
ab : x ≤ y
eq : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : ¬x = y
ab : x ≤ y
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
have eq_symm := Eq.symm eq
State after:
case inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
neq : ¬x = y
ab : x ≤ y
eq : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
eq_symm : x = y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : ¬x = y
ab : x ≤ y
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inr.inl
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
neq : ¬x = y
ab : x ≤ y
eq : y = x
ba : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := x :: xs, property := p })
eq_symm : x = y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : ¬x = y
ab : x ≤ y
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
contradiction
State after:
case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : ¬x = y
ab : x ≤ y
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
h✝¹ : ¬x = y
ab : x ≤ y
h✝ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
rename_i neq₁ neq₂
State after:
case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
neq₁ : ¬x = y
ab : x ≤ y
neq₂ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
neq₁ : ¬x = y
ab : x ≤ y
neq₂ : ¬y = x
ba : y ≤ x
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
have eq := Nat.le_antisymm ab ba
State after:
case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
neq₁ : ¬x = y
ab : x ≤ y
neq₂ : ¬y = x
ba : y ≤ x
eq : x = y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }

State before:
case inr.inr
n : ℕ
v₁ v₂ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₁
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
neq₁ : ¬x = y
ab : x ≤ y
neq₂ : ¬y = x
ba : y ≤ x
eq : x = y
⊢ { val := x :: xs, property := p } = { val := y :: ys, property := q }
Tactic:
contradiction
State after:
no goals