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)

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)
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
⊢ UniformContinuous (AbstractCompletion.extend pkg f)
by_cases hf : UniformContinuous f
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)
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)
rw [pkg.extend_def hf]
no goals
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)
exact uniformContinuous_uniformly_extend pkg.uniformInducing pkg.dense hf
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))
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)
change UniformContinuous (ite _ _ _)
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)
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))
rw [if_neg hf]
no goals
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)
exact uniformContinuous_of_const fun a b => by congr 1
no goals
α : 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)
congr 1