case h.h
α : Type ?u.6729
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.6761
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ swap hammingDist x y = hammingDist x y
α : Type ?u.6729
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.6761
inst✝ : (i : ι) → DecidableEq (γ i)
⊢ swap hammingDist = hammingDist
funext x y
no goals
case h.h
α : Type ?u.6729
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.6761
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ swap hammingDist x y = hammingDist x y
exact hammingDist_comm _ _