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

State before:
α : Type u_1
inst✝ : Encoding α Memory
f₀ f₁ : (Fin 0 → Bool) → α
⊢ encodeOp f₀ = encodeOp f₁ → f₀ = f₁
Tactic:
simpa [encodeOp] using λ h ↦ funext λ x ↦ Subsingleton.elim _ x ▸ h
State after:
no goals

State before:
α : Type u_1
inst✝ : Encoding α Memory
N : ℕ
f₀ f₁ : (Fin (N + 1) → Bool) → α
⊢ encodeOp f₀ = encodeOp f₁ → f₀ = f₁
Tactic:
simpa [encodeOp,
  λ b ↦ Iff.intro
    (encodeOp_inj
      (f₀ ∘ (Fin.cons (α := λ _ ↦ Bool) b))
      (f₁ ∘ (Fin.cons (α := λ _ ↦ Bool) b)))
    (λ h ↦ h ▸ rfl)]
  using λ hf ht ↦ funext λ y ↦ Fin.cons_self_tail y ▸
    match y 0 with
    | false => congrFun hf (Fin.tail y)
    | true => congrFun ht (Fin.tail y)
State after:
no goals