English
If two multisets s and t are equal, then there is a natural equivalence between their underlying types of elements: s.ToType ≃ t.ToType.
Русский
Если два мультимножества s и t равны, то существует естественное эквивалентное соответствие между их соответствующими множествами элементов: s.ToType ≃ t.ToType.
LaTeX
$$$ s^{\mathrm{ToType}} \simeq t^{\mathrm{ToType}} \quad \text{whenever } s = t $$$
Lean4
/-- If `s = t` then there's an equivalence between the appropriate types.
-/
@[simps]
def cast {s t : Multiset α} (h : s = t) : s ≃ t
where
toFun x := ⟨x.1, x.2.cast (by simp [h])⟩
invFun x := ⟨x.1, x.2.cast (by simp [h])⟩
