[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x : (i : ι) → β i
⊢ hammingDist x x = 0
[PROOFSTEP]
rw [hammingDist, card_eq_zero, filter_eq_empty_iff]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x : (i : ι) → β i
⊢ ∀ (x_1 : ι), x_1 ∈ univ → ¬x x_1 ≠ x x_1
[PROOFSTEP]
exact fun _ _ H => H rfl
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingDist y x
[PROOFSTEP]
simp_rw [hammingDist, ne_comm]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x z ≤ hammingDist x y + hammingDist y z
[PROOFSTEP]
classical
unfold hammingDist
refine le_trans (card_mono ?_) (card_union_le _ _)
rw [← filter_or]
exact monotone_filter_right _ fun i h ↦ (h.ne_or_ne _).imp_right Ne.symm
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x z ≤ hammingDist x y + hammingDist y z
[PROOFSTEP]
unfold hammingDist
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ card (filter (fun i => x i ≠ z i) univ) ≤
    card (filter (fun i => x i ≠ y i) univ) + card (filter (fun i => y i ≠ z i) univ)
[PROOFSTEP]
refine le_trans (card_mono ?_) (card_union_le _ _)
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ filter (fun i => x i ≠ z i) univ ≤ filter (fun i => x i ≠ y i) univ ∪ filter (fun i => y i ≠ z i) univ
[PROOFSTEP]
rw [← filter_or]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ filter (fun i => x i ≠ z i) univ ≤ filter (fun a => x a ≠ y a ∨ y a ≠ z a) univ
[PROOFSTEP]
exact monotone_filter_right _ fun i h ↦ (h.ne_or_ne _).imp_right Ne.symm
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist z x + hammingDist z y
[PROOFSTEP]
rw [hammingDist_comm z]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist z y
[PROOFSTEP]
exact hammingDist_triangle _ _ _
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist y z
[PROOFSTEP]
rw [hammingDist_comm y]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist z y
[PROOFSTEP]
exact hammingDist_triangle _ _ _
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
⊢ swap hammingDist = hammingDist
[PROOFSTEP]
funext x y
[GOAL]
case h.h
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ swap hammingDist x y = hammingDist x y
[PROOFSTEP]
exact hammingDist_comm _ _
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ hammingDist x y = 0 → x = y
[PROOFSTEP]
simp_rw [hammingDist, card_eq_zero, filter_eq_empty_iff, Classical.not_not, funext_iff, mem_univ, forall_true_left,
  imp_self]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
H : x = y
⊢ hammingDist x y = 0
[PROOFSTEP]
rw [H]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
H : x = y
⊢ hammingDist y y = 0
[PROOFSTEP]
exact hammingDist_self _
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ 0 = hammingDist x y ↔ x = y
[PROOFSTEP]
rw [eq_comm, hammingDist_eq_zero]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ 0 < hammingDist x y ↔ x ≠ y
[PROOFSTEP]
rw [← hammingDist_ne_zero, iff_not_comm, not_lt, le_zero_iff]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
x y : (i : ι) → β i
⊢ hammingDist x y < 1 ↔ x = y
[PROOFSTEP]
rw [Nat.lt_one_iff, hammingDist_eq_zero]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝² : (i : ι) → DecidableEq (γ i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → Zero (γ i)
x : (i : ι) → β i
⊢ hammingDist 0 x = hammingNorm x
[PROOFSTEP]
rw [hammingDist_comm, hammingDist_zero_right]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
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
[PROOFSTEP]
simpa only [← hammingDist_zero_right, hf] using hammingDist_comp_le_hammingDist f (y := fun _ ↦ 0)
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝² : (i : ι) → DecidableEq (γ i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → Zero (γ i)
f : (i : ι) → γ i → β i
x : (i : ι) → γ i
hf₁ : ∀ (i : ι), Injective (f i)
hf₂ : ∀ (i : ι), f i 0 = 0
⊢ (hammingNorm fun i => f i (x i)) = hammingNorm x
[PROOFSTEP]
simpa only [← hammingDist_zero_right, hf₂] using hammingDist_comp f hf₁ (y := fun _ ↦ 0)
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁶ : Fintype ι
inst✝⁵ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝⁴ : (i : ι) → DecidableEq (γ i)
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → Zero (γ i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
x : (i : ι) → β i
i : ι
⊢ (fun i c => k • c) i 0 = 0
[PROOFSTEP]
simp_rw [smul_zero]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁶ : Fintype ι
inst✝⁵ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝⁴ : (i : ι) → DecidableEq (γ i)
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → Zero (γ i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
hk : ∀ (i : ι), IsSMulRegular (β i) k
x : (i : ι) → β i
i : ι
⊢ (fun i c => k • c) i 0 = 0
[PROOFSTEP]
simp_rw [smul_zero]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝¹ : (i : ι) → DecidableEq (γ i)
inst✝ : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingNorm (x - y)
[PROOFSTEP]
simp_rw [hammingNorm, hammingDist, Pi.sub_apply, sub_ne_zero]
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x : Hamming β), dist x x = 0
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x : Hamming β), ↑(hammingDist (↑ofHamming x) (↑ofHamming x)) = 0
[PROOFSTEP]
exact_mod_cast hammingDist_self
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y : Hamming β), dist x y = dist y x
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y : Hamming β), ↑(hammingDist (↑ofHamming x) (↑ofHamming y)) = ↑(hammingDist (↑ofHamming y) (↑ofHamming x))
[PROOFSTEP]
exact_mod_cast hammingDist_comm
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y z : Hamming β), dist x z ≤ dist x y + dist y z
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y z : Hamming β),
    ↑(hammingDist (↑ofHamming x) (↑ofHamming z)) ≤
      ↑(hammingDist (↑ofHamming x) (↑ofHamming y)) + ↑(hammingDist (↑ofHamming y) (↑ofHamming z))
