α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β → γ
h : ∀ (a : α) (c : β) (b : α) (d : β), (a, b) ∈ 𝓢 α → (c, d) ∈ 𝓢 β → f a c = f b d
hf : UniformContinuous fun p => f p.fst p.snd
⊢ Tendsto
    (((fun x => (Quotient.lift₂ f h x.fst.fst x.fst.snd, Quotient.lift₂ f h x.snd.fst x.snd.snd)) ∘ fun p =>
        ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ∘
      fun p =>
      ((Quotient.mk (separationSetoid α) p.fst.fst, Quotient.mk (separationSetoid α) p.fst.snd),
        Quotient.mk (separationSetoid β) p.snd.fst, Quotient.mk (separationSetoid β) p.snd.snd))
    (𝓤 α ×ˢ 𝓤 β) (𝓤 γ)
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β → γ
h : ∀ (a : α) (c : β) (b : α) (d : β), (a, b) ∈ 𝓢 α → (c, d) ∈ 𝓢 β → f a c = f b d
hf : UniformContinuous fun p => f p.fst p.snd
⊢ UniformContinuous fun p => Quotient.lift₂ f h p.fst p.snd
rw [UniformContinuous, uniformity_prod_eq_prod, uniformity_quotient, uniformity_quotient,
  Filter.prod_map_map_eq, Filter.tendsto_map'_iff, Filter.tendsto_map'_iff]
no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β → γ
h : ∀ (a : α) (c : β) (b : α) (d : β), (a, b) ∈ 𝓢 α → (c, d) ∈ 𝓢 β → f a c = f b d
hf : UniformContinuous fun p => f p.fst p.snd
⊢ Tendsto
    (((fun x => (Quotient.lift₂ f h x.fst.fst x.fst.snd, Quotient.lift₂ f h x.snd.fst x.snd.snd)) ∘ fun p =>
        ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ∘
      fun p =>
      ((Quotient.mk (separationSetoid α) p.fst.fst, Quotient.mk (separationSetoid α) p.fst.snd),
        Quotient.mk (separationSetoid β) p.snd.fst, Quotient.mk (separationSetoid β) p.snd.snd))
    (𝓤 α ×ˢ 𝓤 β) (𝓤 γ)
rwa [UniformContinuous, uniformity_prod_eq_prod, Filter.tendsto_map'_iff] at hf