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

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
State after:
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex_lt a b ↔ Order.grlex a b ∧ ¬Order.grlex b a

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

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

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

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

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