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

State before:
n : ℕ
⊢ ∀ (a b : Variables n order.Lex), Order.lex_lt a b ↔ Order.lex a b ∧ ¬Order.lex b a
Tactic:
intros v₁ v₂
State after:
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex_lt v₁ v₂ ↔ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁

State before:
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex_lt v₁ v₂ ↔ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁
Tactic:
apply Iff.intro
State after:
case mp
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex_lt v₁ v₂ → Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁

case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex_lt v₁ v₂

State before:
case mp
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex_lt v₁ v₂ → Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁

case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex_lt v₁ v₂
Tactic:
repeat (
  rw [Order.lex_lt]
  simp
)
State after:
no goals

State before:
case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex_lt v₁ v₂
Tactic:
(
rw [Order.lex_lt]
simp
)
State after:
no goals

State before:
case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex_lt v₁ v₂
Tactic:
rw [Order.lex_lt]
State after:
case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁

State before:
case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁
Tactic:
simp
State after:
no goals