Ways and can error

theorem ways_and_can_error {e₁ e₂ : Expr} {request : Request} {entities : Entities} {err : Error} :  evaluate (Expr.and e₁ e₂) request entities = .error err →  evaluate e₁ request entities = .error err ∨  (evaluate e₁ request entities = .ok true ∧ evaluate e₂ request entities = .error err) ∨  (err = Error.typeError ∧ producesNonBool e₁ request entities) ∨  (err = Error.typeError ∧ evaluate e₁ request entities = .ok true ∧ producesNonBool e₂ request entities):= by  intro h₁  cases h_e₁ : (evaluate e₁ request entities) <;> simp [h_e₁, producesNonBool]  case ok val =>    cases val <;>    simp [h_e₁, evaluate, Result.as, Coe.coe, Value.asBool] at h₁ <;>    simp [h₁]    case prim prim =>      cases prim <;>      simp at h₁ <;>      simp [h₁]      case bool b =>        cases b with        | true =>          simp only [true_and]          simp only [reduceCtorEq] at h₁          cases h_e₂ : (evaluate e₂ request entities) with          | ok val =>            cases val <;>            simp [h_e₂] at h₁ <;>            simp [h₁]            case prim prim =>              cases prim <;>              simp at h₁ <;>              simp [h₁]          | error e =>            simp only [↓reduceIte, h_e₂, Except.map_error, Except.error.injEq] at h₁            simp only [h₁, and_false, or_false]        | false => simp at h₁  case error e =>    simp [h_e₁, evaluate, Result.as, Coe.coe, Value.asBool] at h₁    simp [h₁]