Dist pos of Nontrivial

lemma dist_pos_of_Nontrivial {ι : Type*} [Fintype ι] {F : Type*} (C : Set (ι → F))    [DecidableEq F] (hC : Set.Nontrivial C) : Code.dist C > 0 := by  rw [Code.dist_eq_minDist]  unfold Code.minDist  let S_eq : Set ℕ := {d | ∃ u ∈ C, ∃ v ∈ C, u ≠ v ∧ hammingDist u v = d}  -- 2. `hC : Set.Nontrivial C` means `∃ u ∈ C, ∃ v ∈ C, u ≠ v`  rcases hC with ⟨u, hu, v, hv, hne⟩  -- 3. This implies S_eq is non-empty, because the distance d' = Δ₀(u, v) is in it  let d' := hammingDist u v  have hd'_in_Seq : d' ∈ S_eq := ⟨u, hu, v, hv, hne, rfl⟩  have hS_eq_nonempty : S_eq.Nonempty := ⟨d', hd'_in_Seq⟩  -- 4. Get the minimum element d_min = sInf S_eq  let d_min := sInf S_eq  -- 5. By `Nat.sInf_mem_of_nonempty`, this minimum d_min is itself an element of S_eq  have h_d_min_in_Seq : d_min ∈ S_eq := by    exact Nat.sInf_mem hS_eq_nonempty  -- 6. Unpack the proof that d_min ∈ S_eq  --    This gives us a pair (u', v') that *achieves* this minimum distance  rcases h_d_min_in_Seq with ⟨u', hu', v', hv', hne', hdist_eq_dmin⟩  -- 7. The goal is to show d_min > 0.  -- We know d_min = hammingDist u' v' from hdist_eq_dmin  dsimp only [d_min, S_eq] at hdist_eq_dmin  rw [←hdist_eq_dmin]  exact hammingDist_pos.mpr hne'