case refine'_1
α : Type u
β : Type v
X : Type ?u.429067
ι : Type ?u.429070
inst✝² : PseudoMetricSpace α
π : β → Type ?u.429078
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x y x' y' : β → ℝ
hx : x ∈ Set.Icc x' y'
hy : y ∈ Set.Icc x' y'
b : β
⊢ x b ∈ Set.Icc (x' b) (y' b)

case refine'_2
α : Type u
β : Type v
X : Type ?u.429067
ι : Type ?u.429070
inst✝² : PseudoMetricSpace α
π : β → Type ?u.429078
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x y x' y' : β → ℝ
hx : x ∈ Set.Icc x' y'
hy : y ∈ Set.Icc x' y'
b : β
⊢ y b ∈ Set.Icc (x' b) (y' b)
α : Type u
β : Type v
X : Type ?u.429067
ι : Type ?u.429070
inst✝² : PseudoMetricSpace α
π : β → Type ?u.429078
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x y x' y' : β → ℝ
hx : x ∈ Set.Icc x' y'
hy : y ∈ Set.Icc x' y'
⊢ dist x y ≤ dist x' y'
refine' (dist_pi_le_iff dist_nonneg).2 fun b =>
  (Real.dist_le_of_mem_uIcc _ _).trans (dist_le_pi_dist x' y' b) <;> refine' Icc_subset_uIcc _
no goals
case refine'_1
α : Type u
β : Type v
X : Type ?u.429067
ι : Type ?u.429070
inst✝² : PseudoMetricSpace α
π : β → Type ?u.429078
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x y x' y' : β → ℝ
hx : x ∈ Set.Icc x' y'
hy : y ∈ Set.Icc x' y'
b : β
⊢ x b ∈ Set.Icc (x' b) (y' b)

case refine'_2
α : Type u
β : Type v
X : Type ?u.429067
ι : Type ?u.429070
inst✝² : PseudoMetricSpace α
π : β → Type ?u.429078
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x y x' y' : β → ℝ
hx : x ∈ Set.Icc x' y'
hy : y ∈ Set.Icc x' y'
b : β
⊢ y b ∈ Set.Icc (x' b) (y' b)
exacts [⟨hx.1 _, hx.2 _⟩, ⟨hy.1 _, hy.2 _⟩]