Record value contains evaluated attrs

theorem record_value_contains_evaluated_attrs {rxs : List (Attr × Expr)} {rvs : Map Attr Value} {a : Attr} {av : Value} {request : Request} {entities : Entities}  (he : evaluate (.record rxs) request entities = .ok (.record rvs))  (hfv : rvs.find? a = some av) :  ∃ x, (Map.make rxs).find? a = some x ∧ evaluate x request entities = .ok av:= by  simp only [evaluate] at he  cases he₁ : rxs.mapM₂ fun x => bindAttr x.1.fst (evaluate x.1.snd request entities) <;>    simp only [he₁, Except.bind_err, reduceCtorEq, Except.bind_ok, Except.ok.injEq, Value.record.injEq] at he  subst rvs  rename_i rvs'  replace he₁ : List.Forallᵥ (λ x y => evaluate x request entities = Except.ok y) rxs rvs' := by    simp only [List.forallᵥ_def]    rw [List.mapM₂_eq_mapM λ (x : Attr × Expr) => bindAttr x.fst (evaluate x.snd request entities)] at he₁    rw [List.mapM_ok_iff_forall₂] at he₁    apply List.Forall₂.imp _ he₁    intro x y h    simp only [bindAttr] at h    simp_do_let (evaluate x.snd request entities) as hx at h    simp only [pure, Except.pure, Except.ok.injEq] at h    simp only [←h, and_self]  replace he₁ := List.canonicalize_preserves_forallᵥ _ _ _ he₁  have hfv : List.find? (λ x => x.fst == a) (Map.make rvs').toList = some (a, av) := by    simp only [Map.find?] at hfv    split at hfv <;> simp only [Option.some.injEq, reduceCtorEq] at hfv    subst hfv    rename_i a' _ hfv    rw [(by simpa using List.find?_some hfv : a' = a)] at hfv    exact hfv  rw [List.forallᵥ_def] at he₁  rw [Map.toList_make_eq_canonicalize] at hfv  have ⟨(a', x), he₂, he₃⟩ := List.forall₂_implies_all_right he₁ (a, av) (List.mem_of_find?_eq_some hfv)  simp only at he₃ ; replace ⟨_, he₃⟩ := he₃ ; subst a'  exists x  simp [Map.find?, Map.toList_make_eq_canonicalize, List.mem_of_sortedBy_implies_find? he₂ (List.canonicalize_sortedBy _ _), he₃]