Batched authorize decision eq authorize

theorem batched_authorize_decision_eq_authorize  {schema : Schema} {policies : List Policy} {req : Request}  {es : Entities} {response : TPE.Response} {d : Decision} :  EntityLoader.WellBehaved es loader →  schema.validateWellFormed = .ok () →  validateEntities schema es = .ok () →  batchedAuthorize schema policies req loader iters = .ok response →  response.decision = some d →  (Spec.isAuthorized req es policies).decision = d:= by  intro h_loader h_schema_wf h_entities h_batched h_dec  simp only [batchedAuthorize] at h_batched  cases h_mapM : policies.mapM (λ p =>    ResidualPolicy.mk p.id p.effect <$> evaluatePolicy schema p req.asPartialRequest Map.empty) with  | error e => simp [h_mapM, bind_pure_comp] at h_batched  | ok residualPolicies =>    simp only [bind_pure_comp, h_mapM, Except.map_ok, Except.ok.injEq] at h_batched    subst h_batched    rw [List.mapM_ok_iff_forall₂] at h_mapM    match policies, h_mapM with    | [], .nil =>      have h_dec' : (isAuthorizedFromResiduals []).decision = some .deny := by        simp [isAuthorizedFromResiduals, isAuthorizedFromResiduals.satisfiedPolicies, isAuthorizedFromResiduals.residualPolicies]      apply residuals_decision_agrees .nil      unfold batchedAuthorizeLoop at h_dec      simpa [h_dec'] using h_dec    | p :: _, .cons h_first h_rest =>      have ⟨r, h_ep⟩ : ∃ r, evaluatePolicy schema p req.asPartialRequest Map.empty = .ok r := by        cases h_ep : evaluatePolicy schema p req.asPartialRequest Map.empty <;>          simp [h_ep] at ⊢ h_first      obtain ⟨env, h_schema_env, h_wf⟩ :=        evaluatePolicy_ok_implies_well_formed_env h_ep h_schema_wf h_entities      have h_ref : RequestAndEntitiesRefine req es req.asPartialRequest Map.empty :=        ⟨as_partial_request_refines, any_refines_empty_entities⟩      exact batched_authorize_loop_decision_agrees es h_loader        (evaluatePolicies_equiv_and_well_typed (.cons h_first h_rest) h_schema_env h_wf h_ref)        h_ref h_wf h_dec