-- Mathlib/Topology/MetricSpace/Ultra/Basic.lean
lemma ball_subset_trichotomy :
    ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball 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 → ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : ¬r ≤ s
⊢ ball y s ⊆ ball x r ∨ ball x r ⊆ ball y s ∨ Disjoint (ball y s) (ball x r)

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

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 : (ball x r ∩ ball y s).Nonempty
hxz : h.some ∈ ball x r
hyz : h.some ∈ ball y s
hx : ball x r ⊆ ball x s
⊢ ball x r ⊆ ball y s

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

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball 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 → ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : ¬r ≤ s
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball 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
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)

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 : (ball x r ∩ ball y s).Nonempty
⊢ ball x r ⊆ ball 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 : (ball x r ∩ ball y s).Nonempty
hxz : h.some ∈ ball x r
hyz : h.some ∈ ball y s
⊢ ball x r ⊆ ball 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 : (ball x r ∩ ball y s).Nonempty
hxz : h.some ∈ ball x r
hyz : h.some ∈ ball y s
⊢ ball x r ⊆ ball y s

Tactic:
have hx := ball_subset_ball 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 : (ball x r ∩ ball y s).Nonempty
hxz : h.some ∈ ball x r
hyz : h.some ∈ ball y s
hx : ball x r ⊆ ball x s
⊢ ball x r ⊆ ball 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 → ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : ¬r ≤ s
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball 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 → ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : ¬r ≤ s
⊢ ball y s ⊆ ball x r ∨ ball x r ⊆ ball y s ∨ Disjoint (ball y s) (ball x r)