no goals
α : Type ?u.3412
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.3444
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x z ≤ hammingDist x y + hammingDist y z
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
α : Type ?u.3412
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.3444
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)
α : Type ?u.3412
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.3444
inst✝ : (i : ι) → DecidableEq (γ i)
x y z : (i : ι) → β i
⊢ hammingDist x z ≤ hammingDist x y + hammingDist y z
unfold hammingDist
α : Type ?u.3412
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.3444
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
α : Type ?u.3412
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.3444
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)
refine le_trans (card_mono ?_) (card_union_le _ _)
α : Type ?u.3412
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.3444
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
α : Type ?u.3412
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.3444
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
rw [← filter_or]
no goals
α : Type ?u.3412
ι : Type u_1
β : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type ?u.3444
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
exact monotone_filter_right _ fun i h ↦ (h.ne_or_ne _).imp_right Ne.symm