internlm/Lean-Github huggingface dataset:
Theorem: algebra.lex_le_antisymm
Proof 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]
Proof 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 }
Theorem: algebra.lex_le_antisymm
Proof 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
Proof 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 }
Theorem: algebra.lex_le_antisymm
Proof 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₁
Proof 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 }
Theorem: algebra.lex_le_antisymm
Proof 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
Proof 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 }
Theorem: algebra.lex_le_antisymm
Proof 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
Proof 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 }
Theorem: algebra.lex_le_antisymm
Proof 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
Proof 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 }
Theorem: algebra.lex_le_antisymm
Proof 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
Proof 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 }
Theorem: algebra.lex_le_antisymm
Proof 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
Proof 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 }
Theorem: algebra.lex_le_antisymm
Proof 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
Proof 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 }
Theorem: algebra.lex_le_antisymm
Proof 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
Proof 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 }