[GOAL]
E : Type u_1
inst✝ : SeminormedAddCommGroup E
x y : Completion E
⊢ dist x y = ‖x - y‖
[PROOFSTEP]
induction x, y using Completion.induction_on₂
[GOAL]
case hp
E : Type u_1
inst✝ : SeminormedAddCommGroup E
⊢ IsClosed {x | dist x.fst x.snd = ‖x.fst - x.snd‖}
[PROOFSTEP]
refine' isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous _
[GOAL]
case hp
E : Type u_1
inst✝ : SeminormedAddCommGroup E
⊢ Continuous fun x => ‖x.fst - x.snd‖
[PROOFSTEP]
exact Continuous.comp Completion.continuous_extension continuous_sub
[GOAL]
case ih
E : Type u_1
inst✝ : SeminormedAddCommGroup E
a✝ b✝ : E
⊢ dist (↑E a✝) (↑E b✝) = ‖↑E a✝ - ↑E b✝‖
[PROOFSTEP]
rw [← Completion.coe_sub, norm_coe, Completion.dist_eq, dist_eq_norm]
