-- Mathlib/Topology/MetricSpace/Ultra/Basic.lean
lemma closedBall_subset_trichotomy :
    closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨
    Disjoint (closedBall x r) (closedBall y s)

Proof state:
case intro
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
h : (closedBall x r ∩ closedBall y s).Nonempty
hxz : h.some ∈ closedBall x r
hyz : h.some ∈ closedBall y s
hx : closedBall x r ⊆ closedBall x s
⊢ closedBall x r ⊆ closedBall y s

Tactic:
rwa [closedBall_eq_of_mem hyz |>.trans (closedBall_eq_of_mem <| hx hxz).symm]

Result:
no goals

Proof state:
case intro
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
h : (closedBall x r ∩ closedBall y s).Nonempty
hxz : h.some ∈ closedBall x r
hyz : h.some ∈ closedBall y s
⊢ closedBall x r ⊆ closedBall y s

Tactic:
have hx := closedBall_subset_closedBall hrs (x := x)

Result:
case intro
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
h : (closedBall x r ∩ closedBall y s).Nonempty
hxz : h.some ∈ closedBall x r
hyz : h.some ∈ closedBall y s
hx : closedBall x r ⊆ closedBall x s
⊢ closedBall x r ⊆ closedBall y s

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)

Tactic:
wlog hrs : r ≤ s generalizing x y r s

Result:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this :
  ∀ (x y : X) (r s : ℝ),
    r ≤ s →
      closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : ¬r ≤ s
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)

X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this :
  ∀ (x y : X) (r s : ℝ),
    r ≤ s →
      closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : ¬r ≤ s
⊢ closedBall y s ⊆ closedBall x r ∨ closedBall x r ⊆ closedBall y s ∨ Disjoint (closedBall y s) (closedBall x r)

Tactic:
exact this y x s r (lt_of_not_le hrs).le

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
h : (closedBall x r ∩ closedBall y s).Nonempty
⊢ closedBall x r ⊆ closedBall y s

Tactic:
obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem

Result:
case intro
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
h : (closedBall x r ∩ closedBall y s).Nonempty
hxz : h.some ∈ closedBall x r
hyz : h.some ∈ closedBall y s
⊢ closedBall x r ⊆ closedBall y s

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this :
  ∀ (x y : X) (r s : ℝ),
    r ≤ s →
      closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : ¬r ≤ s
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)

Tactic:
rw [disjoint_comm, ← or_assoc, or_comm (b := _ ⊆ _), or_assoc]

Result:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this :
  ∀ (x y : X) (r s : ℝ),
    r ≤ s →
      closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : ¬r ≤ s
⊢ closedBall y s ⊆ closedBall x r ∨ closedBall x r ⊆ closedBall y s ∨ Disjoint (closedBall y s) (closedBall x r)