case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ IsClosed {x | dist x.fst x.snd = dist x.snd x.fst}

case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ ∀ (a b : α), dist (↑α a) (↑α b) = dist (↑α b) (↑α a)
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ dist x y = dist y x
refine' induction_on₂ x y _ _
no goals
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ IsClosed {x | dist x.fst x.snd = dist x.snd x.fst}
exact isClosed_eq (Completion.continuous_dist continuous_fst continuous_snd)
    (Completion.continuous_dist continuous_snd continuous_fst)
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
a b : α
⊢ dist (↑α a) (↑α b) = dist (↑α b) (↑α a)
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ ∀ (a b : α), dist (↑α a) (↑α b) = dist (↑α b) (↑α a)
intro a b
no goals
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
a b : α
⊢ dist (↑α a) (↑α b) = dist (↑α b) (↑α a)
rw [Completion.dist_eq, Completion.dist_eq, dist_comm]