case a
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type ?u.2210
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
f : G →* H
emb : OpenEmbedding ↑f
U : Set H
hU : U ∈ nhds 1
⊢ U ∈ nhds (↑f 1)
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type ?u.2210
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
f : G →* H
emb : OpenEmbedding ↑f
U : Set H
hU : U ∈ nhds 1
⊢ ↑f ⁻¹' U ∈ nhds 1
apply emb.continuous.tendsto
no goals
case a
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type ?u.2210
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
f : G →* H
emb : OpenEmbedding ↑f
U : Set H
hU : U ∈ nhds 1
⊢ U ∈ nhds (↑f 1)
rwa [f.map_one]