Extract? implies enum complete

theorem extract?_implies_enum_complete  {env : Env} {εnv : SymEnv} {I : Interpretation} {exprs : List Expr}  (hext : env = εnv.extract? exprs I) :  Env.EnumCompleteFor env εnv:= by  simp only [    SymEnv.extract?, SymEnv.concretize?,    bind, Option.bind,  ] at hext  split at hext  contradiction  rename_i req hreq  simp only at hext  split at hext  contradiction  rename_i entities hents  simp only [Option.some.injEq] at hext  simp only [hext, Env.EnumCompleteFor]  intros uid δ eids hfind_uid_ty heids heid  have huid := sym_entities_entityUIDs_include_enums (Interpretation.repair (footprints exprs εnv) εnv I) hfind_uid_ty heids heid  replace ⟨eds, heds, hents⟩ := concretize?_εs_some_eq hents  simp only [←hents]  have ⟨⟨uid', data⟩, hmem_uid'_data, huid'⟩  := List.mapM_some_implies_all_some heds uid    ((Set.mem_union _ _ uid).mpr (Or.intro_right _ huid))  have ⟨δ, d, hfind_uid_ty, hd, heq_uid'⟩ := concretize?_entityData?_some_eq huid'  simp only [Prod.mk.injEq] at heq_uid'  simp only [←heq_uid'.1] at hmem_uid'_data huid'  exists data  rw [← Map.list_find?_iff_make_find?]  apply List.find?_unique_entry  · intros x hmem heq_fst    have ⟨uid', data'⟩ := x    simp only [beq_iff_eq] at heq_fst    simp only [heq_fst]    have ⟨uid'', hmem_uid'', huid''⟩ := List.mapM_some_implies_all_from_some heds (uid', data') hmem    have ⟨_, d', hfind_uid_ty', hd', heq_uid''⟩ := concretize?_entityData?_some_eq huid''    simp only [Prod.mk.injEq] at heq_uid''    simp only [heq_uid''.1, heq_fst] at hd' hfind_uid_ty'    simp only [hfind_uid_ty, Option.some.injEq] at hfind_uid_ty'    simp only [←hfind_uid_ty'] at hd'    simp only [hd', Option.some.injEq] at hd    simp only [←heq_uid''.2, hd, heq_uid'.2]  · exact hmem_uid'_data  · simp