no goals
α : Type ?u.12284
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.12316
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ 0 < hammingDist x y ↔ x ≠ y
rw [← hammingDist_ne_zero, iff_not_comm, not_lt, le_zero_iff]