Theorem: HMem.Encoding.decodeOp_inv (HMem/Encoding/Basic.lean)

State before:
α : Type u_1
inst✝ : Coding α Memory
x✝ : (Fin 0 → Bool) → α
⊢ decodeOp (encodeOp x✝) = some x✝
Tactic:
simpa [decodeOp, encodeOp]
using funext λ _ ↦ congrArg _ (funext finZeroElim)
State after:
no goals

State before:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
⊢ decodeOp (encodeOp g) = some g
Tactic:
simp [decodeOp, encodeOp, decodeOp_inv (N := N)]
State after:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
⊢ (fun g_1 =>
      match g_1 0 with
      | false => g (Fin.cons false (Fin.tail g_1))
      | true => g (Fin.cons true (Fin.tail g_1))) =
    g

State before:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
⊢ (fun g_1 =>
      match g_1 0 with
      | false => g (Fin.cons false (Fin.tail g_1))
      | true => g (Fin.cons true (Fin.tail g_1))) =
    g
Tactic:
apply funext
State after:
case h
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
⊢ ∀ (x : Fin (N + 1) → Bool),
    (match x 0 with
      | false => g (Fin.cons false (Fin.tail x))
      | true => g (Fin.cons true (Fin.tail x))) =
      g x

State before:
case h
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
⊢ ∀ (x : Fin (N + 1) → Bool),
    (match x 0 with
      | false => g (Fin.cons false (Fin.tail x))
      | true => g (Fin.cons true (Fin.tail x))) =
      g x
Tactic:
intro x
State after:
case h
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
⊢ (match x 0 with
    | false => g (Fin.cons false (Fin.tail x))
    | true => g (Fin.cons true (Fin.tail x))) =
    g x

State before:
case h
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
⊢ (match x 0 with
    | false => g (Fin.cons false (Fin.tail x))
    | true => g (Fin.cons true (Fin.tail x))) =
    g x
Tactic:
match h:x 0 with
| true =>
  apply congrArg g
  exact h ▸ Fin.cons_self_tail _
| false =>
  apply congrArg g
  exact h ▸ Fin.cons_self_tail _
State after:
no goals

State before:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
h : x 0 = true
⊢ (match true with
    | false => g (Fin.cons false (Fin.tail x))
    | true => g (Fin.cons true (Fin.tail x))) =
    g x
Tactic:
apply congrArg g
State after:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
h : x 0 = true
⊢ Fin.cons true (Fin.tail x) = x

State before:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
h : x 0 = true
⊢ Fin.cons true (Fin.tail x) = x
Tactic:
exact h ▸ Fin.cons_self_tail _
State after:
no goals

State before:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
h : x 0 = false
⊢ (match false with
    | false => g (Fin.cons false (Fin.tail x))
    | true => g (Fin.cons true (Fin.tail x))) =
    g x
Tactic:
apply congrArg g
State after:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
h : x 0 = false
⊢ Fin.cons false (Fin.tail x) = x

State before:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
h : x 0 = false
⊢ Fin.cons false (Fin.tail x) = x
Tactic:
exact h ▸ Fin.cons_self_tail _
State after:
no goals