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

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.181909 → Type ?u.181911
α : Type u_1
β : Type ?u.181917
inst✝¹ : Monad m
inst✝ : DecidableEq α
l : List α
a b : α
ne : a ≠ b
⊢ remove b (a :: l) = a :: remove b l
Tactic:
simp_all [remove]
State after:
no goals