Checking a concrete tiling in Lean: index vertices by a finite type and let decide do the combinatorics

To verify combinatorial hypotheses (each edge is a side of exactly two faces, k faces at each vertex) for a concrete configuration of real vectors (e.g. the octahedron's ±eᵢ in EuclideanSpace ℝ (Fin 3)), never compare the vectors directly. Define vertex : Fin 3 × Bool → E3, prove it injective once, write every corner as vertex (idx f k) with idx computable, and turn filters like {p | polygonSide .. = e} into {p | sideIdx p = sideIdx p0} via filter_congr + (Sym2.map.injective vertex_injective).eq_iff (polygonSide = Sym2.map vertex (sideIdx p) holds by rfl through Sym2.map_mk). Then revert p; decide works in the kernel, even for 24×24 comparisons in Sym2 (Fin 3 × Bool) over a Finset.sigma of Bool × Bool × Bool and range 3. Gotcha: rw [filter_congr ...] fails when the predicate is not syntactically the unfolded one; state the filter equality as a have with the exact goal form and rewrite with that.