internlm/Lean-Github huggingface dataset:
Theorem: algebra.Order.ble_eq_true_of_lex
Proof state before:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
neq : ¬(x✝ == y✝) = true
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = 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 := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Tactic:
simp at neq
Proof state after:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
neq : ¬x✝ = y✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = 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 := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Theorem: algebra.Order.ble_eq_true_of_lex
Proof state before:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x = y
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
neq : ¬x✝ = y✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = 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 := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Tactic:
rw [eq₁, eq₂] at eq
Proof state after:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
neq : ¬x✝ = y✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = 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 := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Theorem: algebra.Order.ble_eq_true_of_lex
Proof state before:
case h_2.inr.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
h : lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x = x✝
eq₂ : y = y✝
neq : ¬x✝ = y✝
⊢ decide (x✝ ≤ y✝) = true

case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = 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 := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Tactic:
contradiction
Proof state after:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = 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 := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Theorem: algebra.Order.ble_eq_true_of_lex
Proof state before:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = 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 := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ decide (x✝ ≤ y✝) = true
Tactic:
simp
Proof state after:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = 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 := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ x✝ ≤ y✝
Theorem: algebra.Order.ble_eq_true_of_lex
Proof state before:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = 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 := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ x✝ ≤ y✝
Tactic:
rename_i heq₁ heq₂ _ _
Proof state after:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = 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 := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ x✝ ≤ y✝
Theorem: algebra.Order.ble_eq_true_of_lex
Proof state before:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = 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 := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
⊢ x✝ ≤ y✝
Tactic:
simp at heq₁ heq₂
Proof state after:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
⊢ x✝ ≤ y✝
Theorem: algebra.Order.ble_eq_true_of_lex
Proof state before:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
⊢ x✝ ≤ y✝
Tactic:
have eq₁ := Eq.symm heq₁.left
Proof state after:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x✝ = x
⊢ x✝ ≤ y✝
Theorem: algebra.Order.ble_eq_true_of_lex
Proof state before:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x✝ = x
⊢ x✝ ≤ y✝
Tactic:
have eq₂ := Eq.symm heq₂.left
Proof state after:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x✝ = x
eq₂ : y✝ = y
⊢ x✝ ≤ y✝
Theorem: algebra.Order.ble_eq_true_of_lex
Proof state before:
case h_2.inr.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h✝¹ : ¬(x✝ == y✝) = true
h✝ : ¬x = y
h : x ≤ y
heq₁ : x = x✝ ∧ xs = tail✝¹
heq₂ : y = y✝ ∧ ys = tail✝
eq₁ : x✝ = x
eq₂ : y✝ = y
⊢ x✝ ≤ y✝
Tactic:
rwa [eq₁, eq₂]
Proof state after:
no goals
Theorem: algebra.grlex_lt_iff_le_not_le
Proof state before:
n : ℕ
⊢ ∀ (a b : Variables n order.GrLex), Order.grlex_lt a b ↔ Order.grlex a b ∧ ¬Order.grlex b a
Tactic:
intros a b
Proof state after:
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex_lt a b ↔ Order.grlex a b ∧ ¬Order.grlex b a
Theorem: algebra.grlex_lt_iff_le_not_le
Proof state before:
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex_lt a b ↔ Order.grlex a b ∧ ¬Order.grlex b a
Tactic:
apply Iff.intro
Proof state after:
case mp
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex_lt a b → Order.grlex a b ∧ ¬Order.grlex b a

case mpr
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex a b ∧ ¬Order.grlex b a → Order.grlex_lt a b
Theorem: algebra.grlex_lt_iff_le_not_le
Proof state before:
case mp
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex_lt a b → Order.grlex a b ∧ ¬Order.grlex b a

case mpr
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex a b ∧ ¬Order.grlex b a → Order.grlex_lt a b
Tactic:
repeat (
    rw [Order.grlex_lt]
    simp
)
Proof state after:
no goals
Theorem: algebra.grlex_lt_iff_le_not_le
Proof state before:
case mpr
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex a b ∧ ¬Order.grlex b a → Order.grlex_lt a b
Tactic:
(
rw [Order.grlex_lt]
simp
)
Proof state after:
no goals
Theorem: algebra.grlex_lt_iff_le_not_le
Proof state before:
case mpr
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex a b ∧ ¬Order.grlex b a → Order.grlex_lt a b
Tactic:
rw [Order.grlex_lt]
Proof state after:
case mpr
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex a b ∧ ¬Order.grlex b a → Order.grlex a b ∧ ¬Order.grlex b a
Theorem: algebra.grlex_lt_iff_le_not_le
Proof state before:
case mpr
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex a b ∧ ¬Order.grlex b a → Order.grlex a b ∧ ¬Order.grlex b a
Tactic:
simp
Proof state after:
no goals
Theorem: algebra.grlex_le_refl
Proof state before:
n : ℕ
⊢ ∀ (a : Variables n order.GrLex), Order.grlex a a
Tactic:
intros a
Proof state after:
n : ℕ
a : Variables n order.GrLex
⊢ Order.grlex a a
Theorem: algebra.grlex_le_refl
Proof state before:
n : ℕ
a : Variables n order.GrLex
⊢ Order.grlex a a
Tactic:
simp [Order.grlex]
Proof state after:
n : ℕ
a : Variables n order.GrLex
⊢ if Order.lex a a then True else False
Theorem: algebra.grlex_le_refl
Proof state before:
n : ℕ
a : Variables n order.GrLex
⊢ if Order.lex a a then True else False
Tactic:
split
Proof state after:
case inl
n : ℕ
a : Variables n order.GrLex
h✝ : Order.lex a a
⊢ True

