Theorem: polynomial.minus_lt (Diploma/Algebra/PolynomialHelpers.lean)

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
⊢ (m_cmp (Polynomial.lt p) (Polynomial.lt (p - Polynomial.Lt p)) == Ordering.lt) = true
Tactic:
simp [Polynomial.Lt, Polynomial.lt, not_empty]
State after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
⊢ (m_cmp (Std.RBSet.min! p)
        (if Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false then
          Std.RBSet.min! (p - Polynomial.single (Std.RBSet.min! p))
        else (1, get_variables n)) ==
      Ordering.lt) =
    true

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
⊢ (m_cmp (Std.RBSet.min! p)
        (if Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false then
          Std.RBSet.min! (p - Polynomial.single (Std.RBSet.min! p))
        else (1, get_variables n)) ==
      Ordering.lt) =
    true
Tactic:
split
State after:
case inl
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (Std.RBSet.min! (p - Polynomial.single (Std.RBSet.min! p))) == Ordering.lt) = true

case inr
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : ¬Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (1, get_variables n) == Ordering.lt) = true

State before:
case inl
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (Std.RBSet.min! (p - Polynomial.single (Std.RBSet.min! p))) == Ordering.lt) = true

case inr
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : ¬Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (1, get_variables n) == Ordering.lt) = true
Tactic:
sorry
State after:
case inr
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : ¬Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (1, get_variables n) == Ordering.lt) = true

State before:
case inr
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : ¬Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (1, get_variables n) == Ordering.lt) = true
Tactic:
sorry
State after:
no goals