lemma proved term proof

`toNat3_pattern3`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 122lemma toNat3_pattern3 (w : Fin 8) : toNat3 (pattern3 w) = w.val := by

Term-mode proof.

 123  -- Only 8 cases; compute directly.
 124  fin_cases w <;> decide
 125

From the project-wide theorem graph. These declarations reference this one in their body.

Lean names referenced from this declaration's body.