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

State before:
α : Type u_1
inst✝ : BEq α
⊢ ∀ (l : List α), (l == []) = true → l = []
Tactic:
intros l h
State after:
α : Type u_1
inst✝ : BEq α
l : List α
h : (l == []) = true
⊢ l = []

State before:
α : Type u_1
inst✝ : BEq α
l : List α
h : (l == []) = true
⊢ l = []
Tactic:
cases l
State after:
case nil
α : Type u_1
inst✝ : BEq α
h : ([] == []) = true
⊢ [] = []

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

State before:
case nil
α : Type u_1
inst✝ : BEq α
h : ([] == []) = true
⊢ [] = []

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

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