no goals
𝓕 : Type ?u.51314
𝕜 : Type ?u.51317
α : Type ?u.51320
ι : Type ?u.51323
κ : Type ?u.51326
E : Type u_1
F : Type u_2
G : Type ?u.51335
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : E → F
hi : Isometry f
h₁ : f 1 = 1
x : E
⊢ ‖f x‖ = ‖x‖
rw [← dist_one_right, ← h₁, hi.dist_eq, dist_one_right]