To Shape of Special Sound eq distinct Shape

theorem toShape_ofSpecialSound_eq_distinctShape (k : pSpec.ChallengeIdx → ℕ) (hk : ∀ i, 2 ≤ k i) :    (CWSSStructure.ofSpecialSound k hk).toShape = distinctShape k := by  have harity : (CWSSStructure.ofSpecialSound k hk).toShape.arity = (distinctShape k).arity := by    funext i    change 1 * (k i - 1) + 1 = k i    have := hk i; omega  refine ChallengeTreeShape.ext harity (Function.hfunext rfl (fun i i' hi => ?_))  obtain rfl := eq_of_heq hi  refine Function.hfunext (by rw [harity]) (fun c c' hc => ?_)  refine HEq.trans (heq_of_eq (propext ?_)) (heq_injective (congrArg Fin (congrFun harity i)) hc)  change CoordinateWise.IsSpecialSoundFamily 1 (k i)      (fun j : Fin (1 * (k i - 1) + 1) =>        (Equiv.funUnique (Fin 1) (pSpec.Challenge i)).symm (c j)) ↔ Function.Injective c  rw [CoordinateWise.isSpecialSoundFamily_one_iff_injective]  exact Equiv.comp_injective c (Equiv.funUnique (Fin 1) (pSpec.Challenge i)).symm