English
If s = ↑S, then S.copy s hs = S.
Русский
Если s = ↑S, то S.copy s hs = S.
LaTeX
$$$S.copy\, s\, hs = S\quad\text{ when } hs : s = \uparrow S$$$
Lean4
/-- Copy of a star subalgebra with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (S : StarSubalgebra R A) (s : Set A) (hs : s = ↑S) : StarSubalgebra R A
where
toSubalgebra := Subalgebra.copy S.toSubalgebra s hs
star_mem' {a} ha := hs ▸ S.star_mem' (by simpa [hs] using ha)