internlm/Lean-Github huggingface dataset:
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex b a
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.lex a b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
rename_i eq _ _ neq
Proof state after:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
neq : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
neq : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
rw [eq] at neq
Proof state after:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
neq : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum b
⊢ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
eq : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
neq : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum b
⊢ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
contradiction
Proof state after:
case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
split
Proof state after:
case inr.inr.inr.inl
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : Order.grlex.elem_sum b < Order.grlex.elem_sum a
⊢ False ∨ True

case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
⊢ False ∨ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inr.inl
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : Order.grlex.elem_sum b < Order.grlex.elem_sum a
⊢ False ∨ True

case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
⊢ False ∨ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
simp at *
Proof state after:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
⊢ False ∨ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
⊢ False ∨ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
simp at *
Proof state after:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝³ : Order.lex b a
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
rename_i neq h₁ h₂
Proof state after:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
have contr := Nat.le_antisymm h₁ h₂
Proof state after:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
contr : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
contr : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
rw [contr] at neq
Proof state after:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum a
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
contr : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
neq : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum a
h₁ : Order.grlex.elem_sum b ≤ Order.grlex.elem_sum a
h₂ : Order.grlex.elem_sum a ≤ Order.grlex.elem_sum b
contr : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
simp at *
Proof state after:
no goals
Theorem: algebra.grlex_le_total
Proof state before:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : ¬Order.lex b a
⊢ False ∨ False

case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False
Tactic:
(first | split | simp)
Proof state after:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : ¬Order.lex b a
⊢ False

case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False
Theorem: algebra.grlex_le_total
Proof state before:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : ¬Order.lex b a
⊢ False ∨ False

case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False
Tactic:
first | split | simp
Proof state after:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : ¬Order.lex b a
⊢ False

case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False
Theorem: algebra.grlex_le_total
Proof state before:
case inl.inr.inr.inr.inl
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ if Order.lex b a then True else False

case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False
Tactic:
split
Proof state after:
case inl.inr.inr.inr.inl.inl
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : Order.lex b a
⊢ False ∨ True

case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : ¬Order.lex b a
⊢ False ∨ False

case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False
Theorem: algebra.grlex_le_total
Proof state before:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : ¬Order.lex b a
⊢ False ∨ False

case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False
Tactic:
simp
Proof state after:
case inl.inr.inr.inr.inl.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex a b
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝¹ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
h✝ : ¬Order.lex b a
⊢ False

case inl.inr.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex a b
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex b a
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.lex a b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
(first | split | simp)
Proof state after:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex b a
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.lex a b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex b a
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.lex a b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
first | split | simp
Proof state after:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex b a
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.lex a b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inl.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁴ : Order.lex b a
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝² : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝¹ : ¬Order.lex a b
h✝ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
⊢ False ∨ if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
split
Proof state after:
case inr.inr.inl.inr.inr.inl
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex b a
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.lex a b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ True

case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex b a
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.lex a b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.grlex_le_total
Proof state before:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex b a
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.lex a b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False ∨ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Tactic:
simp
Proof state after:
case inr.inr.inl.inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝⁵ : Order.lex b a
h✝⁴ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝³ : Order.grlex.elem_sum a = Order.grlex.elem_sum b
h✝² : ¬Order.lex a b
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum a
h✝ : ¬Order.grlex.elem_sum b = Order.grlex.elem_sum a
⊢ False

case inr.inr.inr
n : ℕ
a b : Variables n order.GrLex
h✝² : Order.lex b a
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum b
⊢ False ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then True else False
Theorem: algebra.zipWith_to_fold
Proof state before:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
h : List.length l₁ = List.length l₂
⊢ foldl algebra.sum (init₁ + init₂) (zipWith algebra.sum l₁ l₂) =
    algebra.sum (foldl algebra.sum init₁ l₁) (foldl algebra.sum init₂ l₂)
Tactic:
simp [algebra.sum]
Proof state after:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
h : List.length l₁ = List.length l₂
⊢ foldl (fun a b => a + b) (init₁ + init₂) (zipWith (fun a b => a + b) l₁ l₂) =
    foldl (fun a b => a + b) init₁ l₁ + foldl (fun a b => a + b) init₂ l₂
Theorem: algebra.zipWith_to_fold
Proof state before:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
h : List.length l₁ = List.length l₂
⊢ foldl (fun a b => a + b) (init₁ + init₂) (zipWith (fun a b => a + b) l₁ l₂) =
    foldl (fun a b => a + b) init₁ l₁ + foldl (fun a b => a + b) init₂ l₂
Tactic:
match l₁, l₂ with
  | [], []       => simp
  | x::xs, y::ys => simp
                    have open_init₂ : init₂ + (x + y) = x + init₂ + y
                    rw [Nat.add_right_comm, Nat.add_comm] 
                    rw [Nat.add_assoc, open_init₂, ← Nat.add_assoc, ←Nat.add_assoc]
                    have size_eq : xs.length = ys.length
                    simp at h
                    exact h
                    have res := zipWith_to_fold (init₁ + x) (init₂ + y) xs ys size_eq
                    simp [sum] at res
                    rw [Nat.add_assoc]
                    exact res
Proof state after:
no goals
Theorem: algebra.zipWith_to_fold
Proof state before:
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
h : List.length [] = List.length []
⊢ foldl (fun a b => a + b) (init₁ + init₂) (zipWith (fun a b => a + b) [] []) =
    foldl (fun a b => a + b) init₁ [] + foldl (fun a b => a + b) init₂ []
Tactic:
simp
Proof state after:
no goals
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₂) (zipWith (fun a b => a + b) (x :: xs) (y :: ys)) =
    foldl (fun a b => a + b) init₁ (x :: xs) + foldl (fun a b => a + b) init₂ (y :: ys)
Tactic:
simp
Proof state after:
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