Theorem: Countable.totallyDisconnectedSpace (Ray/Misc/TotallyDisconnected.lean)

State before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
⊢ TotallyDisconnectedSpace X
Tactic:
generalize hR : {r | ∃ x y : X, dist x y = r} = R
State after:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
⊢ TotallyDisconnectedSpace X

State before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
⊢ TotallyDisconnectedSpace X
Tactic:
have rc : R.Countable := by
  have e : R = range (uncurry dist) := by
    apply Set.ext; intro r; simp only [mem_setOf, mem_range, Prod.exists, uncurry, ← hR]; rfl
  rw [e]; exact countable_range _
State after:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
⊢ TotallyDisconnectedSpace X

State before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
⊢ TotallyDisconnectedSpace X
Tactic:
refine ⟨?_⟩
State after:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
⊢ IsTotallyDisconnected univ

State before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
⊢ IsTotallyDisconnected univ
Tactic:
apply isTotallyDisconnected_of_isClopen_set
State after:
case hX
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
⊢ Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U

State before:
case hX
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
⊢ Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
Tactic:
intro x y xy
State after:
case hX
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : x ≠ y
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U

State before:
case hX
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : x ≠ y
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
Tactic:
rw [← dist_pos] at xy
State after:
case hX
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U

State before:
case hX
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
Tactic:
have h : ¬Ioo 0 (dist x y) ⊆ R := by by_contra h; exact not_countable_Ioo xy (rc.mono h)
State after:
case hX
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
h : ¬Ioo 0 (dist x y) ⊆ R
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U

State before:
case hX
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
h : ¬Ioo 0 (dist x y) ⊆ R
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
Tactic:
simp only [not_subset, mem_Ioo] at h
State after:
case hX
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
h : ∃ a, (0 < a ∧ a < dist x y) ∧ a ∉ R
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U

State before:
case hX
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
h : ∃ a, (0 < a ∧ a < dist x y) ∧ a ∉ R
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
Tactic:
rcases h with ⟨r, ⟨rp, rxy⟩, rr⟩
State after:
case hX.intro.intro.intro
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U

State before:
case hX.intro.intro.intro
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
Tactic:
have e : ball x r = closedBall x r := by
  apply Set.ext; intro z; simp only [mem_ball, mem_closedBall]
  simp only [mem_setOf, not_exists, ← hR] at rr; simp only [Ne.le_iff_lt (rr z x)]
State after:
case hX.intro.intro.intro
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U

State before:
case hX.intro.intro.intro
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
Tactic:
refine ⟨ball x r, ⟨?_, isOpen_ball⟩, ?_⟩
State after:
case hX.intro.intro.intro.refine_1
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ IsClosed (ball x r)

case hX.intro.intro.intro.refine_2
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ x ∈ ball x r ∧ y ∉ ball x r

State before:
case hX.intro.intro.intro.refine_1
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ IsClosed (ball x r)

case hX.intro.intro.intro.refine_2
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ x ∈ ball x r ∧ y ∉ ball x r
Tactic:
rw [e]
State after:
case hX.intro.intro.intro.refine_1
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ IsClosed (closedBall x r)

case hX.intro.intro.intro.refine_2
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ x ∈ ball x r ∧ y ∉ ball x r

State before:
case hX.intro.intro.intro.refine_1
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ IsClosed (closedBall x r)

case hX.intro.intro.intro.refine_2
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ x ∈ ball x r ∧ y ∉ ball x r
Tactic:
exact isClosed_ball
State after:
case hX.intro.intro.intro.refine_2
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ x ∈ ball x r ∧ y ∉ ball x r

State before:
case hX.intro.intro.intro.refine_2
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ x ∈ ball x r ∧ y ∉ ball x r
Tactic:
use mem_ball_self rp
State after:
case right
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ y ∉ ball x r

State before:
case right
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ y ∉ ball x r
Tactic:
simp only [mem_ball, not_lt]
State after:
case right
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ r ≤ dist y x

State before:
case right
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ r ≤ dist y x
Tactic:
rw [dist_comm]
State after:
case right
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ r ≤ dist x y

State before:
case right
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ r ≤ dist x y
Tactic:
exact rxy.le
State after:
no goals

State before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
⊢ R.Countable
Tactic:
have e : R = range (uncurry dist) := by
  apply Set.ext; intro r; simp only [mem_setOf, mem_range, Prod.exists, uncurry, ← hR]; rfl
State after:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
e : R = range (uncurry dist)
⊢ R.Countable

State before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
e : R = range (uncurry dist)
⊢ R.Countable
Tactic:
rw [e]
State after:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
e : R = range (uncurry dist)
⊢ (range (uncurry dist)).Countable

State before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
e : R = range (uncurry dist)
⊢ (range (uncurry dist)).Countable
Tactic:
exact countable_range _
State after:
no goals

State before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
⊢ R = range (uncurry dist)
Tactic:
apply Set.ext
State after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
⊢ ∀ (x : ℝ), x ∈ R ↔ x ∈ range (uncurry dist)

State before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
⊢ ∀ (x : ℝ), x ∈ R ↔ x ∈ range (uncurry dist)
Tactic:
intro r
State after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
r : ℝ
⊢ r ∈ R ↔ r ∈ range (uncurry dist)

State before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
r : ℝ
⊢ r ∈ R ↔ r ∈ range (uncurry dist)
Tactic:
simp only [mem_setOf, mem_range, Prod.exists, uncurry, ← hR]
State after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
r : ℝ
⊢ (∃ x y, dist x y = r) ↔ ∃ a b, dist a b = r

State before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
r : ℝ
⊢ (∃ x y, dist x y = r) ↔ ∃ a b, dist a b = r
Tactic:
rfl
State after:
no goals

State before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
⊢ ¬Ioo 0 (dist x y) ⊆ R
Tactic:
by_contra h
State after:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
h : Ioo 0 (dist x y) ⊆ R
⊢ False

State before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
h : Ioo 0 (dist x y) ⊆ R
⊢ False
Tactic:
exact not_countable_Ioo xy (rc.mono h)
State after:
no goals

State before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
⊢ ball x r = closedBall x r
Tactic:
apply Set.ext
State after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
⊢ ∀ (x_1 : X), x_1 ∈ ball x r ↔ x_1 ∈ closedBall x r

State before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
⊢ ∀ (x_1 : X), x_1 ∈ ball x r ↔ x_1 ∈ closedBall x r
Tactic:
intro z
State after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
z : X
⊢ z ∈ ball x r ↔ z ∈ closedBall x r

State before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
z : X
⊢ z ∈ ball x r ↔ z ∈ closedBall x r
Tactic:
simp only [mem_ball, mem_closedBall]
State after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
z : X
⊢ dist z x < r ↔ dist z x ≤ r

State before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
z : X
⊢ dist z x < r ↔ dist z x ≤ r
Tactic:
simp only [mem_setOf, not_exists, ← hR] at rr
State after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rp : 0 < r
rxy : r < dist x y
z : X
rr : ∀ (x x_1 : X), ¬dist x x_1 = r
⊢ dist z x < r ↔ dist z x ≤ r

State before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rp : 0 < r
rxy : r < dist x y
z : X
rr : ∀ (x x_1 : X), ¬dist x x_1 = r
⊢ dist z x < r ↔ dist z x ≤ r
Tactic:
simp only [Ne.le_iff_lt (rr z x)]
State after:
no goals