[GOAL]
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ AbstractCompletion.extend pkg f (coe pkg a) = f a
[PROOFSTEP]
rw [pkg.extend_def hf]
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ DenseInducing.extend (_ : DenseInducing pkg.coe) f (coe pkg a) = f a
[PROOFSTEP]
exact pkg.denseInducing.extend_eq hf.continuous a
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
⊢ UniformContinuous (AbstractCompletion.extend pkg f)
[PROOFSTEP]
by_cases hf : UniformContinuous f
[GOAL]
case pos
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (AbstractCompletion.extend pkg f)
[PROOFSTEP]
rw [pkg.extend_def hf]
[GOAL]
case pos
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (DenseInducing.extend (_ : DenseInducing pkg.coe) f)
[PROOFSTEP]
exact uniformContinuous_uniformly_extend pkg.uniformInducing pkg.dense hf
[GOAL]
case neg
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous (AbstractCompletion.extend pkg f)
[PROOFSTEP]
change UniformContinuous (ite _ _ _)
[GOAL]
case neg
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous
    (if UniformContinuous f then DenseInducing.extend (_ : DenseInducing pkg.coe) f
    else fun x => f (DenseRange.some (_ : DenseRange pkg.coe) x))
[PROOFSTEP]
rw [if_neg hf]
[GOAL]
case neg
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x => f (DenseRange.some (_ : DenseRange pkg.coe) x)
[PROOFSTEP]
exact uniformContinuous_of_const fun a b => by congr 1
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
a b : pkg.space
⊢ f (DenseRange.some (_ : DenseRange pkg.coe) a) = f (DenseRange.some (_ : DenseRange pkg.coe) b)
[PROOFSTEP]
congr 1
[GOAL]
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (coe pkg a)
⊢ AbstractCompletion.extend pkg f = g
[PROOFSTEP]
apply pkg.funext pkg.continuous_extend hg.continuous
[GOAL]
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (coe pkg a)
⊢ ∀ (a : α), AbstractCompletion.extend pkg f (coe pkg a) = g (coe pkg a)
[PROOFSTEP]
simpa only [pkg.extend_coe hf] using h
[GOAL]
α : 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)
[PROOFSTEP]
intro a
[GOAL]
α : 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)
[PROOFSTEP]
change pkg.extend (ι' ∘ f) _ = _
[GOAL]
α : 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)
[PROOFSTEP]
simp only [(· ∘ ·), h, ← comp_apply (f := g)]
[GOAL]
α : 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
[PROOFSTEP]
rw [pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)]
[GOAL]
α : Type u_1
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝³ : UniformSpace β
pkg' : AbstractCompletion β
f✝ : α → β
γ : Type u_3
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)
[PROOFSTEP]
rw [pkg.extend_coe (hf.comp hg), comp_apply, pkg.map_coe pkg' hg, pkg'.extend_coe hf]
[GOAL]
α : Type u_1
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝³ : UniformSpace β
pkg' : AbstractCompletion β
f✝ : α → β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : SeparatedSpace γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ f (g a) = (f ∘ g) a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
⊢ compare pkg pkg' ∘ compare pkg' pkg = id
[PROOFSTEP]
have uc := pkg.uniformContinuous_compare pkg'
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
⊢ compare pkg pkg' ∘ compare pkg' pkg = id
[PROOFSTEP]
have uc' := pkg'.uniformContinuous_compare pkg
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
⊢ compare pkg pkg' ∘ compare pkg' pkg = id
[PROOFSTEP]
apply pkg'.funext (uc.comp uc').continuous continuous_id
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
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)
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
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)
[PROOFSTEP]
rw [comp_apply, pkg'.compare_coe pkg, pkg.compare_coe pkg']
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion α
uc : UniformContinuous (compare pkg pkg')
uc' : UniformContinuous (compare pkg' pkg)
a : α
⊢ coe pkg' a = id (coe pkg' a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
pkg' : AbstractCompletion β
γ : Type u_3
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous₂ (AbstractCompletion.extend₂ pkg pkg' f)
[PROOFSTEP]
rw [uniformContinuous₂_def, AbstractCompletion.extend₂, uncurry_curry]
[GOAL]
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
pkg' : AbstractCompletion β
γ : Type u_3
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous (AbstractCompletion.extend (AbstractCompletion.prod pkg pkg') (uncurry f))
[PROOFSTEP]
apply uniformContinuous_extend
