Hamming Dist le of outer comp injective

theorem hammingDist_le_of_outer_comp_injective {ι₁ ι₂ : Type*} [Fintype ι₁] [Fintype ι₂]    {β : ι₂ → Type*} [∀ i, DecidableEq (β i)] [DecidableEq ι₂]    (x y : ∀ i, β i) (g : ι₁ → ι₂) (hg : Function.Injective g) :    hammingDist (fun i => x (g i)) (fun i => y (g i)) ≤ hammingDist x y := by  -- Let D₂ be the set of disagreeing indices for x and y.  let D₂ := Finset.filter (fun i₂ => x i₂ ≠ y i₂) Finset.univ  -- The Hamming distance of the composed functions is the card of the preimage of D₂.  suffices (Finset.filter (fun i₁ => x (g i₁) ≠ y (g i₁)) Finset.univ).card ≤ D₂.card by    unfold hammingDist; simp only [this, D₂]  -- The cardinality of a preimage is at most the cardinalit    -- of the original set for an injective function.  -- ⊢ #{i₁ | x (g i₁) ≠ y (g i₁)} ≤ #D₂   -- First, we state that the set on the left is the `preimage` of D₂ under g.  have h_preimage : Finset.filter (fun i₁ => x (g i₁) ≠ y (g i₁)) Finset.univ    = D₂.preimage g (by exact hg.injOn) := by    -- Use `ext` to prove equality by showing the membership conditions are the same.    ext i₁    -- Now `simp` can easily unfold `mem_filter` and `mem_preimage` and see they are equivalent.    simp only [ne_eq, mem_filter, mem_univ, true_and, mem_preimage, D₂]   -- Now, rewrite the goal using `preimage`.  rw [h_preimage]  set D₁ := D₂.preimage g (by exact hg.injOn)  -- ⊢ #D₁ ≤ #D₂  -- Step 1 : The size of a set is at most the size of its image under an injective function.  have h_card_le_image : D₁.card ≤ (D₁.image g).card := by    -- This follows directly from the fact that `g` is injective on the set D₁.    apply Finset.card_le_card_of_injOn (f := g)    · -- Goal 1 : Prove that `g` maps `D₁` to `D₁.image g`. This is true by definition of image.      have res := Set.mapsTo_image (f := g) (s := D₁)      convert res      simp only [coe_image]      -- (D₁.image g : Set ι₂)    · -- Goal 2 : Prove that `g` is injective on the set `D₁`.      -- This is true because our main hypothesis `hg` states that `g` is injective everywhere.      exact Function.Injective.injOn hg   -- Step 2 : The image of the preimage of a set is always a subset of the original set.  have h_image_subset : D₁.image g ⊆ D₂ := by    simp [D₁, Finset.image_preimage]   -- Step 3 : By combining these two facts, we get our result.  -- |D₁| ≤ |image g(D₁)| (from Step 1)  -- and |image g(D₁)| ≤ |D₂| (since it's a subset)  exact h_card_le_image.trans (Finset.card_le_card h_image_subset)