[PROOFSTEP]
exact_mod_cast hammingDist_triangle
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝¹ x✝ : Hamming β
⊢ (fun x y => ↑{ val := dist x y, property := (_ : 0 ≤ dist x y) }) x✝¹ x✝ = ENNReal.ofReal (dist x✝¹ x✝)
[PROOFSTEP]
exact ENNReal.coe_nnreal_eq _
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) ↔ ∃ ε, ε > 0 ∧ ∀ {a b : Hamming β}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) ↔
    ∃ ε, ε > 0 ∧ ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < ε → (a, b) ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) →
    ∃ ε, ε > 0 ∧ ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < ε → (a, b) ∈ s
[PROOFSTEP]
refine' fun hs => ⟨1, zero_lt_one, fun hab => _⟩
[GOAL]
case mp
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
hs : s ∈ uniformity (Hamming β)
a✝ b✝ : Hamming β
hab : ↑(hammingDist (↑ofHamming a✝) (↑ofHamming b✝)) < 1
⊢ (a✝, b✝) ∈ s
[PROOFSTEP]
rw_mod_cast [hammingDist_lt_one] at hab 
[GOAL]
case mp
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
hs : s ∈ uniformity (Hamming β)
a✝ b✝ : Hamming β
hab : ↑ofHamming a✝ = ↑ofHamming b✝
⊢ (a✝, b✝) ∈ s
[PROOFSTEP]
rw [ofHamming_inj, ← mem_idRel] at hab 
[GOAL]
case mp
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
hs : s ∈ uniformity (Hamming β)
a✝ b✝ : Hamming β
hab : (a✝, b✝) ∈ idRel
⊢ (a✝, b✝) ∈ s
[PROOFSTEP]
exact hs hab
[GOAL]
case mpr
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ (∃ ε, ε > 0 ∧ ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < ε → (a, b) ∈ s) →
    s ∈ uniformity (Hamming β)
