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

case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ ∀ (a b c : α), dist (↑α a) (↑α c) ≤ dist (↑α a) (↑α b) + dist (↑α b) (↑α c)
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ dist x z ≤ dist x y + dist y z
refine' induction_on₃ x y z _ _
no goals
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ IsClosed {x | dist x.fst x.snd.snd ≤ dist x.fst x.snd.fst + dist x.snd.fst x.snd.snd}
refine' isClosed_le _ (Continuous.add _ _) <;>
  apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist (↑α a) (↑α c) ≤ dist (↑α a) (↑α b) + dist (↑α b) (↑α c)
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ ∀ (a b c : α), dist (↑α a) (↑α c) ≤ dist (↑α a) (↑α b) + dist (↑α b) (↑α c)
intro a b c
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist b c
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist (↑α a) (↑α c) ≤ dist (↑α a) (↑α b) + dist (↑α b) (↑α c)
rw [Completion.dist_eq, Completion.dist_eq, Completion.dist_eq]
no goals
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist b c
exact dist_triangle a b c