case inl
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ dist x x ≤ max (dist x y) (dist y x)

case inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
⊢ dist x z ≤ max (dist x y) (dist y z)
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
⊢ dist x z ≤ max (dist x y) (dist y z)
rcases eq_or_ne x z with (rfl | hxz)
case inr.inl
E : ℕ → Type u_1
x z : (n : ℕ) → E n
hxz : x ≠ z
⊢ dist x z ≤ max (dist x x) (dist x z)

case inr.inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
⊢ dist x z ≤ max (dist x y) (dist y z)
case inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
⊢ dist x z ≤ max (dist x y) (dist y z)
rcases eq_or_ne x y with (rfl | hxy)
case inr.inr.inl
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy hxz : x ≠ y
⊢ dist x y ≤ max (dist x y) (dist y y)

case inr.inr.inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
hyz : y ≠ z
⊢ dist x z ≤ max (dist x y) (dist y z)
case inr.inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
⊢ dist x z ≤ max (dist x y) (dist y z)
rcases eq_or_ne y z with (rfl | hyz)
no goals
case inr.inr.inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
hyz : y ≠ z
⊢ dist x z ≤ max (dist x y) (dist y z)
simp only [dist_eq_of_ne, hxz, hxy, hyz, inv_le_inv, one_div, inv_pow, zero_lt_two, Ne.def,
  not_false_iff, le_max_iff, pow_le_pow_iff, one_lt_two, pow_pos,
  min_le_iff.1 (min_firstDiff_le x y z hxz)]
no goals
case inl
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ dist x x ≤ max (dist x y) (dist y x)
simp [PiNat.dist_self x, PiNat.dist_nonneg]
no goals
case inr.inl
E : ℕ → Type u_1
x z : (n : ℕ) → E n
hxz : x ≠ z
⊢ dist x z ≤ max (dist x x) (dist x z)
simp
no goals
case inr.inr.inl
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy hxz : x ≠ y
⊢ dist x y ≤ max (dist x y) (dist y y)
simp