Theorem: SSAScope.get_some_getT
Proof state before:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
x✝ : Option ((τ : MLIRType δ) × MLIRType.eval τ)
v'✝ : MLIRType.eval τ
Hget : getT name scope = some { fst := τ, snd := v'✝ }
H :
  cast
      (_ :
        (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) =
          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)
      v'✝ =
    v
⊢ getT name scope = some { fst := τ, snd := v }
Tactic:
rw [←H, Hget]
Proof state after:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
x✝ : Option ((τ : MLIRType δ) × MLIRType.eval τ)
v'✝ : MLIRType.eval τ
Hget : getT name scope = some { fst := τ, snd := v'✝ }
H :
  cast
      (_ :
        (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) =
          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)
      v'✝ =
    v
⊢ some { fst := τ, snd := v'✝ } =
    some
      { fst := τ,
        snd :=
          cast
            (_ :
              (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) =
                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)
            v'✝ }