-- Mathlib/Topology/MetricSpace/Ultra/Basic.lean
/-- All triangles are isosceles in an ultrametric space. -/
lemma dist_eq_max_of_dist_ne_dist (h : dist x y ≠ dist y z) :
    dist x z = max (dist x y) (dist y z)

Proof state:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ dist x y ⊔ dist y z ≤ dist x z

Tactic:
rw [max_eq_right h.le]

Result:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ dist y z ≤ dist x z

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h : dist x y ≠ dist y z
⊢ dist x z = dist x y ⊔ dist y z

Tactic:
apply le_antisymm (dist_triangle_max x y z)

Result:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h : dist x y ≠ dist y z
⊢ dist x y ⊔ dist y z ≤ dist x z

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist y z < dist x y
⊢ dist y x ≤ dist z x

Tactic:
apply (le_max_iff.mp <| dist_triangle_max y z x).resolve_left

Result:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist y z < dist x y
⊢ ¬dist y x ≤ dist y z

Proof state:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ dist y z ≤ dist x z

Tactic:
apply (le_max_iff.mp <| dist_triangle_max y x z).resolve_left

Result:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ ¬dist y z ≤ dist y x

Proof state:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ ¬dist y z ≤ dist y x

Tactic:
simpa only [not_le, dist_comm x y] using h

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist y z < dist x y
⊢ ¬dist y x ≤ dist y z

Tactic:
simpa only [not_le, dist_comm x y] using h

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist y z < dist x y
⊢ dist x y ⊔ dist y z ≤ dist x z

Tactic:
rw [max_eq_left h.le, dist_comm x y, dist_comm x z]

Result:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist y z < dist x y
⊢ dist y x ≤ dist z x

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h : dist x y ≠ dist y z
⊢ dist x y ⊔ dist y z ≤ dist x z

Tactic:
rcases h.lt_or_lt with h | h

Result:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ dist x y ⊔ dist y z ≤ dist x z

case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist y z < dist x y
⊢ dist x y ⊔ dist y z ≤ dist x z