Map M' error implies exists error

public theorem mapM'_error_implies_exists_error {α β γ} {f : α → Except γ β} {xs : List α} {e : γ} :  List.mapM' f xs = .error e → ∃ x ∈ xs, f x = .error e:= by  intro h₁  cases xs  case nil =>    simp only [mapM'_nil, pure, Except.pure, reduceCtorEq] at h₁  case cons xhd xtl =>    simp only [mapM'_cons] at h₁    cases h₂ : f xhd <;>    simp only [h₂, Except.bind_ok, Except.bind_err, Except.error.injEq] at h₁    case error =>      subst h₁      exists xhd      simp only [mem_cons, true_or, h₂, and_self]    case ok =>      cases h₃ : mapM' f xtl <;>      simp only [h₃, Except.bind_ok, Except.bind_err, Except.error.injEq, pure, Except.pure, reduceCtorEq] at h₁      subst h₁      replace h₃ := mapM'_error_implies_exists_error h₃      replace ⟨x, h₃⟩ := h₃      exists x      simp only [mem_cons, h₃, or_true, and_self]