Error of mem erroring Policies

theorem error_of_mem_erroringPolicies {ps : Policies} {request : Request} {entities : Entities} {pid : PolicyID}  (h : pid ∈ (isAuthorized request entities ps).erroringPolicies) :  ∃ p ∈ ps, p.id = pid ∧ ∃ e, evaluate p.toExpr request entities = .error e:= by  unfold isAuthorized errorPolicies errored at h  simp only [apply_ite, ite_self, Set.mem_make, List.mem_filterMap,    Option.ite_none_right_eq_some, Option.some.injEq] at h  obtain ⟨p, hp, herr, hid⟩ := h  refine ⟨p, hp, hid, ?_⟩  cases heq : evaluate p.toExpr request entities with  | ok v => simp [hasError, heq] at herr  | error e => exact ⟨e, rfl⟩