Lean4
instance semiNormedCommRing : SeminormedCommRing (R ⧸ I)
where
dist_eq := dist_eq_norm
mul_comm := _root_.mul_comm
norm_mul_le x
y :=
le_of_forall_pos_le_add fun ε hε =>
by
have :=
((nhds_basis_ball.prod_nhds nhds_basis_ball).tendsto_iff nhds_basis_ball).mp (continuous_mul.tendsto (‖x‖, ‖y‖))
ε hε
simp only [Set.mem_prod, mem_ball, and_imp, Prod.forall, Prod.exists] at this
rcases this with ⟨ε₁, ε₂, ⟨h₁, h₂⟩, h⟩
obtain ⟨⟨a, rfl, ha⟩, ⟨b, rfl, hb⟩⟩ := Ideal.Quotient.norm_mk_lt x h₁, Ideal.Quotient.norm_mk_lt y h₂
simp only [dist, abs_sub_lt_iff] at h
specialize
h ‖a‖ ‖b‖ ⟨by linarith, by linarith [Ideal.Quotient.norm_mk_le I a]⟩
⟨by linarith, by linarith [Ideal.Quotient.norm_mk_le I b]⟩
calc
_ ≤ ‖a‖ * ‖b‖ := (Ideal.Quotient.norm_mk_le I (a * b)).trans (norm_mul_le a b)
_ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le
