internlm/Lean-Github huggingface dataset:
Theorem: polynomial.remainder_in_ideal
Proof state before:
case r_eq
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
⊢ remainder = divisible - quotient

n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ remainder ∈ asIdeal dividers
Tactic:
rw [div_sum_r_eq_p, add_comm, sub_eq_add_neg, add_assoc,
    add_comm, add_right_neg, zero_add]
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ remainder ∈ asIdeal dividers
Theorem: polynomial.remainder_in_ideal
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ remainder ∈ asIdeal dividers
Tactic:
rw [r_eq]
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ divisible - quotient ∈ asIdeal dividers
Theorem: polynomial.remainder_in_ideal
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ divisible - quotient ∈ asIdeal dividers
Tactic:
exact sub_mem divisible_in_ideal quotient_in_ideal
Proof state after:
no goals
Theorem: algebra.lex_le_refl
Proof state before:
n : ℕ
⊢ ∀ (a : Variables n order.Lex), Order.lex a a
Tactic:
intro a
Proof state after:
n : ℕ
a : Variables n order.Lex
⊢ Order.lex a a
Theorem: algebra.lex_le_refl
Proof state before:
n : ℕ
a : Variables n order.Lex
⊢ Order.lex a a
Tactic:
exact aux n a
Proof state after:
no goals
Theorem: algebra.lex_le_refl
Proof state before:
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
⊢ Order.lex_impl v v
Tactic:
match v with 
  | ⟨[], p⟩    => rw [Order.lex_impl]
                  split
                  simp at *
                  simp at p
                  simp at *                                   
  | ⟨x::xs, _⟩ => rw [Order.lex_impl]
                  split
                  simp
                  simp at *
                  simp at *
                  simp [Nat.le_refl]
                  rename_i x₁ _ x₂ _ h₁ h₂
                  have h₃ := Eq.symm h₁.left
                  have h₄ := Eq.symm h₂.left
                  rw [h₃, h₄]
                  simp [Nat.le_refl]
                  apply aux (m-1) (tail ⟨x::xs, _⟩)
Proof state after:
no goals
Theorem: algebra.lex_le_refl
Proof state before:
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
p : List.length [] = m
⊢ Order.lex_impl { val := [], property := p } { val := [], property := p }
Tactic:
rw [Order.lex_impl]
Proof state after:
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
p : List.length [] = m
⊢ match { val := [], property := p }, { val := [], property := p } 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 { val := [], property := p }) (Vector.tail { val := [], property := p })
    else x ≤ y
Theorem: algebra.lex_le_refl
Proof state before:
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
p : List.length [] = m
⊢ match { val := [], property := p }, { val := [], property := p } 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 { val := [], property := p }) (Vector.tail { val := [], property := p })
    else x ≤ y
Tactic:
split
Proof state after:
case h_1
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
p : List.length [] = m
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := [], property := p } = { val := [], property := property✝¹ }
heq✝ : { val := [], property := p } = { val := [], property := property✝ }
⊢ True

case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
p : List.length [] = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := [], property := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := [], property := p } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := p }) else x✝ ≤ y✝
Theorem: algebra.lex_le_refl
Proof state before:
case h_1
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
p : List.length [] = m
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := [], property := p } = { val := [], property := property✝¹ }
heq✝ : { val := [], property := p } = { val := [], property := property✝ }
⊢ True

case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
p : List.length [] = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := [], property := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := [], property := p } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := p }) else x✝ ≤ y✝
Tactic:
simp at *
Proof state after:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
p : List.length [] = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := [], property := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := [], property := p } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := p }) else x✝ ≤ y✝
Theorem: algebra.lex_le_refl
Proof state before:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
p : List.length [] = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := [], property := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := [], property := p } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := p }) else x✝ ≤ y✝
Tactic:
simp at p
Proof state after:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
p : 0 = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := [], property := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := [], property := p } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := p }) else x✝ ≤ y✝
Theorem: algebra.lex_le_refl
Proof state before:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
p : 0 = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := [], property := p } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := [], property := p } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then Order.lex_impl (tail { val := [], property := p }) (tail { val := [], property := p }) else x✝ ≤ y✝
Tactic:
simp at *
Proof state after:
no goals
Theorem: algebra.lex_le_refl
Proof state before:
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝ : List.length (x :: xs) = m
⊢ Order.lex_impl { val := x :: xs, property := property✝ } { val := x :: xs, property := property✝ }
Tactic:
rw [Order.lex_impl]
Proof state after:
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝ : List.length (x :: xs) = m
⊢ match { val := x :: xs, property := property✝ }, { val := x :: xs, property := property✝ } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x_1 :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
    if x_1 = y then
      Order.lex_impl (Vector.tail { val := x :: xs, property := property✝ })
        (Vector.tail { val := x :: xs, property := property✝ })
    else x_1 ≤ y