[PROOFSTEP]
rintro ⟨_, hε, hs⟩ ⟨_, _⟩ hab
[GOAL]
case mpr.intro.intro.mk
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
w✝ : ℝ
hε : w✝ > 0
hs : ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < w✝ → (a, b) ∈ s
fst✝ snd✝ : Hamming β
hab : (fst✝, snd✝) ∈ idRel
⊢ (fst✝, snd✝) ∈ s
[PROOFSTEP]
rw [mem_idRel] at hab 
[GOAL]
case mpr.intro.intro.mk
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
w✝ : ℝ
hε : w✝ > 0
hs : ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < w✝ → (a, b) ∈ s
fst✝ snd✝ : Hamming β
hab : fst✝ = snd✝
⊢ (fst✝, snd✝) ∈ s
[PROOFSTEP]
rw [hab]
[GOAL]
case mpr.intro.intro.mk
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
w✝ : ℝ
hε : w✝ > 0
hs : ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < w✝ → (a, b) ∈ s
fst✝ snd✝ : Hamming β
hab : fst✝ = snd✝
⊢ (snd✝, snd✝) ∈ s
[PROOFSTEP]
refine' hs (lt_of_eq_of_lt _ hε)
[GOAL]
case mpr.intro.intro.mk
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
w✝ : ℝ
hε : w✝ > 0
hs : ∀ {a b : Hamming β}, ↑(hammingDist (↑ofHamming a) (↑ofHamming b)) < w✝ → (a, b) ∈ s
fst✝ snd✝ : Hamming β
hab : fst✝ = snd✝
⊢ ↑(hammingDist (↑ofHamming snd✝) (↑ofHamming snd✝)) = 0
[PROOFSTEP]
exact_mod_cast hammingDist_self _
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ (Bornology.cobounded (Hamming β)).sets =
    {s | ∃ C, ∀ (x : Hamming β), x ∈ sᶜ → ∀ (y : Hamming β), y ∈ sᶜ → dist x y ≤ C}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝ : Set (Hamming β)
⊢ x✝ ∈ (Bornology.cobounded (Hamming β)).sets ↔
    x✝ ∈ {s | ∃ C, ∀ (x : Hamming β), x ∈ sᶜ → ∀ (y : Hamming β), y ∈ sᶜ → dist x y ≤ C}
[PROOFSTEP]
push_cast
[GOAL]
case h
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝ : Set (Hamming β)
⊢ x✝ ∈ (Bornology.cobounded (Hamming β)).sets ↔
    x✝ ∈
      {s |
        ∃ C, ∀ (x : Hamming β), x ∈ sᶜ → ∀ (y : Hamming β), y ∈ sᶜ → ↑(hammingDist (↑ofHamming x) (↑ofHamming y)) ≤ C}
[PROOFSTEP]
refine' iff_of_true (Filter.mem_sets.mpr Filter.mem_bot) ⟨Fintype.card ι, fun _ _ _ _ => _⟩
[GOAL]
case h
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝⁴ : Set (Hamming β)
x✝³ : Hamming β
x✝² : x✝³ ∈ x✝⁴ᶜ
x✝¹ : Hamming β
x✝ : x✝¹ ∈ x✝⁴ᶜ
⊢ ↑(hammingDist (↑ofHamming x✝³) (↑ofHamming x✝¹)) ≤ ↑(Fintype.card ι)
[PROOFSTEP]
exact_mod_cast hammingDist_le_card_fintype
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddCommGroup (β i)
⊢ ∀ (x y : Hamming β), dist x y = ‖x - y‖
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddCommGroup (β i)
⊢ ∀ (x y : Hamming β), ↑(hammingDist (↑ofHamming x) (↑ofHamming y)) = ↑(hammingNorm (↑ofHamming (x - y)))
[PROOFSTEP]
exact_mod_cast hammingDist_eq_hammingNorm
