[GOAL]
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
⊢ IsOpenMap ↑(mk N)
[PROOFSTEP]
intro s s_op
[GOAL]
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
s : Set R
s_op : IsOpen s
⊢ IsOpen (↑(mk N) '' s)
[PROOFSTEP]
change IsOpen (mk N ⁻¹' (mk N '' s))
[GOAL]
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
s : Set R
s_op : IsOpen s
⊢ IsOpen (↑(mk N) ⁻¹' (↑(mk N) '' s))
[PROOFSTEP]
rw [quotient_ring_saturate]
[GOAL]
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
s : Set R
s_op : IsOpen s
⊢ IsOpen (⋃ (x : { x // x ∈ N }), (fun y => ↑x + y) '' s)
[PROOFSTEP]
exact isOpen_iUnion fun ⟨n, _⟩ => isOpenMap_add_left n s s_op
[GOAL]
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
⊢ Function.Surjective fun p => (↑(mk N) p.fst, ↑(mk N) p.snd)
[PROOFSTEP]
rintro ⟨⟨x⟩, ⟨y⟩⟩
[GOAL]
case mk.mk.mk
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
fst✝ snd✝ : R ⧸ N
x y : R
⊢ ∃ a, (fun p => (↑(mk N) p.fst, ↑(mk N) p.snd)) a = (Quot.mk Setoid.r x, Quot.mk Setoid.r y)
[PROOFSTEP]
exact ⟨(x, y), rfl⟩
