English
Let E be a type with an equivalence-like structure between R and S and e ∈ E. For any ideal I ⊆ R and y ∈ S, membership of y in I.map e is equivalent to the existence of x ∈ I with e(x) = y.
Русский
Пусть e задаёт эквивалентность между R и S в общем виде. Тогда для любого идеала I ⊆ R и любого y ∈ S: y ∈ I.map e ⇔ существует x ∈ I с e(x) = y.
LaTeX
$$$y \\in \\operatorname{map} e I \\;\\iff\\; \\exists x \\in I,\\ e x = y$$$
Lean4
theorem mem_map_of_equiv {E : Type*} [EquivLike E R S] [RingEquivClass E R S] (e : E) {I : Ideal R} (y : S) :
y ∈ map e I ↔ ∃ x ∈ I, e x = y := by
constructor
· intro h
simp_rw [show map e I = _ from map_comap_of_equiv (e : R ≃+* S)] at h
exact ⟨(e : R ≃+* S).symm y, h, (e : R ≃+* S).apply_symm_apply y⟩
· rintro ⟨x, hx, rfl⟩
exact mem_map_of_mem e hx
