ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i j : ι
h : i ≠ j
x : E i
y : E j
⊢ 1 ≤ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i j : ι
h : i ≠ j
x : E i
y : E j
⊢ 1 ≤ dist { fst := i, snd := x } { fst := j, snd := y }
rw [Sigma.dist_ne h x y]
no goals
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i j : ι
h : i ≠ j
x : E i
y : E j
⊢ 1 ≤ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y
linarith [@dist_nonneg _ _ x (Nonempty.some ⟨x⟩), @dist_nonneg _ _ (Nonempty.some ⟨y⟩) y]