no goals
ι : Type ?u.425241
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ length (List.erase l a) + 1 = length l
rw [erase_eq_eraseP, length_eraseP_add_one h (decide_eq_true rfl)]