case inr
n : ℕ
a : Variables n order.GrLex
h✝ : ¬Order.lex a a
⊢ False
Theorem: algebra.grlex_le_refl
Proof state before:
case inl
n : ℕ
a : Variables n order.GrLex
h✝ : Order.lex a a
⊢ True

case inr
n : ℕ
a : Variables n order.GrLex
h✝ : ¬Order.lex a a
⊢ False
Tactic:
simp [lex_le_refl]
Proof state after:
case inr
n : ℕ
a : Variables n order.GrLex
h✝ : ¬Order.lex a a
⊢ False
Theorem: algebra.grlex_le_refl
Proof state before:
case inr
n : ℕ
a : Variables n order.GrLex
h✝ : ¬Order.lex a a
⊢ False
Tactic:
simp [lex_le_refl] at *
Proof state after:
no goals
Theorem: algebra.grlex_le_trans
Proof state before:
n : ℕ
⊢ ∀ (a b c : Variables n order.GrLex), Order.grlex a b → Order.grlex b c → Order.grlex a c
Tactic:
intros a b c ab bc
Proof state after:
n : ℕ
a b c : Variables n order.GrLex
ab : Order.grlex a b
bc : Order.grlex b c
⊢ Order.grlex a c
Theorem: algebra.grlex_le_trans
Proof state before:
n : ℕ
a b c : Variables n order.GrLex
ab : Order.grlex a b
bc : Order.grlex b c
⊢ Order.grlex a c
Tactic:
simp [Order.grlex]
Proof state after:
n : ℕ
a b c : Variables n order.GrLex
ab : Order.grlex a b
bc : Order.grlex b c
⊢ if Order.grlex.elem_sum a < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False
Theorem: algebra.grlex_le_trans
Proof state before:
n : ℕ
a b c : Variables n order.GrLex
ab : Order.grlex a b
bc : Order.grlex b c
⊢ if Order.grlex.elem_sum a < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False
Tactic:
simp [Order.grlex] at ab bc
Proof state after:
n : ℕ
a b c : Variables n order.GrLex
ab :
  if Order.grlex.elem_sum a < Order.grlex.elem_sum b then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
⊢ if Order.grlex.elem_sum a < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False
Theorem: algebra.grlex_le_trans
Proof state before:
n : ℕ
a b c : Variables n order.GrLex
ab :
  if Order.grlex.elem_sum a < Order.grlex.elem_sum b then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
⊢ if Order.grlex.elem_sum a < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False
Tactic:
split <;> simp
Proof state after:
case inr
n : ℕ
a b c : Variables n order.GrLex
ab :
  if Order.grlex.elem_sum a < Order.grlex.elem_sum b then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
⊢ if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False
Theorem: algebra.grlex_le_trans
Proof state before:
case inr
n : ℕ
a b c : Variables n order.GrLex
ab :
  if Order.grlex.elem_sum a < Order.grlex.elem_sum b then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
⊢ if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False
Tactic:
split at ab
Proof state after:
case inr.inl
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝ : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
⊢ if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False

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

case inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False
Tactic:
split at bc <;> split
Proof state after:
case inr.inl.inl.inl
n : ℕ
a b c : Variables n order.GrLex
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
h✝¹ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
h✝ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
⊢ if Order.lex a c then True else False

case inr.inl.inl.inr
n : ℕ
a b c : Variables n order.GrLex
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
h✝¹ : Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : True
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
⊢ False

case inr.inl.inr.inl
n : ℕ
a b c : Variables n order.GrLex
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝ : Order.grlex.elem_sum a = Order.grlex.elem_sum c
⊢ if Order.lex a c then True else False

case inr.inl.inr.inr
n : ℕ
a b c : Variables n order.GrLex
h✝³ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝² : Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : True
h✝¹ : ¬Order.grlex.elem_sum b < Order.grlex.elem_sum c
bc : if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝ : ¬Order.grlex.elem_sum a = Order.grlex.elem_sum c
⊢ False

case inr.inr
n : ℕ
a b c : Variables n order.GrLex
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
h✝¹ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum c
h✝ : ¬Order.grlex.elem_sum a < Order.grlex.elem_sum b
ab : if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False
⊢ if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False