Theorem: SSAScope.get_none_getT (MLIR/Semantics/SSAEnv.lean)

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
⊢ (∀ (τ : MLIRType δ), get name scope τ = none) → getT name scope = none
Tactic:
induction scope <;> simp
State after:
case cons
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
head✝ : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail✝ : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : (∀ (τ : MLIRType δ), get name tail✝ τ = none) → getT name tail✝ = none
⊢ (∀ (τ : MLIRType δ),
      (if head✝.fst = name then
          if h : head✝.2.fst = τ then
            some
              (cast
                (_ :
                  (match head✝.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)
                head✝.2.snd)
          else none
        else get name tail✝ τ) =
        none) →
    (if head✝.fst = name then some head✝.2 else getT name tail✝) = none

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : (∀ (τ : MLIRType δ), get name tail τ = none) → getT name tail = none
⊢ (∀ (τ : MLIRType δ),
      (if head.fst = name then
          if h : head.2.fst = τ then
            some
              (cast
                (_ :
                  (match head.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)
                head.2.snd)
          else none
        else get name tail τ) =
        none) →
    (if head.fst = name then some head.2 else getT name tail) = none
Tactic:
case cons head tail HInd =>
byCases Hname: head.fst = name <;> try assumption
State after:
no goals

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : (∀ (τ : MLIRType δ), get name tail τ = none) → getT name tail = none
⊢ (∀ (τ : MLIRType δ),
      (if head.fst = name then
          if h : head.2.fst = τ then
            some
              (cast
                (_ :
                  (match head.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)
                head.2.snd)
          else none
        else get name tail τ) =
        none) →
    (if head.fst = name then some head.2 else getT name tail) = none
Tactic:
byCases Hname: head.fst = name <;> try assumption
State after:
no goals

State before:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : (∀ (τ : MLIRType δ), get name tail τ = none) → getT name tail = none
Hname : ¬head.fst = name
⊢ (∀ (τ : MLIRType δ), get name tail τ = none) → getT name tail = none
Tactic:
assumption
State after:
no goals