Error implies scope satisfied

theorem error_implies_scope_satisfied {policy : Policy} {request : Request} {entities : Entities} {err : Error} :  evaluate policy.toExpr request entities = .error err →  evaluate policy.principalScope.toExpr request entities = .ok true ∧  evaluate policy.actionScope.toExpr request entities = .ok true ∧  evaluate policy.resourceScope.toExpr request entities = .ok true:= by  intro h₁  unfold Policy.toExpr at h₁  rcases (ways_and_can_error h₁) with h₂ | ⟨h₂, h₃⟩ | ⟨_, h₃⟩ | ⟨h₂, _, h₄⟩ <;> clear h₁  case _ =>    -- in this case, evaluating principal produced the error    exfalso; simp only [principal_scope_does_not_throw] at h₂  case _ =>    -- in this case, evaluating (action ∧ resource ∧ condition) produced the error    rcases (ways_and_can_error h₃) with h₄ | ⟨h₄, h₅⟩ | ⟨_, h₅⟩ | ⟨_, _, h₅⟩ <;> clear h₃    case _ =>      -- in this case, evaluating action produced the error      exfalso; simp only [action_scope_does_not_throw] at h₄    case _ =>      -- in this case, evaluating (resource ∧ condition) produced the error      rcases (ways_and_can_error h₅) with h₆ | ⟨h₆, _⟩ | ⟨_, h₇⟩ | ⟨_, h₇, _⟩ <;> clear h₅      case _ =>        -- in this case, evaluating resource produced the error        exfalso; simp only [resource_scope_does_not_throw] at h₆      case _ =>        -- in this case, evaluating condition produced the error        exact And.intro h₂ (And.intro h₄ h₆)      case _ =>        -- in this case, evaluating resource produced a non-boolean        exfalso        clear h₂        have h := resource_scope_produces_boolean policy request entities        apply produces_boolean_means_not_non_boolean (e := policy.resourceScope.toExpr) h h₇      case _ =>        -- in this case, evaluating condition produced a non-boolean        exact And.intro h₂ (And.intro h₄ h₇)    case _ =>      -- in this case, evaluating action produced a non-boolean      exfalso      have h := action_scope_produces_boolean policy request entities      apply produces_boolean_means_not_non_boolean (e := policy.actionScope.toExpr) h h₅    case _ =>      -- in this case, evaluating (resource ∧ condition) produced a non-boolean      exfalso      clear h₂      unfold producesNonBool at h₅      have h₄ := and_produces_bool_or_error policy.resourceScope.toExpr policy.condition.toExpr request entities      split at h₄ <;> simp at h₄      case _ h₆ => simp [h₆] at h₅      case _ h₆ => simp [h₆] at h₅  case _ =>    -- in this case, evaluating principal produced a non-boolean    exfalso    have h := principal_scope_produces_boolean policy request entities    apply produces_boolean_means_not_non_boolean (e := policy.principalScope.toExpr) h h₃  case _ =>    -- in this case, evaluating (action ∧ resource ∧ condition) produced a non-boolean    exfalso    unfold producesNonBool at h₄    generalize (Expr.and policy.resourceScope.toExpr policy.condition.toExpr) = resource_and_condition at h₂ h₄    have h₅ := and_produces_bool_or_error policy.actionScope.toExpr resource_and_condition request entities    split at h₅ <;> simp at h₅    case _ h₆ => simp [h₆] at h₄    case _ h₆ => simp [h₆] at h₄