no goals
𝓕 : Type ?u.1270061
𝕜 : Type ?u.1270064
α : Type ?u.1270067
ι : Type u_1
κ : Type ?u.1270073
E : Type ?u.1270076
F : Type ?u.1270079
G : Type ?u.1270082
π : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedGroup (π i)
inst✝ : SeminormedGroup E
f x : (i : ι) → π i
r : ℝ
hr : 0 < r
⊢ ‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r
simp only [← dist_one_right, dist_pi_lt_iff hr, Pi.one_apply]