English
The copy operation preserves membership under equality of carriers; i.e., the proof that S.copy s hs has a carrier equal to s is provided by reflexivity.
Русский
Операция копирования сохраняет членство при равенстве носителей; доказательство следует из рефлексивности.
LaTeX
$$copy_eq {S : NonUnitalStarSubsemiring R} {s : Set R} {hs : s = ↑S} : S.copy s hs = S$$
Lean4
/-- Copy of a non-unital star subsemiring with a new `carrier` equal to the old one.
Useful to fix definitional equalities. -/
protected def copy (S : NonUnitalStarSubsemiring R) (s : Set R) (hs : s = ↑S) : NonUnitalStarSubsemiring R :=
{ S.toNonUnitalSubsemiring.copy s hs with
star_mem' := fun {x} (hx : x ∈ s) => by
change star x ∈ s
rw [hs] at hx ⊢
exact S.star_mem' hx }
