Batched evaluate eq evaluate

theorem batched_evaluate_eq_evaluate  {x : TypedExpr}  {req : Request}  {es : Entities}  {env : TypeEnv} :  EntityLoader.WellBehaved es loader →  TypedExpr.WellTyped env x →  InstanceOfWellFormedEnvironment req es env →  (Residual.evaluate (batchedEvaluate x req loader iters) req es).toOption = (evaluate x.toExpr req es).toOption := by  simp only [batchedEvaluate]  intro h₁ h₂ h₃  have h₄ := (direct_request_and_entities_refine req es)   have h₅ : Residual.WellTyped env (TypedExpr.toResidual x) := by {    apply conversion_preserves_typedness    exact h₂  }  rw [conversion_preserves_evaluation x req es]  rw [partial_evaluate_is_sound h₅ h₃ h₄]   have h₆ : Residual.WellTyped env (TPE.evaluate x.toResidual req.asPartialRequest Map.empty) := by    apply partial_eval_preserves_well_typed h₃ _ h₅    . constructor      . apply as_partial_request_refines      . apply any_refines_empty_entities  have h₇: RequestAndEntitiesRefine req es req.asPartialRequest Map.empty := by    constructor    . apply as_partial_request_refines    . apply any_refines_empty_entities   rw [batched_evaluate_loop_eq_evaluate es h₁ h₆ h₇ h₃]  rw [←partial_evaluate_is_sound h₅ h₃ h₇]  rw [←partial_evaluate_is_sound h₅ h₃ h₄]