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

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

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

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

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

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

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

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

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

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

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

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

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

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