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

State before:
α : Type u_1
inst✝ : Encoding α Memory
N₀ N₁ : ℕ
f₀ : (Fin N₀ → Bool) → α
f₁ : (Fin N₁ → Bool) → α
h : encode f₀ = encode f₁
⊢ N₀ = N₁ ∧ HEq f₀ f₁
Tactic:
cases (encodeOp_injN h)
State after:
case refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ f₁ : (Fin N₀ → Bool) → α
h : encode f₀ = encode f₁
⊢ N₀ = N₀ ∧ HEq f₀ f₁

State before:
case refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ f₁ : (Fin N₀ → Bool) → α
h : encode f₀ = encode f₁
⊢ N₀ = N₀ ∧ HEq f₀ f₁
Tactic:
simp [h, ← encodeInjEq]
State after:
no goals

State before:
α : Type u_1
inst✝ : Encoding α Memory
N₀ N₁ : ℕ
f₀ : (Fin N₀ → Bool) → α
f₁ : (Fin N₁ → Bool) → α
h : N₀ = N₁ ∧ HEq f₀ f₁
⊢ encode f₀ = encode f₁
Tactic:
cases h.left
State after:
case refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ f₁ : (Fin N₀ → Bool) → α
h : N₀ = N₀ ∧ HEq f₀ f₁
⊢ encode f₀ = encode f₁

State before:
case refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ f₁ : (Fin N₀ → Bool) → α
h : N₀ = N₀ ∧ HEq f₀ f₁
⊢ encode f₀ = encode f₁
Tactic:
cases h.right
State after:
case refl.refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ : (Fin N₀ → Bool) → α
h : N₀ = N₀ ∧ HEq f₀ f₀
⊢ encode f₀ = encode f₀

State before:
case refl.refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ : (Fin N₀ → Bool) → α
h : N₀ = N₀ ∧ HEq f₀ f₀
⊢ encode f₀ = encode f₀
Tactic:
rfl
State after:
no goals