Theorem: algebra.lex_le_refl
Proof state before:
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝ : List.length (x :: xs) = m
⊢ match { val := x :: xs, property := property✝ }, { val := x :: xs, property := property✝ } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x_1 :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
    if x_1 = y then
      Order.lex_impl (Vector.tail { val := x :: xs, property := property✝ })
        (Vector.tail { val := x :: xs, property := property✝ })
    else x_1 ≤ y
Tactic:
split
Proof state after:
case h_1
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝² : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := x :: xs, property := property✝² } = { val := [], property := property✝¹ }
heq✝ : { val := x :: xs, property := property✝² } = { val := [], property := property✝ }
⊢ True

case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝² : List.length (x :: xs) = m
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 := property✝² } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝² }) (tail { val := x :: xs, property := property✝² })
  else x✝ ≤ y✝
Theorem: algebra.lex_le_refl
Proof state before:
case h_1
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝² : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
property✝¹ property✝ : List.length [] = m
heq✝¹ : { val := x :: xs, property := property✝² } = { val := [], property := property✝¹ }
heq✝ : { val := x :: xs, property := property✝² } = { val := [], property := property✝ }
⊢ True

case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝² : List.length (x :: xs) = m
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 := property✝² } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝² }) (tail { val := x :: xs, property := property✝² })
  else x✝ ≤ y✝
Tactic:
simp
Proof state after:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝² : List.length (x :: xs) = m
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 := property✝² } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝² }) (tail { val := x :: xs, property := property✝² })
  else x✝ ≤ y✝
Theorem: algebra.lex_le_refl
Proof state before:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝² : List.length (x :: xs) = m
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 := property✝² } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := x :: xs, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝² }) (tail { val := x :: xs, property := property✝² })
  else x✝ ≤ y✝
Tactic:
simp at *
Proof state after:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝² : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : x = x✝ ∧ xs = tail✝¹
heq✝ : x = y✝ ∧ xs = tail✝
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝² }) (tail { val := x :: xs, property := property✝² })
  else x✝ ≤ y✝
Theorem: algebra.lex_le_refl
Proof state before:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝² : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : x = x✝ ∧ xs = tail✝¹
heq✝ : x = y✝ ∧ xs = tail✝
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝² }) (tail { val := x :: xs, property := property✝² })
  else x✝ ≤ y✝
Tactic:
simp at *
Proof state after:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝² : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : succ (List.length tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : succ (List.length tail✝) = m
heq✝¹ : x = x✝ ∧ xs = tail✝¹
heq✝ : x = y✝ ∧ xs = tail✝
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝² }) (tail { val := x :: xs, property := property✝² })
  else x✝ ≤ y✝
Theorem: algebra.lex_le_refl
Proof state before:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝² : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : succ (List.length tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : succ (List.length tail✝) = m
heq✝¹ : x = x✝ ∧ xs = tail✝¹
heq✝ : x = y✝ ∧ xs = tail✝
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝² }) (tail { val := x :: xs, property := property✝² })
  else x✝ ≤ y✝
Tactic:
rename_i x₁ _ x₂ _ h₁ h₂
Proof state after:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝ : List ℕ
x₁ : succ (List.length tail✝) = m
y✝ : ℕ
x₂ : List ℕ
property✝ : succ (List.length x₂) = m
h₁ : x = x✝ ∧ xs = tail✝
h₂ : x = y✝ ∧ xs = x₂
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝¹ }) (tail { val := x :: xs, property := property✝¹ })
  else x✝ ≤ y✝
Theorem: algebra.lex_le_refl
Proof state before:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝ : List ℕ
x₁ : succ (List.length tail✝) = m
y✝ : ℕ
x₂ : List ℕ
property✝ : succ (List.length x₂) = m
h₁ : x = x✝ ∧ xs = tail✝
h₂ : x = y✝ ∧ xs = x₂
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝¹ }) (tail { val := x :: xs, property := property✝¹ })
  else x✝ ≤ y✝
Tactic:
have h₃ := Eq.symm h₁.left
Proof state after:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝ : List ℕ
x₁ : succ (List.length tail✝) = m
y✝ : ℕ
x₂ : List ℕ
property✝ : succ (List.length x₂) = m
h₁ : x = x✝ ∧ xs = tail✝
h₂ : x = y✝ ∧ xs = x₂
h₃ : x✝ = x
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝¹ }) (tail { val := x :: xs, property := property✝¹ })
  else x✝ ≤ y✝
Theorem: algebra.lex_le_refl
Proof state before:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝ : List ℕ
x₁ : succ (List.length tail✝) = m
y✝ : ℕ
x₂ : List ℕ
property✝ : succ (List.length x₂) = m
h₁ : x = x✝ ∧ xs = tail✝
h₂ : x = y✝ ∧ xs = x₂
h₃ : x✝ = x
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝¹ }) (tail { val := x :: xs, property := property✝¹ })
  else x✝ ≤ y✝
