no goals
α : Type u_2
β : Type ?u.15386
γ : Type ?u.15389
ι : Type ?u.15392
inst✝⁵ : NormedField α
inst✝⁴ : SeminormedAddCommGroup β
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace α E
F : Type ?u.15423
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace α F
c : α
x : E
ε : ℝ
h : 0 < ε
⊢ ‖c • (id x - x)‖ = 0
simp