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)
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)
rintro ⟨⟨x⟩, ⟨y⟩⟩
no goals
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)
exact ⟨(x, y), rfl⟩