-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem uniformContinuous_of_tendsto_one {hom : Type*} [UniformSpace β] [Group β] [UniformGroup β]
    [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} (h : Tendsto f (𝓝 1) (𝓝 1)) :
    UniformContinuous f

Proof state:
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : UniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (⇑f) (𝓝 1) (𝓝 1)
this : ((fun x => x.2 / x.1) ∘ fun x => (f x.1, f x.2)) = fun x => f (x.2 / x.1)
⊢ Tendsto (fun x => f (x.2 / x.1)) (comap (fun x => x.2 / x.1) (𝓝 1)) (𝓝 1)

Tactic:
exact Tendsto.comp h tendsto_comap

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : UniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (⇑f) (𝓝 1) (𝓝 1)
x✝ : α × α
⊢ ((fun x => x.2 / x.1) ∘ fun x => (f x.1, f x.2)) x✝ = f (x✝.2 / x✝.1)

Tactic:
simp only [Function.comp_apply, map_div]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : UniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (⇑f) (𝓝 1) (𝓝 1)
⊢ UniformContinuous ⇑f

Tactic:
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]

Result:
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : UniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (⇑f) (𝓝 1) (𝓝 1)
this : ((fun x => x.2 / x.1) ∘ fun x => (f x.1, f x.2)) = fun x => f (x.2 / x.1)
⊢ UniformContinuous ⇑f

Proof state:
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : UniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (⇑f) (𝓝 1) (𝓝 1)
⊢ ((fun x => x.2 / x.1) ∘ fun x => (f x.1, f x.2)) = fun x => f (x.2 / x.1)

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : UniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (⇑f) (𝓝 1) (𝓝 1)
x✝ : α × α
⊢ ((fun x => x.2 / x.1) ∘ fun x => (f x.1, f x.2)) x✝ = f (x✝.2 / x✝.1)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : UniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (⇑f) (𝓝 1) (𝓝 1)
this : ((fun x => x.2 / x.1) ∘ fun x => (f x.1, f x.2)) = fun x => f (x.2 / x.1)
⊢ UniformContinuous ⇑f

Tactic:
rw [UniformContinuous, uniformity_eq_comap_nhds_one α, uniformity_eq_comap_nhds_one β,
  tendsto_comap_iff, this]

Result:
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : UniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (⇑f) (𝓝 1) (𝓝 1)
this : ((fun x => x.2 / x.1) ∘ fun x => (f x.1, f x.2)) = fun x => f (x.2 / x.1)
⊢ Tendsto (fun x => f (x.2 / x.1)) (comap (fun x => x.2 / x.1) (𝓝 1)) (𝓝 1)