no goals
α : Type ?u.180835
β : Type ?u.180838
γ : Type ?u.180841
ι : Type ?u.180844
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.180875
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
⊢ ↑(↑homeomorphUnitBall 0) = 0
simp