α : Type u_3
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝³ : UniformSpace β
pkg' : AbstractCompletion β
f✝ : α → β
γ : Type u_1
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : SeparatedSpace γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ f (g a) = (f ∘ g) a
α : Type u_3
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝³ : UniformSpace β
pkg' : AbstractCompletion β
f✝ : α → β
γ : Type u_1
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : SeparatedSpace γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ (AbstractCompletion.extend pkg' f ∘ AbstractCompletion.map pkg pkg' g) (coe pkg a) =
    AbstractCompletion.extend pkg (f ∘ g) (coe pkg a)
rw [pkg.extend_coe (hf.comp hg), comp_apply, pkg.map_coe pkg' hg, pkg'.extend_coe hf]
no goals
α : Type u_3
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝³ : UniformSpace β
pkg' : AbstractCompletion β
f✝ : α → β
γ : Type u_1
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : SeparatedSpace γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ f (g a) = (f ∘ g) a
rfl