Lean: σ-algebra generated by e(x) on UnitAddCircle is Borel (measurable embedding)

To show comap of a continuous injective map from a compact space is the whole Borel σ-algebra, use (hf_cont.isClosedEmbedding hinj).measurableEmbedding (Continuous.isClosedEmbedding needs CompactSpace domain and T2 codomain), then for measurable S write snd⁻¹' S as (e ∘ snd)⁻¹' (e '' S) with MeasurableEmbedding.measurableSet_image and Function.Injective.mem_set_image. For fourier 1 on UnitAddCircle, injectivity: rewrite with fourier_one, then AddCircle.injective_toCircle one_ne_zero and Circle.coe_injective. To prove a sub-σ-algebra m of a product equals the product, le_antisymm h (sup_le ?_ ?_) works directly because the product instance unfolds to comap fst ⊔ comap snd; the goals are rintro _ ⟨s, hs, rfl⟩.