α : Type u_1
inst✝ : Ring α
f g : RingTopology α
a✝ : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g
α : Type u_1
inst✝ : Ring α
⊢ Injective toTopologicalSpace
intro f g _
case mk
α : Type u_1
inst✝ : Ring α
g : RingTopology α
toTopologicalSpace✝ : TopologicalSpace α
toTopologicalRing✝ : TopologicalRing α
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝, toTopologicalRing := toTopologicalRing✝ }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, toTopologicalRing := toTopologicalRing✝ } = g
α : Type u_1
inst✝ : Ring α
f g : RingTopology α
a✝ : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g
cases f
case mk.mk
α : Type u_1
inst✝ : Ring α
toTopologicalSpace✝¹ : TopologicalSpace α
toTopologicalRing✝¹ : TopologicalRing α
toTopologicalSpace✝ : TopologicalSpace α
toTopologicalRing✝ : TopologicalRing α
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝¹, toTopologicalRing := toTopologicalRing✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, toTopologicalRing := toTopologicalRing✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, toTopologicalRing := toTopologicalRing✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, toTopologicalRing := toTopologicalRing✝ }
case mk
α : Type u_1
inst✝ : Ring α
g : RingTopology α
toTopologicalSpace✝ : TopologicalSpace α
toTopologicalRing✝ : TopologicalRing α
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝, toTopologicalRing := toTopologicalRing✝ }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, toTopologicalRing := toTopologicalRing✝ } = g
cases g
no goals
case mk.mk
α : Type u_1
inst✝ : Ring α
toTopologicalSpace✝¹ : TopologicalSpace α
toTopologicalRing✝¹ : TopologicalRing α
toTopologicalSpace✝ : TopologicalSpace α
toTopologicalRing✝ : TopologicalRing α
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝¹, toTopologicalRing := toTopologicalRing✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, toTopologicalRing := toTopologicalRing✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, toTopologicalRing := toTopologicalRing✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, toTopologicalRing := toTopologicalRing✝ }
congr