Theorem: List.removeAllEq_singleton_nonelem_eq (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (xs : List α) (x : α), ¬x ∈ xs → removeAllEq xs [x] = xs
Tactic:
intro xs x hnmem
State after:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x : α
hnmem : ¬x ∈ xs
⊢ removeAllEq xs [x] = xs

State before:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x : α
hnmem : ¬x ∈ xs
⊢ removeAllEq xs [x] = xs
Tactic:
induction xs with
| nil => rfl
| cons x' xs ih =>
  rw [removeAllEq_singleton_hd_neq]
  congr
  apply ih
  intro hneg
  apply hnmem
  apply Mem.tail
  . exact hneg
  . intro hneg'
    rw [hneg'] at hnmem
    apply hnmem
    apply Mem.head
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
hnmem : ¬x ∈ []
⊢ removeAllEq [] [x] = []
Tactic:
rfl
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ removeAllEq (x' :: xs) [x] = x' :: xs
Tactic:
rw [removeAllEq_singleton_hd_neq]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' :: removeAllEq xs [x] = x' :: xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' :: removeAllEq xs [x] = x' :: xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
congr
State after:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ removeAllEq xs [x] = xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x

State before:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ removeAllEq xs [x] = xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
apply ih
State after:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ ¬x ∈ xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x

State before:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ ¬x ∈ xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
intro hneg
State after:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ False

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x

State before:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ False

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
apply hnmem
State after:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ x ∈ x' :: xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x

State before:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ x ∈ x' :: xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
apply Mem.tail
State after:
case cons.e_tail.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ Mem x xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x

State before:
case cons.e_tail.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ Mem x xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
. exact hneg
State after:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x

State before:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
. intro hneg'
  rw [hneg'] at hnmem
  apply hnmem
  apply Mem.head
State after:
no goals

State before:
case cons.e_tail.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ Mem x xs
Tactic:
exact hneg
State after:
no goals

State before:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
intro hneg'
State after:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg' : x' = x
⊢ False

State before:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg' : x' = x
⊢ False
Tactic:
rw [hneg'] at hnmem
State after:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x :: xs
hneg' : x' = x
⊢ False

State before:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x :: xs
hneg' : x' = x
⊢ False
Tactic:
apply hnmem
State after:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x :: xs
hneg' : x' = x
⊢ x ∈ x :: xs

State before:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x :: xs
hneg' : x' = x
⊢ x ∈ x :: xs
Tactic:
apply Mem.head
State after:
no goals