no goals
α : Type ?u.19245
ι : Type u_1
β : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.19277
inst✝² : (i : ι) → DecidableEq (γ i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → Zero (γ i)
x : (i : ι) → β i
⊢ hammingDist 0 x = hammingNorm x
rw [hammingDist_comm, hammingDist_zero_right]