α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f✝ f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), coe pkg' (f a) = g (coe pkg a)
a : α
⊢ AbstractCompletion.map pkg pkg' f (coe pkg a) = g (coe pkg a)
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f✝ f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), coe pkg' (f a) = g (coe pkg a)
⊢ ∀ (a : α), AbstractCompletion.map pkg pkg' f (coe pkg a) = g (coe pkg a)
intro a
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f✝ f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), coe pkg' (f a) = g (coe pkg a)
a : α
⊢ AbstractCompletion.extend pkg (pkg'.coe ∘ f) (coe pkg a) = g (coe pkg a)
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f✝ f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), coe pkg' (f a) = g (coe pkg a)
a : α
⊢ AbstractCompletion.map pkg pkg' f (coe pkg a) = g (coe pkg a)
change pkg.extend (ι' ∘ f) _ = _
no goals
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f✝ f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), coe pkg' (f a) = g (coe pkg a)
a : α
⊢ AbstractCompletion.extend pkg (fun x => (g ∘ pkg.coe) x) (coe pkg a) = (g ∘ pkg.coe) a
rw [pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)]