Theorem: run_TopM_get_ (MLIR/Semantics/Semantics.lean)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env : SSAEnv Δ
ty : MLIRType Δ
name : SSAVal
⊢ run (TopM.get ty name) env =
    Except.ok
      (match SSAEnv.get name ty env with
        | some v => v
        | none => default,
        env)
Tactic:
simp[TopM.get, run, StateT.run, StateT.get, bind, StateT.bind, Except.bind, pure,
Except.pure, StateT.pure]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env : SSAEnv Δ
ty : MLIRType Δ
name : SSAVal
⊢ (match SSAEnv.get name ty env with
      | some v => fun s => Except.ok (v, s)
      | none => fun s => Except.ok (default, s))
      env =
    Except.ok
      (match SSAEnv.get name ty env with
        | some v => v
        | none => default,
        env)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env : SSAEnv Δ
ty : MLIRType Δ
name : SSAVal
⊢ (match SSAEnv.get name ty env with
      | some v => fun s => Except.ok (v, s)
      | none => fun s => Except.ok (default, s))
      env =
    Except.ok
      (match SSAEnv.get name ty env with
        | some v => v
        | none => default,
        env)
Tactic:
cases H:SSAEnv.get name ty env <;> simp
State after:
no goals