Opt compile correctness get Attr

theorem Opt.compile.correctness.getAttr (expr : Expr) (attr : Attr) (εnv : SymEnv) :  Opt.compile (.getAttr expr attr) εnv = (do    let term ← SymCC.compile (.getAttr expr attr) εnv    let footprint := footprint (.getAttr expr attr) εnv    .ok { term, footprint }  ):= by  simp [Opt.compile, SymCC.compile, footprint]  rw [Opt.compile.correctness expr εnv]  cases h₁ : SymCC.compile expr εnv <;> simp  case ok t =>    rw [Opt.compileGetAttr.correctness]    simp only [Opt.CompileResult.mapTerm, bind_assoc, Except.bind_ok]    simp_do_let compileGetAttr (Factory.option.get t) attr εnv.entities ; rename_i t' h₂    simp only [Except.ok.injEq, Opt.CompileResult.mk.injEq, true_and]    rw [Opt.directFootprint.correctness (t := Factory.ifSome t t') (x := .getAttr expr attr) (εnv := εnv)]    · apply Data.Set.union_comm    · -- here we have to show that the `t` and `x` arguments we chose for `Opt.directFootprint.correctness` in the `rw` above correspond to each other correctly      simp [SymCC.compile, h₁, h₂]