English
When two sets s and t are equal via a proof H' and their elementwise identifications match via H, casting an element from s to t corresponds to keeping its underlying value and adjusting the membership proof accordingly.
Русский
При равенстве множеств s и t и совместимости элементов, приведение элемента из s к t сохраняет его значение и корректно трансформирует доказательство принадлежности.
LaTeX
$$$\forall {s t : Set \alpha} (H' : s = t) (H : \uparrow s = \uparrow t) (x : s),\; cast H x = \langle x.1, H' \;\ x.2\rangle$$$
Lean4
@[simp]
theorem set_coe_cast : ∀ {s t : Set α} (H' : s = t) (H : ↥s = ↥t) (x : s), cast H x = ⟨x.1, H' ▸ x.2⟩
| _, _, rfl, _, _ => rfl
