Theorem: SSAScope.set_commutes
Proof state before:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ equiv [(v', { fst := τ', snd := val' }), (v, { fst := τ, snd := val })]
    [(v, { fst := τ, snd := val }), (v', { fst := τ', snd := val' })]
Tactic:
simp [equiv]
Proof state after:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ ∀ (name : SSAVal) (τ_1 : MLIRType δ),
    (if v' = name then
        if h : τ' = τ_1 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 τ_1 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 v = name then
          if h : τ = τ_1 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 τ_1 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 none) =
      if v = name then
        if h : τ = τ_1 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 τ_1 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 v' = name then
          if h : τ' = τ_1 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 τ_1 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 none