case h.e'_5.h.h.e'_2.h.h.e'_3.h.e'_3
𝓕 : Type ?u.129849
𝕜 : Type ?u.129852
α : Type ?u.129855
ι : Type ?u.129858
κ : Type ?u.129861
E : Type u_1
F : Type ?u.129867
G : Type ?u.129870
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ x✝¹ : ℝ
x✝ : E
⊢ x✝ = x✝ / 1
𝓕 : Type ?u.129849
𝕜 : Type ?u.129852
α : Type ?u.129855
ι : Type ?u.129858
κ : Type ?u.129861
E : Type u_1
F : Type ?u.129867
G : Type ?u.129870
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ HasBasis (𝓝 1) (fun ε => 0 < ε) fun ε => {y | ‖y‖ < ε}
convert NormedCommGroup.nhds_basis_norm_lt (1 : E)
no goals
case h.e'_5.h.h.e'_2.h.h.e'_3.h.e'_3
𝓕 : Type ?u.129849
𝕜 : Type ?u.129852
α : Type ?u.129855
ι : Type ?u.129858
κ : Type ?u.129861
E : Type u_1
F : Type ?u.129867
G : Type ?u.129870
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ x✝¹ : ℝ
x✝ : E
⊢ x✝ = x✝ / 1
simp