α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type ?u.20377
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
⊢ compare pkg pkg' ∘ compare pkg' pkg = id
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type ?u.20377
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
⊢ compare pkg pkg' ∘ compare pkg' pkg = id
have uc := pkg.uniformContinuous_compare pkg'
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type ?u.20377
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
⊢ compare pkg pkg' ∘ compare pkg' pkg = id
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type ?u.20377
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
⊢ compare pkg pkg' ∘ compare pkg' pkg = id
have uc' := pkg'.uniformContinuous_compare pkg
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type ?u.20377
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
⊢ ∀ (a : α), (compare pkg pkg' ∘ compare pkg' pkg) (coe pkg' a) = id (coe pkg' a)
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type ?u.20377
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
⊢ compare pkg pkg' ∘ compare pkg' pkg = id
apply pkg'.funext (uc.comp uc').continuous continuous_id
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type ?u.20377
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
a : α
⊢ (compare pkg pkg' ∘ compare pkg' pkg) (coe pkg' a) = id (coe pkg' a)
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type ?u.20377
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
⊢ ∀ (a : α), (compare pkg pkg' ∘ compare pkg' pkg) (coe pkg' a) = id (coe pkg' a)
intro a
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type ?u.20377
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
a : α
⊢ coe pkg' a = id (coe pkg' a)
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type ?u.20377
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
a : α
⊢ (compare pkg pkg' ∘ compare pkg' pkg) (coe pkg' a) = id (coe pkg' a)
rw [comp_apply, pkg'.compare_coe pkg, pkg.compare_coe pkg']
no goals
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type ?u.20377
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
a : α
⊢ coe pkg' a = id (coe pkg' a)
rfl