Theorem: polynomial.cons_non_empty (Diploma/Polynomials/Groebner.lean)

State before:
α : Type u_1
inst✝ : BEq α
a b : List α
h : ¬(b == []) = true
⊢ ¬(a ++ b == []) = true
Tactic:
simp at *
State after:
α : Type u_1
inst✝ : BEq α
a b : List α
h : (b == []) = false
⊢ (a ++ b == []) = false

State before:
α : Type u_1
inst✝ : BEq α
a b : List α
h : (b == []) = false
⊢ (a ++ b == []) = false
Tactic:
cases a
State after:
case nil
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
⊢ ([] ++ b == []) = false

case cons
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝ ++ b == []) = false

State before:
case nil
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
⊢ ([] ++ b == []) = false

case cons
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝ ++ b == []) = false
Tactic:
simp [h]
State after:
case cons
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝ ++ b == []) = false

State before:
case cons
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝ ++ b == []) = false
Tactic:
rfl
State after:
no goals