case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ IsClosed {a | dist a a = 0}

case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ ∀ (a : α), dist (↑α a) (↑α a) = 0
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ dist x x = 0
refine' induction_on x _ _
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ Continuous fun a => dist a a
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ IsClosed {a | dist a a = 0}
refine' isClosed_eq _ continuous_const
no goals
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ Continuous fun a => dist a a
exact Completion.continuous_dist continuous_id continuous_id
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
a : α
⊢ dist (↑α a) (↑α a) = 0
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ ∀ (a : α), dist (↑α a) (↑α a) = 0
intro a
no goals
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
a : α
⊢ dist (↑α a) (↑α a) = 0
rw [Completion.dist_eq, dist_self]