internlm/Lean-Github huggingface dataset:
Theorem: algebra.zipWith_to_fold
Proof state before:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
⊢ foldl (fun a b => a + b) (init₁ + init₂ + (x + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Tactic:
have open_init₂ : init₂ + (x + y) = x + init₂ + y
Proof state after:
case open_init₂
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
⊢ init₂ + (x + y) = x + init₂ + y

init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
⊢ foldl (fun a b => a + b) (init₁ + init₂ + (x + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Theorem: algebra.zipWith_to_fold
Proof state before:
case open_init₂
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
⊢ init₂ + (x + y) = x + init₂ + y

init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
⊢ foldl (fun a b => a + b) (init₁ + init₂ + (x + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Tactic:
rw [Nat.add_right_comm, Nat.add_comm]
Proof state after:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
⊢ foldl (fun a b => a + b) (init₁ + init₂ + (x + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Theorem: algebra.zipWith_to_fold
Proof state before:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
⊢ foldl (fun a b => a + b) (init₁ + init₂ + (x + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Tactic:
rw [Nat.add_assoc, open_init₂, ← Nat.add_assoc, ←Nat.add_assoc]
Proof state after:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Theorem: algebra.zipWith_to_fold
Proof state before:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Tactic:
have size_eq : xs.length = ys.length
Proof state after:
case size_eq
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
⊢ List.length xs = List.length ys

init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Theorem: algebra.zipWith_to_fold
Proof state before:
case size_eq
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
⊢ List.length xs = List.length ys

init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Tactic:
simp at h
Proof state after:
case size_eq
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
open_init₂ : init₂ + (x + y) = x + init₂ + y
h : List.length xs = List.length ys
⊢ List.length xs = List.length ys

init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Theorem: algebra.zipWith_to_fold
Proof state before:
case size_eq
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
open_init₂ : init₂ + (x + y) = x + init₂ + y
h : List.length xs = List.length ys
⊢ List.length xs = List.length ys

init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Tactic:
exact h
Proof state after:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Theorem: algebra.zipWith_to_fold
Proof state before:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Tactic:
have res := zipWith_to_fold (init₁ + x) (init₂ + y) xs ys size_eq
Proof state after:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
res :
  foldl algebra.sum (init₁ + x + (init₂ + y)) (zipWith algebra.sum xs ys) =
    algebra.sum (foldl algebra.sum (init₁ + x) xs) (foldl algebra.sum (init₂ + y) ys)
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Theorem: algebra.zipWith_to_fold
Proof state before:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
res :
  foldl algebra.sum (init₁ + x + (init₂ + y)) (zipWith algebra.sum xs ys) =
    algebra.sum (foldl algebra.sum (init₁ + x) xs) (foldl algebra.sum (init₂ + y) ys)
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Tactic:
simp [sum] at res
Proof state after:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
res :
  foldl (fun a b => a + b) (init₁ + x + (init₂ + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Theorem: algebra.zipWith_to_fold
Proof state before:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
res :
  foldl (fun a b => a + b) (init₁ + x + (init₂ + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Tactic:
rw [Nat.add_assoc]
Proof state after:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
res :
  foldl (fun a b => a + b) (init₁ + x + (init₂ + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
⊢ foldl (fun a b => a + b) (init₁ + x + (init₂ + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Theorem: algebra.zipWith_to_fold
Proof state before:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
res :
  foldl (fun a b => a + b) (init₁ + x + (init₂ + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
⊢ foldl (fun a b => a + b) (init₁ + x + (init₂ + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
Tactic:
exact res
Proof state after:
no goals
Theorem: algebra.elem_sum_is_hom
Proof state before:
n : ℕ
⊢ ∀ (a b : Variables n order.GrLex),
    Order.grlex.elem_sum (Variables.mul a b) = Order.grlex.elem_sum a + Order.grlex.elem_sum b
Tactic:
intros a b
Proof state after:
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex.elem_sum (Variables.mul a b) = Order.grlex.elem_sum a + Order.grlex.elem_sum b
Theorem: algebra.elem_sum_is_hom
Proof state before:
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex.elem_sum (Variables.mul a b) = Order.grlex.elem_sum a + Order.grlex.elem_sum b
Tactic:
match a, b with
  | ⟨[], _⟩   , ⟨[], _⟩    => simp [Order.grlex.elem_sum, Variables.mul]
  | ⟨x::xs, p⟩, ⟨y::ys, q⟩ => simp [Order.grlex.elem_sum, Variables.mul]
                              simp [List.zipWith]
                              simp [foldl_cons]
                              have size_eq : (x::xs).length = (y::ys).length
                              rw [Eq.symm q] at p
                              exact p
                              have tails_size_eq : xs.length = ys.length
                              simp at size_eq
                              exact size_eq
                              have hh := zipWith_to_fold x y xs ys tails_size_eq
                              simp [algebra.sum] at hh 
                              simp [hh]
Proof state after:
no goals
Theorem: algebra.elem_sum_is_hom
Proof state before:
n : ℕ
a b : Variables n order.GrLex
property✝¹ property✝ : List.length [] = n
⊢ Order.grlex.elem_sum (Variables.mul { val := [], property := property✝¹ } { val := [], property := property✝ }) =
    Order.grlex.elem_sum { val := [], property := property✝¹ } +
      Order.grlex.elem_sum { val := [], property := property✝ }
Tactic:
simp [Order.grlex.elem_sum, Variables.mul]
Proof state after:
no goals
Theorem: algebra.elem_sum_is_hom
Proof state before:
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
⊢ Order.grlex.elem_sum (Variables.mul { val := x :: xs, property := p } { val := y :: ys, property := q }) =
    Order.grlex.elem_sum { val := x :: xs, property := p } + Order.grlex.elem_sum { val := y :: ys, property := q }
Tactic:
simp [Order.grlex.elem_sum, Variables.mul]
Proof state after:
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Theorem: algebra.elem_sum_is_hom
Proof state before:
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Tactic:
have size_eq : (x::xs).length = (y::ys).length
Proof state after:
case size_eq
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
⊢ List.length (x :: xs) = List.length (y :: ys)

n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Theorem: algebra.elem_sum_is_hom
Proof state before:
case size_eq
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
⊢ List.length (x :: xs) = List.length (y :: ys)

n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Tactic:
rw [Eq.symm q] at p
Proof state after:
case size_eq
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
p : List.length (x :: xs) = List.length (y :: ys)
q : List.length (y :: ys) = n
⊢ List.length (x :: xs) = List.length (y :: ys)

n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Theorem: algebra.elem_sum_is_hom
Proof state before:
case size_eq
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
p : List.length (x :: xs) = List.length (y :: ys)
q : List.length (y :: ys) = n
⊢ List.length (x :: xs) = List.length (y :: ys)

n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Tactic:
exact p
Proof state after:
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Theorem: algebra.elem_sum_is_hom
Proof state before:
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Tactic:
have tails_size_eq : xs.length = ys.length
Proof state after:
case tails_size_eq
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
⊢ List.length xs = List.length ys

n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
tails_size_eq : List.length xs = List.length ys
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Theorem: algebra.elem_sum_is_hom
Proof state before:
case tails_size_eq
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
⊢ List.length xs = List.length ys

n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
tails_size_eq : List.length xs = List.length ys
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Tactic:
simp at size_eq
Proof state after:
case tails_size_eq
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length xs = List.length ys
⊢ List.length xs = List.length ys

n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
tails_size_eq : List.length xs = List.length ys
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Theorem: algebra.elem_sum_is_hom
Proof state before:
case tails_size_eq
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length xs = List.length ys
⊢ List.length xs = List.length ys

n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
tails_size_eq : List.length xs = List.length ys
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Tactic:
exact size_eq
Proof state after:
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
tails_size_eq : List.length xs = List.length ys
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Theorem: algebra.elem_sum_is_hom
Proof state before:
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
tails_size_eq : List.length xs = List.length ys
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Tactic:
have hh := zipWith_to_fold x y xs ys tails_size_eq
Proof state after:
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
tails_size_eq : List.length xs = List.length ys
hh :
  foldl algebra.sum (x + y) (zipWith algebra.sum xs ys) = algebra.sum (foldl algebra.sum x xs) (foldl algebra.sum y ys)
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Theorem: algebra.elem_sum_is_hom
Proof state before:
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
tails_size_eq : List.length xs = List.length ys
hh :
  foldl algebra.sum (x + y) (zipWith algebra.sum xs ys) = algebra.sum (foldl algebra.sum x xs) (foldl algebra.sum y ys)
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Tactic:
simp [algebra.sum] at hh
Proof state after:
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
tails_size_eq : List.length xs = List.length ys
hh :
  foldl (fun a b => a + b) (x + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) x xs + foldl (fun a b => a + b) y ys
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Theorem: algebra.elem_sum_is_hom
Proof state before:
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
tails_size_eq : List.length xs = List.length ys
hh :
  foldl (fun a b => a + b) (x + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) x xs + foldl (fun a b => a + b) y ys
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
Tactic:
simp [hh]
Proof state after:
no goals
Theorem: algebra.grlex_add_le_add
Proof state before:
n : ℕ
⊢ ∀ (a b c : Variables n order.GrLex), Order.grlex a b → Order.grlex (Variables.mul a c) (Variables.mul b c)
Tactic:
intros a b c h_le
Proof state after:
n : ℕ
a b c : Variables n order.GrLex
h_le : Order.grlex a b
⊢ Order.grlex (Variables.mul a c) (Variables.mul b c)
Theorem: algebra.grlex_add_le_add
Proof state before:
n : ℕ
a b c : Variables n order.GrLex
h_le : Order.grlex a b
⊢ Order.grlex (Variables.mul a c) (Variables.mul b c)
Tactic:
rw [Order.grlex]
Proof state after:
n : ℕ
a b c : Variables n order.GrLex
h_le : Order.grlex a b
⊢ let sum₁ := Order.grlex.elem_sum (Variables.mul a c);
  let sum₂ := Order.grlex.elem_sum (Variables.mul b c);
  if sum₁ < sum₂ then True
  else if sum₁ = sum₂ then if Order.lex (Variables.mul a c) (Variables.mul b c) then True else False else False
Theorem: algebra.grlex_add_le_add
Proof state before:
n : ℕ
a b c : Variables n order.GrLex
h_le : Order.grlex a b
⊢ let sum₁ := Order.grlex.elem_sum (Variables.mul a c);
  let sum₂ := Order.grlex.elem_sum (Variables.mul b c);
  if sum₁ < sum₂ then True
  else if sum₁ = sum₂ then if Order.lex (Variables.mul a c) (Variables.mul b c) then True else False else False
Tactic:
rw [Order.grlex] at h_le
Proof state after:
n : ℕ
a b c : Variables n order.GrLex
h_le :
  let sum₁ := Order.grlex.elem_sum a;
  let sum₂ := Order.grlex.elem_sum b;
  if sum₁ < sum₂ then True else if sum₁ = sum₂ then if Order.lex a b then True else False else False
⊢ let sum₁ := Order.grlex.elem_sum (Variables.mul a c);
  let sum₂ := Order.grlex.elem_sum (Variables.mul b c);
  if sum₁ < sum₂ then True
  else if sum₁ = sum₂ then if Order.lex (Variables.mul a c) (Variables.mul b c) then True else False else False