α : Type ?u.489
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.521
inst✝ : (i : ι) → DecidableEq (γ i)
x : (i : ι) → β i
⊢ ∀ (x_1 : ι), x_1 ∈ univ → ¬x x_1 ≠ x x_1
α : Type ?u.489
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.521
inst✝ : (i : ι) → DecidableEq (γ i)
x : (i : ι) → β i
⊢ hammingDist x x = 0
rw [hammingDist, card_eq_zero, filter_eq_empty_iff]
no goals
α : Type ?u.489
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.521
inst✝ : (i : ι) → DecidableEq (γ i)
x : (i : ι) → β i
⊢ ∀ (x_1 : ι), x_1 ∈ univ → ¬x x_1 ≠ x x_1
exact fun _ _ H => H rfl