Tactic:
have h₄ := Eq.symm h₂.left
Proof state after:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝ : List ℕ
x₁ : succ (List.length tail✝) = m
y✝ : ℕ
x₂ : List ℕ
property✝ : succ (List.length x₂) = m
h₁ : x = x✝ ∧ xs = tail✝
h₂ : x = y✝ ∧ xs = x₂
h₃ : x✝ = x
h₄ : y✝ = x
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝¹ }) (tail { val := x :: xs, property := property✝¹ })
  else x✝ ≤ y✝
Theorem: algebra.lex_le_refl
Proof state before:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝ : List ℕ
x₁ : succ (List.length tail✝) = m
y✝ : ℕ
x₂ : List ℕ
property✝ : succ (List.length x₂) = m
h₁ : x = x✝ ∧ xs = tail✝
h₂ : x = y✝ ∧ xs = x₂
h₃ : x✝ = x
h₄ : y✝ = x
⊢ if x✝ = y✝ then
    Order.lex_impl (tail { val := x :: xs, property := property✝¹ }) (tail { val := x :: xs, property := property✝¹ })
  else x✝ ≤ y✝
Tactic:
rw [h₃, h₄]
Proof state after:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝ : List ℕ
x₁ : succ (List.length tail✝) = m
y✝ : ℕ
x₂ : List ℕ
property✝ : succ (List.length x₂) = m
h₁ : x = x✝ ∧ xs = tail✝
h₂ : x = y✝ ∧ xs = x₂
h₃ : x✝ = x
h₄ : y✝ = x
⊢ if x = x then
    Order.lex_impl (tail { val := x :: xs, property := property✝¹ }) (tail { val := x :: xs, property := property✝¹ })
  else x ≤ x
Theorem: algebra.lex_le_refl
Proof state before:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝ : List ℕ
x₁ : succ (List.length tail✝) = m
y✝ : ℕ
x₂ : List ℕ
property✝ : succ (List.length x₂) = m
h₁ : x = x✝ ∧ xs = tail✝
h₂ : x = y✝ ∧ xs = x₂
h₃ : x✝ = x
h₄ : y✝ = x
⊢ if x = x then
    Order.lex_impl (tail { val := x :: xs, property := property✝¹ }) (tail { val := x :: xs, property := property✝¹ })
  else x ≤ x
Tactic:
simp [Nat.le_refl]
Proof state after:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝ : List ℕ
x₁ : succ (List.length tail✝) = m
y✝ : ℕ
x₂ : List ℕ
property✝ : succ (List.length x₂) = m
h₁ : x = x✝ ∧ xs = tail✝
h₂ : x = y✝ ∧ xs = x₂
h₃ : x✝ = x
h₄ : y✝ = x
⊢ Order.lex_impl (tail { val := x :: xs, property := property✝¹ }) (tail { val := x :: xs, property := property✝¹ })
Theorem: algebra.lex_le_refl
Proof state before:
case h_2
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝¹ : List.length (x :: xs) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝ : List ℕ
x₁ : succ (List.length tail✝) = m
y✝ : ℕ
x₂ : List ℕ
property✝ : succ (List.length x₂) = m
h₁ : x = x✝ ∧ xs = tail✝
h₂ : x = y✝ ∧ xs = x₂
h₃ : x✝ = x
h₄ : y✝ = x
⊢ Order.lex_impl (tail { val := x :: xs, property := property✝¹ }) (tail { val := x :: xs, property := property✝¹ })
Tactic:
apply aux (m-1) (tail ⟨x::xs, _⟩)
Proof state after:
no goals
Theorem: algebra.lex_le_trans
Proof state before:
n : ℕ
⊢ ∀ (a b c : Variables n order.Lex), Order.lex a b → Order.lex b c → Order.lex a c
Tactic:
intros v₁ v₂ v₃ h₁ h₂
Proof state after:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
⊢ Order.lex v₁ v₃
Theorem: algebra.lex_le_trans
Proof state before:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
⊢ Order.lex v₁ v₃
Tactic:
exact aux n v₁ v₂ v₃ h₁ h₂
Proof state after:
no goals
Theorem: algebra.lex_le_trans
Proof state before:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
p q l : List.length [] = m
ab : Order.lex_impl { val := [], property := p } { val := [], property := q }
bc : Order.lex_impl { val := [], property := q } { val := [], property := l }
⊢ Order.lex_impl { val := [], property := p } { val := [], property := l }
Tactic:
rw [Order.lex_impl]
Proof state after:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
p q l : List.length [] = m
ab : Order.lex_impl { val := [], property := p } { val := [], property := q }
bc : Order.lex_impl { val := [], property := q } { val := [], property := l }
⊢ match { val := [], property := p }, { val := [], property := l } 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 { val := [], property := p }) (Vector.tail { val := [], property := l })
    else x ≤ y