no goals
α : Type ?u.26239
ι : Type u_3
β : ι → Type u_1
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_2
inst✝² : (i : ι) → DecidableEq (γ i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → Zero (γ i)
f : (i : ι) → γ i → β i
x : (i : ι) → γ i
hf : ∀ (i : ι), f i 0 = 0
⊢ (hammingNorm fun i => f i (x i)) ≤ hammingNorm x
simpa only [← hammingDist_zero_right, hf] using hammingDist_comp_le_hammingDist f (y := fun _ ↦ 0)