α : Type u_3
β : Type u_2
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
hom : Type u_1
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (↑f) (𝓝 1) (𝓝 1)
this : ((fun x => x.snd / x.fst) ∘ fun x => (↑f x.fst, ↑f x.snd)) = fun x => ↑f (x.snd / x.fst)
⊢ UniformContinuous ↑f
α : Type u_3
β : Type u_2
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
hom : Type u_1
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (↑f) (𝓝 1) (𝓝 1)
⊢ UniformContinuous ↑f
have :
  ((fun x : β × β => x.2 / x.1) ∘ fun x : α × α => (f x.1, f x.2)) = fun x : α × α =>
    f (x.2 / x.1) := by ext; simp only [Function.comp_apply, map_div]
α : Type u_3
β : Type u_2
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
hom : Type u_1
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (↑f) (𝓝 1) (𝓝 1)
this : ((fun x => x.snd / x.fst) ∘ fun x => (↑f x.fst, ↑f x.snd)) = fun x => ↑f (x.snd / x.fst)
⊢ Tendsto (fun x => ↑f (x.snd / x.fst)) (comap (fun x => x.snd / x.fst) (𝓝 1)) (𝓝 1)
α : Type u_3
β : Type u_2
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
hom : Type u_1
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (↑f) (𝓝 1) (𝓝 1)
this : ((fun x => x.snd / x.fst) ∘ fun x => (↑f x.fst, ↑f x.snd)) = fun x => ↑f (x.snd / x.fst)
⊢ UniformContinuous ↑f
rw [UniformContinuous, uniformity_eq_comap_nhds_one α, uniformity_eq_comap_nhds_one β,
  tendsto_comap_iff, this]
no goals
α : Type u_3
β : Type u_2
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
hom : Type u_1
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (↑f) (𝓝 1) (𝓝 1)
this : ((fun x => x.snd / x.fst) ∘ fun x => (↑f x.fst, ↑f x.snd)) = fun x => ↑f (x.snd / x.fst)
⊢ Tendsto (fun x => ↑f (x.snd / x.fst)) (comap (fun x => x.snd / x.fst) (𝓝 1)) (𝓝 1)
exact Tendsto.comp h tendsto_comap
case h
α : Type u_3
β : Type u_2
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
hom : Type u_1
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (↑f) (𝓝 1) (𝓝 1)
x✝ : α × α
⊢ ((fun x => x.snd / x.fst) ∘ fun x => (↑f x.fst, ↑f x.snd)) x✝ = ↑f (x✝.snd / x✝.fst)
α : Type u_3
β : Type u_2
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
hom : Type u_1
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (↑f) (𝓝 1) (𝓝 1)
⊢ ((fun x => x.snd / x.fst) ∘ fun x => (↑f x.fst, ↑f x.snd)) = fun x => ↑f (x.snd / x.fst)
ext
no goals
case h
α : Type u_3
β : Type u_2
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
hom : Type u_1
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : UniformGroup β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (↑f) (𝓝 1) (𝓝 1)
x✝ : α × α
⊢ ((fun x => x.snd / x.fst) ∘ fun x => (↑f x.fst, ↑f x.snd)) x✝ = ↑f (x✝.snd / x✝.fst)
simp only [Function.comp_apply, map_div]