Theorem: SSAScope.getT_some_get
Proof state before:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
headName : SSAVal
headτ : MLIRType δ
headVal : MLIRType.eval headτ
HInd :
  getT (headName, { fst := headτ, snd := headVal }).fst tail = some { fst := τ, snd := v } →
    get (headName, { fst := headτ, snd := headVal }).fst tail τ = some v
⊢ (headName, { fst := headτ, snd := headVal }).2 = { fst := τ, snd := v } →
    (if h : (headName, { fst := headτ, snd := headVal }).2.fst = τ then
        some
          (cast
            (_ :
              (match (headName, { fst := headτ, snd := headVal }).2.fst with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε σ
                | MLIRType.erased => Unit)
            (headName, { fst := headτ, snd := headVal }).2.snd)
      else none) =
      some v
Tactic:
simp at *
Proof state after:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
headName : SSAVal
headτ : MLIRType δ
headVal : MLIRType.eval headτ
HInd : getT headName tail = some { fst := τ, snd := v } → get headName tail τ = some v
⊢ headτ = τ →
    HEq headVal v →
      (if h : headτ = τ then
          some
            (cast
              (_ :
                (match (headName, { fst := headτ, snd := headVal }).2.fst with
                  | MLIRType.float a => Float
                  | MLIRType.int signedness sz => FinInt sz
                  | MLIRType.tensor1d => Tensor1D
                  | MLIRType.tensor2d => Tensor2D
                  | MLIRType.tensor4d => Tensor4D
                  | MLIRType.index => ℤ
                  | MLIRType.undefined a => Unit
                  | MLIRType.extended σ => ε σ
                  | MLIRType.erased => Unit) =
                  match τ with
                  | MLIRType.float a => Float
                  | MLIRType.int signedness sz => FinInt sz
                  | MLIRType.tensor1d => Tensor1D
                  | MLIRType.tensor2d => Tensor2D
                  | MLIRType.tensor4d => Tensor4D
                  | MLIRType.index => ℤ
                  | MLIRType.undefined a => Unit
                  | MLIRType.extended σ => ε σ
                  | MLIRType.erased => Unit)
              headVal)
        else none) =
        some v