[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : NonAssocRing α
inst✝ : ContinuousMul α
⊢ Continuous fun a => -a
[PROOFSTEP]
simpa using (continuous_const.mul continuous_id : Continuous fun x : α => -1 * x)
[GOAL]
α : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
refine continuous_of_continuousAt_zero₂ (AddMonoidHom.mul (R := R)) ?_ ?_ ?_
[GOAL]
case refine_1
α : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (fun x => ↑(↑AddMonoidHom.mul x.fst) x.snd) (0, 0)
[PROOFSTEP]
simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]
[GOAL]
case refine_2
α : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (x : R), ContinuousAt (↑(↑AddMonoidHom.mul x)) 0
[PROOFSTEP]
simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]
[GOAL]
case refine_3
α : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (y : R), ContinuousAt (fun x => ↑(↑AddMonoidHom.mul x) y) 0
[PROOFSTEP]
simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]
[GOAL]
α : Type u_1
inst✝ : Ring α
⊢ Injective toTopologicalSpace
[PROOFSTEP]
intro f g _
[GOAL]
α : Type u_1
inst✝ : Ring α
f g : RingTopology α
a✝ : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
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
[PROOFSTEP]
cases g
[GOAL]
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✝ }
[PROOFSTEP]
congr
