Determining erroring disjoint when unique ids

theorem determining_erroring_disjoint_when_unique_ids (request : Request) (entities : Entities) (policies : Policies) :  PolicyIdsUnique policies →    ((isAuthorized request entities policies).determiningPolicies ∩ (isAuthorized request entities policies).erroringPolicies).isEmpty:= by  intro  rw [Set.empty_iff_not_exists]  simp only [Set.mem_inter_iff, not_exists, not_and]  rw [determiningPolicies_of]  intro _ h_det h_err  unfold isAuthorized satisfiedPolicies errorPolicies satisfiedWithEffect errored at *  simp only [    Bool.and_eq_true, beq_iff_eq, apply_ite, ite_self, Set.mem_make, List.mem_filterMap, Option.ite_none_right_eq_some, Option.some.injEq  ] at *  -- Extract the determining policy  obtain ⟨p₁, _, ⟨_, _⟩, _⟩ := h_det  -- Extract the erroring policy, and the fact that it is erroring  obtain ⟨p₂, _, h₂, _⟩ := h_err  -- They're the same policy, leading to a contradiction  have heq : p₁ = p₂ := by grind [PolicyIdsUnique]  subst heq  have l₁ : ∀ p, hasError p request entities → ¬satisfied p request entities := by    unfold satisfied hasError    intro    split <;> rename_i _ s <;> simp [s]  have : ¬satisfied _ request entities := l₁ _ h₂  contradiction