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

State before:
n : ℕ
⊢ ∀ (a : Variables n order.GrLex), Order.grlex a a
Tactic:
intros a
State after:
n : ℕ
a : Variables n order.GrLex
⊢ Order.grlex a a

State before:
n : ℕ
a : Variables n order.GrLex
⊢ Order.grlex a a
Tactic:
simp [Order.grlex]
State after:
n : ℕ
a : Variables n order.GrLex
⊢ if Order.lex a a then True else False

State before:
n : ℕ
a : Variables n order.GrLex
⊢ if Order.lex a a then True else False
Tactic:
split
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

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]
State after:
case inr
n : ℕ
a : Variables n order.GrLex
h✝ : ¬Order.lex a a
⊢ False

State before:
case inr
n : ℕ
a : Variables n order.GrLex
h✝ : ¬Order.lex a a
⊢ False
Tactic:
simp [lex_le_refl] at *
State after:
no goals