-- Mathlib/Topology/MetricSpace/Ultra/Basic.lean
lemma isClosed_ball (x : X) (r : ℝ) : IsClosed (ball x r)

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
⊢ IsClosed (ball x r)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff]

Result:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
⊢ ∀ x_1 ∈ (ball x r)ᶜ, ∃ ε > 0, ball x_1 ε ⊆ (ball x r)ᶜ

Proof state:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≤ 0
⊢ IsClosed (ball x r)

Tactic:
simp [ball_eq_empty.mpr hr]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
⊢ IsClosed (ball x r)

Tactic:
cases le_or_lt r 0 with
| inl hr =>
  simp [ball_eq_empty.mpr hr]
| inr h =>
  rw [← isOpen_compl_iff, isOpen_iff]
  simp only [Set.mem_compl_iff, not_lt, gt_iff_lt]
  intro y hy
  cases ball_eq_or_disjoint x y r with
  | inl hd =>
    rw [hd] at hy
    simp [h.not_le] at hy
  | inr hd =>
    use r
    simp [h, hy, ← Set.le_iff_subset, le_compl_iff_disjoint_left, hd]

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
⊢ ∀ x_1 ∈ (ball x r)ᶜ, ∃ ε > 0, ball x_1 ε ⊆ (ball x r)ᶜ

Tactic:
simp only [Set.mem_compl_iff, not_lt, gt_iff_lt]

Result:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
⊢ ∀ x_1 ∉ ball x r, ∃ ε, 0 < ε ∧ ball x_1 ε ⊆ (ball x r)ᶜ

Proof state:
case inr.inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball y r
hd : ball x r = ball y r
⊢ ∃ ε, 0 < ε ∧ ball y ε ⊆ (ball x r)ᶜ

Tactic:
simp [h.not_le] at hy

Result:
no goals

Proof state:
case inr.inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball x r
hd : Disjoint (ball x r) (ball y r)
⊢ ∃ ε, 0 < ε ∧ ball y ε ⊆ (ball x r)ᶜ

Tactic:
use r

Result:
case h
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball x r
hd : Disjoint (ball x r) (ball y r)
⊢ 0 < r ∧ ball y r ⊆ (ball x r)ᶜ

Proof state:
case inr.inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball x r
hd : ball x r = ball y r
⊢ ∃ ε, 0 < ε ∧ ball y ε ⊆ (ball x r)ᶜ

Tactic:
rw [hd] at hy

Result:
case inr.inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball y r
hd : ball x r = ball y r
⊢ ∃ ε, 0 < ε ∧ ball y ε ⊆ (ball x r)ᶜ

Proof state:
case h
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball x r
hd : Disjoint (ball x r) (ball y r)
⊢ 0 < r ∧ ball y r ⊆ (ball x r)ᶜ

Tactic:
simp [h, hy, ← Set.le_iff_subset, le_compl_iff_disjoint_left, hd]

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball x r
⊢ ∃ ε, 0 < ε ∧ ball y ε ⊆ (ball x r)ᶜ

Tactic:
cases ball_eq_or_disjoint x y r with
| inl hd =>
  rw [hd] at hy
  simp [h.not_le] at hy
| inr hd =>
  use r
  simp [h, hy, ← Set.le_iff_subset, le_compl_iff_disjoint_left, hd]

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
⊢ ∀ x_1 ∉ ball x r, ∃ ε, 0 < ε ∧ ball x_1 ε ⊆ (ball x r)ᶜ

Tactic:
intro y hy

Result:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball x r
⊢ ∃ ε, 0 < ε ∧ ball y ε ⊆ (ball x r)ᶜ