Theorem: List.remove_singleton_of_ne (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.175397 → Type ?u.175399
α : Type u_1
β : Type ?u.175405
inst✝¹ : Monad m
inst✝ : DecidableEq α
p q : α
h : p ≠ q
⊢ remove q [p] = [p]
Tactic:
simp_all [List.remove, Ne.symm]
State after:
no goals