-- Mathlib/Topology/Algebra/Order/Field.lean
theorem IsTopologicalRing.of_norm {R 𝕜 : Type*} [NonUnitalNonAssocRing R] [LinearOrderedField 𝕜]
    [TopologicalSpace R] [IsTopologicalAddGroup R] (norm : R → 𝕜)
    (norm_nonneg : ∀ x, 0 ≤ norm x) (norm_mul_le : ∀ x y, norm (x * y) ≤ norm x * norm y)
    (nhds_basis : (𝓝 (0 : R)).HasBasis ((0 : 𝕜) < ·) (fun ε ↦ { x | norm x < ε })) :
    IsTopologicalRing R

Proof state:
case intro.intro
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
δ : 𝕜
δ0 : 0 < δ
hδ : c * δ < ε
x : R
hx : x ∈ {x | norm x < δ}
⊢ c * norm x < ε

Tactic:
exact (mul_le_mul_of_nonneg_left (le_of_lt hx) c0).trans_lt hδ

Result:
no goals

Proof state:
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ IsTopologicalRing R

Tactic:
apply IsTopologicalRing.of_addGroup_of_nhds_zero

Result:
case hmul
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)

case hmul_left
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)

case hmul_right
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)

Proof state:
case hmul_left
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)

case hmul_right
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)

Tactic:
case hmul_left => exact fun x => h0 _ (norm x) (norm_nonneg _) (norm_mul_le x)

Result:
case hmul_right
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)

Proof state:
case intro.intro
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
δ : 𝕜
δ0 : 0 < δ
hδ : c * δ < ε
⊢ ∃ ia, 0 < ia ∧ ∀ x ∈ {x | norm x < ia}, f x ∈ {x | norm x < ε}

Tactic:
refine ⟨δ, δ0, fun x hx ↦ (hf _).trans_lt ?_⟩

Result:
case intro.intro
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
δ : 𝕜
δ0 : 0 < δ
hδ : c * δ < ε
x : R
hx : x ∈ {x | norm x < δ}
⊢ c * norm x < ε

Proof state:
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
⊢ ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)

Tactic:
refine fun f c c0 hf ↦ (nhds_basis.tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_

Result:
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
⊢ ∃ ia, 0 < ia ∧ ∀ x ∈ {x | norm x < ia}, f x ∈ {x | norm x < ε}

Proof state:
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)

Tactic:
refine ((nhds_basis.prod nhds_basis).tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_

Result:
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
⊢ ∃ ia,
    (0 < ia.1 ∧ 0 < ia.2) ∧
      ∀ x ∈ {x | norm x < ia.1} ×ˢ {x | norm x < ia.2}, uncurry (fun x1 x2 => x1 * x2) x ∈ {x | norm x < ε}