Of Env preserves entity attr

theorem ofEnv_preserves_entity_attr  {Γ : TypeEnv} {εnv : SymEnv}  {rty : RecordType} {ety : EntityType}  (hεnv : εnv = SymEnv.ofEnv Γ)  (hattrs_exists : Γ.ets.attrs? ety = some rty)  (hwf : εnv.WellFormed) :  ∃ attrs : UnaryFunction,    εnv.entities.attrs ety = .some attrs ∧    UnaryFunction.WellFormed εnv.entities attrs ∧    attrs.argType = .entity ety ∧    attrs.outType = .record (Map.mk (TermType.ofRecordType rty.toList)):= by  simp only [EntitySchema.attrs?, Map.find?, Option.map_eq_some_iff] at hattrs_exists  split at hattrs_exists  case h_1 found_ety found_entry hfind =>    simp only [Option.some.injEq, exists_eq_left'] at hattrs_exists    -- The corresponding entity exists in `εnv`    have hety_exists :      Map.find? εnv.entities ety      = some (SymEntityData.ofEntityType ety found_entry)    := by      apply ofEnv_preserves_entity hεnv      simp [Map.find?, hfind]    have ⟨attrs, hattrs_exists2⟩ :      ∃ attrs : UnaryFunction, εnv.entities.attrs ety = .some attrs    := by simp [SymEntities.attrs, hety_exists]    have ⟨hwf_attrs, hty_arg_attrs⟩ := wf_εnv_implies_attrs_wf hwf hattrs_exists2    exists attrs    constructor    -- Entity type exists in `εnv.entities`    · assumption    -- Some well-formedness and well-typedness conditions    · simp only [hwf_attrs, hty_arg_attrs, true_and]      -- TODO: show that the `attrs.outType` is `TermType.ofRecordType rty.1`      simp only [        hety_exists,        SymEntities.attrs, SymEntityData.ofEntityType,        SymEntityData.ofStandardEntityType,        SymEntityData.ofStandardEntityType.attrsUUF,        SymEntityData.ofEnumEntityType,        SymEntityData.emptyAttrs,        Option.bind_some_fun,        Option.some.injEq,      ] at hattrs_exists2      split at hattrs_exists2 <;> simp only at hattrs_exists2      -- Standard entity types      · simp only [          ← hattrs_exists2,          UnaryFunction.outType, TermType.ofType,          TermType.record.injEq, Map.mk.injEq,        ]        simp only [EntitySchemaEntry.attrs] at hattrs_exists        simp [hattrs_exists, Map.deprecated_toList_def] -- `Map.deprecated_toList_def` is required because `TermType.ofType` is defined using `Map` internals      -- Enum entity types      · simp only [← hattrs_exists2, UnaryFunction.outType, TermType.ofType, TermType.record.injEq]        simp only [EntitySchemaEntry.attrs] at hattrs_exists        simp [← hattrs_exists, TermType.ofRecordType, Map.empty]  case _ =>    simp at hattrs_exists