case mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
y z : (i : ι) × E i
i : ι
x : E i
⊢ dist { fst := i, snd := x } z ≤ dist { fst := i, snd := x } y + dist y z
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
x y z : (i : ι) × E i
⊢ dist x z ≤ dist x y + dist y z
rcases x with ⟨i, x⟩
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
z : (i : ι) × E i
i : ι
x : E i
j : ι
y : E j
⊢ dist { fst := i, snd := x } z ≤ dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } z
case mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
y z : (i : ι) × E i
i : ι
x : E i
⊢ dist { fst := i, snd := x } z ≤ dist { fst := i, snd := x } y + dist y z
rcases y with ⟨j, y⟩
case mk.mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
⊢ dist { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := k, snd := z }
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
z : (i : ι) × E i
i : ι
x : E i
j : ι
y : E j
⊢ dist { fst := i, snd := x } z ≤ dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } z
rcases z with ⟨k, z⟩
case mk.mk.mk.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
⊢ dist { fst := i, snd := x } { fst := i, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := i, snd := z }

case mk.mk.mk.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
⊢ dist { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := k, snd := z }
case mk.mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
⊢ dist { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := k, snd := z }
rcases eq_or_ne i k with (rfl | hik)
case mk.mk.mk.inl.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x z y : E i
⊢ dist { fst := i, snd := x } { fst := i, snd := z } ≤
    dist { fst := i, snd := x } { fst := i, snd := y } + dist { fst := i, snd := y } { fst := i, snd := z }

case mk.mk.mk.inl.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist { fst := i, snd := x } { fst := i, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := i, snd := z }
case mk.mk.mk.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
⊢ dist { fst := i, snd := x } { fst := i, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := i, snd := z }
rcases eq_or_ne i j with (rfl | hij)
no goals
case mk.mk.mk.inl.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x z y : E i
⊢ dist { fst := i, snd := x } { fst := i, snd := z } ≤
    dist { fst := i, snd := x } { fst := i, snd := y } + dist { fst := i, snd := y } { fst := i, snd := z }
simpa using dist_triangle x y z
case mk.mk.mk.inl.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist x z ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y +
      (dist y (Nonempty.some (_ : Nonempty (E j))) + 1 + dist (Nonempty.some (_ : Nonempty (E i))) z)
case mk.mk.mk.inl.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist { fst := i, snd := x } { fst := i, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := i, snd := z }
simp only [Sigma.dist_same, Sigma.dist_ne hij, Sigma.dist_ne hij.symm]
no goals
case mk.mk.mk.inl.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist x z ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y +
      (dist y (Nonempty.some (_ : Nonempty (E j))) + 1 + dist (Nonempty.some (_ : Nonempty (E i))) z)
calc
  dist x z ≤ dist x (Nonempty.some ⟨x⟩) + 0 + 0 + (0 + 0 + dist (Nonempty.some ⟨z⟩) z) := by
    simpa only [zero_add, add_zero] using dist_triangle _ _ _
  _ ≤ _ := by apply_rules [add_le_add, le_rfl, dist_nonneg, zero_le_one]
no goals
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist x z ≤ dist x (Nonempty.some (_ : Nonempty (E i))) + 0 + 0 + (0 + 0 + dist (Nonempty.some (_ : Nonempty (E i))) z)
simpa only [zero_add, add_zero] using dist_triangle _ _ _
no goals
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 0 + 0 + (0 + 0 + dist (Nonempty.some (_ : Nonempty (E i))) z) ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y +
      (dist y (Nonempty.some (_ : Nonempty (E j))) + 1 + dist (Nonempty.some (_ : Nonempty (E i))) z)
apply_rules [add_le_add, le_rfl, dist_nonneg, zero_le_one]
case mk.mk.mk.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := i, snd := y } + dist { fst := i, snd := y } { fst := k, snd := z }

case mk.mk.mk.inr.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
⊢ dist { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := k, snd := z }
case mk.mk.mk.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
⊢ dist { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := k, snd := z }
rcases eq_or_ne i j with (rfl | hij)
case mk.mk.mk.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z ≤
    dist x y + (dist y (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z)
case mk.mk.mk.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := i, snd := y } + dist { fst := i, snd := y } { fst := k, snd := z }
simp only [Sigma.dist_ne hik, Sigma.dist_same]
no goals
case mk.mk.mk.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z ≤
    dist x y + (dist y (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z)
calc
  dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
      dist x y + dist y (Nonempty.some ⟨y⟩) + 1 + dist (Nonempty.some ⟨z⟩) z :=
    by apply_rules [add_le_add, le_rfl, dist_triangle]
  _ = _ := by abel
no goals
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z ≤
    dist x y + dist y (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z
apply_rules [add_le_add, le_rfl, dist_triangle]
no goals
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist x y + dist y (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z =
    dist x y + (dist y (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z)
abel
case mk.mk.mk.inr.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist { fst := i, snd := x } { fst := j, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := j, snd := z }

case mk.mk.mk.inr.inr.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := k, snd := z }
case mk.mk.mk.inr.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
⊢ dist { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := k, snd := z }
rcases eq_or_ne j k with (rfl | hjk)
case mk.mk.mk.inr.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) z ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y + dist y z
case mk.mk.mk.inr.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist { fst := i, snd := x } { fst := j, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := j, snd := z }
simp only [Sigma.dist_ne hij, Sigma.dist_same]
no goals
case mk.mk.mk.inr.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) z ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y + dist y z
calc
  dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
      dist x (Nonempty.some ⟨x⟩) + 1 + (dist (Nonempty.some ⟨z⟩) y + dist y z) :=
    by apply_rules [add_le_add, le_rfl, dist_triangle]
  _ = _ := by abel
no goals
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) z ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + (dist (Nonempty.some (_ : Nonempty (E j))) y + dist y z)
apply_rules [add_le_add, le_rfl, dist_triangle]
no goals
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + (dist (Nonempty.some (_ : Nonempty (E j))) y + dist y z) =
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y + dist y z
abel
case mk.mk.mk.inr.inr.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y +
      (dist y (Nonempty.some (_ : Nonempty (E j))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z)
case mk.mk.mk.inr.inr.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := k, snd := z }
simp only [hik, hij, hjk, Sigma.dist_ne, Ne.def, not_false_iff]
no goals
case mk.mk.mk.inr.inr.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y +
      (dist y (Nonempty.some (_ : Nonempty (E j))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z)
calc
  dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z =
      dist x (Nonempty.some ⟨x⟩) + 1 + 0 + (0 + 0 + dist (Nonempty.some ⟨z⟩) z) :=
    by simp only [add_zero, zero_add]
  _ ≤ _ := by apply_rules [add_le_add, zero_le_one, dist_nonneg, le_rfl]
no goals
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z =
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + 0 + (0 + 0 + dist (Nonempty.some (_ : Nonempty (E k))) z)
simp only [add_zero, zero_add]
no goals
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + 0 + (0 + 0 + dist (Nonempty.some (_ : Nonempty (E k))) z) ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y +
      (dist y (Nonempty.some (_ : Nonempty (E j))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z)
apply_rules [add_le_add, zero_le_one, dist_nonneg, le_rfl]