-- Mathlib/Topology/MetricSpace/Ultra/Basic.lean
lemma isOpen_closedBall {r : ℝ} (hr : r ≠ 0) : IsOpen (closedBall x r)

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsOpen (closedBall x r)

Tactic:
cases lt_or_gt_of_ne hr with
| inl h =>
  simp [closedBall_eq_empty.mpr h]
| inr h =>
  rw [isOpen_iff]
  simp only [Set.mem_compl_iff, not_lt, gt_iff_lt]
  intro y hy
  cases closedBall_eq_or_disjoint x y r with
  | inl hd =>
    use r
    simp [h, hd, ball_subset_closedBall]
  | inr hd =>
    simp [closedBall_eq_of_mem hy, h.not_lt] at hd

Result:
no goals

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

Tactic:
simp [closedBall_eq_of_mem hy, h.not_lt] at hd

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : r > 0
⊢ IsOpen (closedBall x r)

Tactic:
rw [isOpen_iff]

Result:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : r > 0
⊢ ∀ x_1 ∈ closedBall x r, ∃ ε > 0, ball x_1 ε ⊆ closedBall x r

Proof state:
case h
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : r > 0
y : X
hy : y ∈ closedBall x r
hd : closedBall x r = closedBall y r
⊢ 0 < r ∧ ball y r ⊆ closedBall x r

Tactic:
simp [h, hd, ball_subset_closedBall]

Result:
no goals

Proof state:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : r < 0
⊢ IsOpen (closedBall x r)

Tactic:
simp [closedBall_eq_empty.mpr h]

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : r > 0
y : X
hy : y ∈ closedBall x r
⊢ ∃ ε, 0 < ε ∧ ball y ε ⊆ closedBall x r

Tactic:
cases closedBall_eq_or_disjoint x y r with
| inl hd =>
  use r
  simp [h, hd, ball_subset_closedBall]
| inr hd =>
  simp [closedBall_eq_of_mem hy, h.not_lt] at hd

Result:
no goals

Proof state:
case inr.inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : r > 0
y : X
hy : y ∈ closedBall x r
hd : closedBall x r = closedBall y r
⊢ ∃ ε, 0 < ε ∧ ball y ε ⊆ closedBall x r

Tactic:
use r

Result:
case h
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : r > 0
y : X
hy : y ∈ closedBall x r
hd : closedBall x r = closedBall y r
⊢ 0 < r ∧ ball y r ⊆ closedBall x r

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

Tactic:
intro y hy

Result:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : r > 0
y : X
hy : y ∈ closedBall x r
⊢ ∃ ε, 0 < ε ∧ ball y ε ⊆ closedBall x r

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : r > 0
⊢ ∀ x_1 ∈ closedBall x r, ∃ ε > 0, ball x_1 ε ⊆ closedBall 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 : ℝ
hr : r ≠ 0
h : r > 0
⊢ ∀ x_1 ∈ closedBall x r, ∃ ε, 0 < ε ∧ ball x_1 ε ⊆ closedBall x r