case refine'_1
α : Type u_3
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_1
inst✝⁴ : UniformSpace β
inst✝³ : DiscreteTopology β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
hf : UniformContinuous ↑f
⊢ IsOpen ↑(MonoidHom.ker ↑f)

case refine'_2
α : Type u_3
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_1
inst✝⁴ : UniformSpace β
inst✝³ : DiscreteTopology β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen ↑(MonoidHom.ker ↑f)
⊢ UniformContinuous ↑f
α : Type u_3
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_1
inst✝⁴ : UniformSpace β
inst✝³ : DiscreteTopology β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
⊢ UniformContinuous ↑f ↔ IsOpen ↑(MonoidHom.ker ↑f)
refine' ⟨fun hf => _, fun hf => _⟩
no goals
case refine'_1
α : Type u_3
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_1
inst✝⁴ : UniformSpace β
inst✝³ : DiscreteTopology β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
hf : UniformContinuous ↑f
⊢ IsOpen ↑(MonoidHom.ker ↑f)
apply (isOpen_discrete ({1} : Set β)).preimage hf.continuous
case refine'_2.hf
α : Type u_3
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_1
inst✝⁴ : UniformSpace β
inst✝³ : DiscreteTopology β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen ↑(MonoidHom.ker ↑f)
⊢ ContinuousAt (↑f) 1
case refine'_2
α : Type u_3
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_1
inst✝⁴ : UniformSpace β
inst✝³ : DiscreteTopology β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen ↑(MonoidHom.ker ↑f)
⊢ UniformContinuous ↑f
apply uniformContinuous_of_continuousAt_one
case refine'_2.hf
α : Type u_3
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_1
inst✝⁴ : UniformSpace β
inst✝³ : DiscreteTopology β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen ↑(MonoidHom.ker ↑f)
⊢ ∀ᶠ (x : α) in 𝓝 1, ↑f x = 1
case refine'_2.hf
α : Type u_3
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_1
inst✝⁴ : UniformSpace β
inst✝³ : DiscreteTopology β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen ↑(MonoidHom.ker ↑f)
⊢ ContinuousAt (↑f) 1
rw [ContinuousAt, nhds_discrete β, map_one, tendsto_pure]
no goals
case refine'_2.hf
α : Type u_3
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_1
inst✝⁴ : UniformSpace β
inst✝³ : DiscreteTopology β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen ↑(MonoidHom.ker ↑f)
⊢ ∀ᶠ (x : α) in 𝓝 1, ↑f x = 1
exact hf.mem_nhds (map_one f)