𝕜 : Type u_1
𝕜₂ : Type ?u.433245
𝕝 : Type ?u.433248
𝕝₂ : Type ?u.433251
E : Type u_2
F : Type ?u.433257
G : Type ?u.433260
ι : Type u_3
ι' : Type ?u.433266
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
⊢ 𝓝 0 = 𝓝 0
𝕜 : Type u_1
𝕜₂ : Type ?u.433245
𝕝 : Type ?u.433248
𝕝₂ : Type ?u.433251
E : Type u_2
F : Type ?u.433257
G : Type ?u.433260
ι : Type u_3
ι' : Type ?u.433266
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
⊢ WithSeminorms p
refine'
  ⟨TopologicalAddGroup.ext inferInstance p.addGroupFilterBasis.isTopologicalAddGroup _⟩
𝕜 : Type u_1
𝕜₂ : Type ?u.433245
𝕝 : Type ?u.433248
𝕝₂ : Type ?u.433251
E : Type u_2
F : Type ?u.433257
G : Type ?u.433260
ι : Type u_3
ι' : Type ?u.433266
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
⊢ 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
𝕜 : Type u_1
𝕜₂ : Type ?u.433245
𝕝 : Type ?u.433248
𝕝₂ : Type ?u.433251
E : Type u_2
F : Type ?u.433257
G : Type ?u.433260
ι : Type u_3
ι' : Type ?u.433266
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
⊢ 𝓝 0 = 𝓝 0
rw [AddGroupFilterBasis.nhds_zero_eq]
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.433245
𝕝 : Type ?u.433248
𝕝₂ : Type ?u.433251
E : Type u_2
F : Type ?u.433257
G : Type ?u.433260
ι : Type u_3
ι' : Type ?u.433266
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
⊢ 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
exact h