α : Type u_3
inst✝⁴ : UniformSpace α
β : Type u_2
inst✝³ : UniformSpace β
γ : Type u_1
inst✝² : UniformSpace γ
f✝ : α → β
inst✝¹ : CompleteSpace γ
inst✝ : SeparatedSpace γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ (Completion.extension f ∘ Completion.map g) (↑α a) = Completion.extension (f ∘ g) (↑α a)
α : Type u_3
inst✝⁴ : UniformSpace α
β : Type u_2
inst✝³ : UniformSpace β
γ : Type u_1
inst✝² : UniformSpace γ
f✝ : α → β
inst✝¹ : CompleteSpace γ
inst✝ : SeparatedSpace γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
⊢ ∀ (a : α), (Completion.extension f ∘ Completion.map g) (↑α a) = Completion.extension (f ∘ g) (↑α a)
intro a
no goals
α : Type u_3
inst✝⁴ : UniformSpace α
β : Type u_2
inst✝³ : UniformSpace β
γ : Type u_1
inst✝² : UniformSpace γ
f✝ : α → β
inst✝¹ : CompleteSpace γ
inst✝ : SeparatedSpace γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ (Completion.extension f ∘ Completion.map g) (↑α a) = Completion.extension (f ∘ g) (↑α a)
rw [extension_coe (hf.comp hg), Function.comp_apply, map_coe hg, extension_coe hf,
  Function.comp_apply]