Theorem: SSAScope.set_commutes
Proof state before:
case nil.h1
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
name : SSAVal
τ'' : MLIRType δ
Hne : name ≠ v
⊢ (if h : τ' = τ'' then
      some
        (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)
          val')
    else none) =
    if v = name then
      if h : τ = τ'' then
        some
          (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)
            val)
      else none
    else
      if h : τ' = τ'' then
        some
          (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)
            val')
      else none
Tactic:
byCases Hτ: τ' = τ'' <;> simp [Hne.symm]
Proof state after:
no goals