Theorem: Ctx.shift_set_comm (STLC.lean)

State before:
ty : Ty
ctx : Ctx
x : Nat
⊢ (↥ctx)[x + 1 ↦ ty] = ↥ctx[x ↦ ty]
Tactic:
funext
State after:
case h
ty : Ty
ctx : Ctx
x x✝ : Nat
⊢ (↥ctx)[x + 1 ↦ ty] x✝ = ↥ctx[x ↦ ty] x✝

State before:
case h
ty : Ty
ctx : Ctx
x x✝ : Nat
⊢ (↥ctx)[x + 1 ↦ ty] x✝ = ↥ctx[x ↦ ty] x✝
Tactic:
simp [shift, set]
State after:
case h
ty : Ty
ctx : Ctx
x x✝ : Nat
⊢ (if x✝ = x + 1 then some ty
    else
      match x✝ with
      | 0 => none
      | Nat.succ x => ctx x) =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1

State before:
case h
ty : Ty
ctx : Ctx
x x✝ : Nat
⊢ (if x✝ = x + 1 then some ty
    else
      match x✝ with
      | 0 => none
      | Nat.succ x => ctx x) =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1
Tactic:
split
State after:
case h.inl
ty : Ty
ctx : Ctx
x x✝ : Nat
h✝ : x✝ = x + 1
⊢ some ty =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1

case h.inr
ty : Ty
ctx : Ctx
x x✝ : Nat
h✝ : ¬x✝ = x + 1
⊢ (match x✝ with
    | 0 => none
    | Nat.succ x => ctx x) =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1

State before:
case h.inl
ty : Ty
ctx : Ctx
x x✝ : Nat
h✝ : x✝ = x + 1
⊢ some ty =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1
Tactic:
simp [*]
State after:
no goals

State before:
case h.inr
ty : Ty
ctx : Ctx
x x✝ : Nat
h✝ : ¬x✝ = x + 1
⊢ (match x✝ with
    | 0 => none
    | Nat.succ x => ctx x) =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1
Tactic:
split <;> simp_all
State after:
no goals