no goals
α : Type ?u.32980
ι : Type u_2
β : ι → Type u_1
inst✝³ : Fintype ι
inst✝² : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.33012
inst✝¹ : (i : ι) → DecidableEq (γ i)
inst✝ : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingNorm (x - y)
simp_rw [hammingNorm, hammingDist, Pi.sub_apply, sub_ne_zero]