Theorem: List.ne_mem_cons (MLIR/Util/List.lean)

State before:
α : Type u_1
x a : α
as : List α
⊢ ¬x ∈ a :: as → x ≠ a ∧ ¬x ∈ as
Tactic:
intros Hne
State after:
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
⊢ x ≠ a ∧ ¬x ∈ as

State before:
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
⊢ x ≠ a ∧ ¬x ∈ as
Tactic:
apply And.intro <;> intros _ <;> apply Hne
State after:
case left
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x = a
⊢ x ∈ a :: as

case right
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x ∈ as
⊢ x ∈ a :: as

State before:
case left
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x = a
⊢ x ∈ a :: as

case right
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x ∈ as
⊢ x ∈ a :: as
Tactic:
. subst x; constructor
State after:
case right
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x ∈ as
⊢ x ∈ a :: as

State before:
case right
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x ∈ as
⊢ x ∈ a :: as
Tactic:
. constructor; assumption
State after:
no goals