no goals
𝓕 : Type ?u.1275542
𝕜 : Type ?u.1275545
α : Type ?u.1275548
ι : Type u_1
κ : Type ?u.1275554
E : Type u_2
F : Type ?u.1275560
G : Type ?u.1275563
π : ι → Type ?u.1275568
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedGroup (π i)
inst✝¹ : SeminormedGroup E
f x : (i : ι) → π i
r : ℝ
inst✝ : Nonempty ι
a : E
⊢ ‖fun _i => a‖ = ‖a‖
simpa only [← dist_one_right] using dist_pi_const a 1