Dist eq min Wt Codewords

lemma dist_eq_minWtCodewords [Ring F] {A : Type*} [DecidableEq A] [AddCommGroup A] [Module F A]    {MC : ModuleCode ι F A} :  Code.minDist (MC : Set (ι → A)) = minWtCodewords MC := by    unfold Code.minDist minWtCodewords    refine congrArg _ (Set.ext fun _ ↦ ⟨fun ⟨u, _, v, _⟩ ↦ ⟨u - v, ?p₁⟩, fun _ ↦ ⟨0, ?p₂⟩⟩) <;>    rename_i u hu v u_sub_v_weight hvv h_u_mem hv_u_v_rel    -- aesop (add simp [hammingDist_eq_wt_sub, sub_eq_zero])    constructor    · rcases hv_u_v_rel with ⟨h_v_mem, h_u_ne_v, h_dist⟩      apply Submodule.sub_mem      · exact h_u_mem      · exact h_v_mem    · -- case p₂      rcases hv_u_v_rel with ⟨h_v_mem, h_u_ne_v, h_dist⟩      constructor      · rw [sub_ne_zero]; exact h_u_ne_v      · -- ⊢ Code.wt (u - v) = hv        -- We know `Code.wt c = h_u_mem`, so we show `Δ₀(0, c) = Code.wt c`        rw [← h_dist]        simp [Code.wt, hammingDist, sub_eq_zero]    · simp only [SetLike.mem_coe, ne_eq, hammingDist_zero_left]      rcases hv_u_v_rel with ⟨c, h_c_mem, h_c_ne, h_c_wt⟩      -- We need to prove the conjunction      constructor      · -- 1. Prove `0 ∈ MC`        let res := Submodule.zero_mem (p := MC)        exact res      · -- 2. Prove `∃ v_1 ...`        refine ⟨c, h_c_mem, ?_, ?_⟩        · -- Prove `¬0 = c` (which is `0 ≠ c`)          exact h_c_ne.symm        · -- Prove `‖c‖₀ = h_u_mem`          rw [←h_c_wt]          simp only [hammingNorm, ne_eq, Code.wt]