internlm/Lean-Github huggingface dataset:
Theorem: Set.Nonempty.continuousOn_invCoe
Proof state before:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
⊢ ContinuousOn (Subtype.val ∘ ne.invCoe) s
Tactic:
apply continuousOn_id.congr
Proof state after:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
⊢ EqOn (Subtype.val ∘ ne.invCoe) id s
Theorem: Set.Nonempty.continuousOn_invCoe
Proof state before:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
⊢ EqOn (Subtype.val ∘ ne.invCoe) id s
Tactic:
intro x m
Proof state after:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
x : X
m : x ∈ s
⊢ (Subtype.val ∘ ne.invCoe) x = id x
Theorem: Set.Nonempty.continuousOn_invCoe
Proof state before:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
x : X
m : x ∈ s
⊢ (Subtype.val ∘ ne.invCoe) x = id x
Tactic:
simp only [Function.comp, ne.right_invCoe _ m, id]
Proof state after:
no goals
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
X : Type
inst✝ : TopologicalSpace X
s : Set X
⊢ TotallyDisconnectedSpace ↑s ↔ IsTotallyDisconnected s
Tactic:
constructor
Proof state after:
case mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
⊢ TotallyDisconnectedSpace ↑s → IsTotallyDisconnected s

case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
⊢ IsTotallyDisconnected s → TotallyDisconnectedSpace ↑s
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
⊢ TotallyDisconnectedSpace ↑s → IsTotallyDisconnected s
Tactic:
intro h
Proof state after:
case mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
⊢ IsTotallyDisconnected s
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
⊢ IsTotallyDisconnected s
Tactic:
by_cases ne : s.Nonempty
Proof state after:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
⊢ IsTotallyDisconnected s

case neg
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : ¬s.Nonempty
⊢ IsTotallyDisconnected s
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
⊢ IsTotallyDisconnected s
Tactic:
intro t ts tc
Proof state after:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
⊢ t.Subsingleton
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
⊢ t.Subsingleton
Tactic:
set t' := ne.invCoe '' t
Proof state after:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
⊢ t.Subsingleton
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
⊢ t.Subsingleton
Tactic:
have tc' : IsPreconnected t' := tc.image _ (ne.continuousOn_invCoe.mono ts)
Proof state after:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
⊢ t.Subsingleton
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
⊢ t.Subsingleton
Tactic:
have q := h.isTotallyDisconnected_univ _ (subset_univ _) tc'
Proof state after:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
⊢ t.Subsingleton
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
e : t = (fun x => ↑x) '' t'
⊢ t.Subsingleton
Tactic:
rw [e]
Proof state after:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
e : t = (fun x => ↑x) '' t'
⊢ ((fun x => ↑x) '' t').Subsingleton
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
e : t = (fun x => ↑x) '' t'
⊢ ((fun x => ↑x) '' t').Subsingleton
Tactic:
exact q.image _
Proof state after:
no goals
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
⊢ t = (fun x => ↑x) '' t'
Tactic:
apply Set.ext
Proof state after:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
⊢ ∀ (x : X), x ∈ t ↔ x ∈ (fun x => ↑x) '' t'
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
⊢ ∀ (x : X), x ∈ t ↔ x ∈ (fun x => ↑x) '' t'
Tactic:
intro x
Proof state after:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ x ∈ t ↔ x ∈ (fun x => ↑x) '' t'
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ x ∈ t ↔ x ∈ (fun x => ↑x) '' t'
Tactic:
simp only [mem_image]
Proof state after:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ x ∈ t ↔ ∃ x_1 ∈ t', ↑x_1 = x
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ x ∈ t ↔ ∃ x_1 ∈ t', ↑x_1 = x
Tactic:
constructor
Proof state after:
case h.mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ x ∈ t → ∃ x_1 ∈ t', ↑x_1 = x

case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ (∃ x_1 ∈ t', ↑x_1 = x) → x ∈ t
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case h.mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ x ∈ t → ∃ x_1 ∈ t', ↑x_1 = x
Tactic:
intro xt
Proof state after:
case h.mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ∃ x_1 ∈ t', ↑x_1 = x
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case h.mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ∃ x_1 ∈ t', ↑x_1 = x
Tactic:
use ⟨x, ts xt⟩
Proof state after:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ⟨x, ⋯⟩ ∈ t' ∧ ↑⟨x, ⋯⟩ = x
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ⟨x, ⋯⟩ ∈ t' ∧ ↑⟨x, ⋯⟩ = x
Tactic:
refine ⟨⟨x,xt,?_⟩,?_⟩
Proof state after:
case h.refine_1
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ne.invCoe x = ⟨x, ⋯⟩

case h.refine_2
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ↑⟨x, ⋯⟩ = x
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case h.refine_1
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ne.invCoe x = ⟨x, ⋯⟩

case h.refine_2
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ↑⟨x, ⋯⟩ = x
Tactic:
simp only [Subtype.ext_iff, Subtype.coe_mk, ne.right_invCoe _ (ts xt)]
Proof state after:
case h.refine_2
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ↑⟨x, ⋯⟩ = x
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case h.refine_2
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ↑⟨x, ⋯⟩ = x
Tactic:
rw [Subtype.coe_mk]
Proof state after:
no goals
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ (∃ x_1 ∈ t', ↑x_1 = x) → x ∈ t
Tactic:
intro ⟨⟨y, ys⟩, ⟨z, zt, zy⟩, yx⟩
Proof state after:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x y : X
ys : y ∈ s
z : X
zt : z ∈ t
zy : ne.invCoe z = ⟨y, ys⟩
yx : ↑⟨y, ys⟩ = x
⊢ x ∈ t
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x y : X
ys : y ∈ s
z : X
zt : z ∈ t
zy : ne.invCoe z = ⟨y, ys⟩
yx : ↑⟨y, ys⟩ = x
⊢ x ∈ t
Tactic:
simp only [Subtype.coe_mk, Subtype.ext_iff, ne.right_invCoe _ (ts zt)] at yx zy
Proof state after:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x y : X
ys : y ∈ s
z : X
zt : z ∈ t
yx : y = x
zy : z = y
⊢ x ∈ t
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x y : X
ys : y ∈ s
z : X
zt : z ∈ t
yx : y = x
zy : z = y
⊢ x ∈ t
Tactic:
rw [← yx, ← zy]
Proof state after:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x y : X
ys : y ∈ s
z : X
zt : z ∈ t
yx : y = x
zy : z = y
⊢ z ∈ t
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x y : X
ys : y ∈ s
z : X
zt : z ∈ t
yx : y = x
zy : z = y
⊢ z ∈ t
Tactic:
exact zt
Proof state after:
no goals
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case neg
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : ¬s.Nonempty
⊢ IsTotallyDisconnected s
Tactic:
simp only [not_nonempty_iff_eq_empty] at ne
Proof state after:
case neg
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s = ∅
⊢ IsTotallyDisconnected s
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case neg
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s = ∅
⊢ IsTotallyDisconnected s
Tactic:
rw [ne]
Proof state after:
case neg
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s = ∅
⊢ IsTotallyDisconnected ∅
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case neg
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s = ∅
⊢ IsTotallyDisconnected ∅
Tactic:
exact isTotallyDisconnected_empty
Proof state after:
no goals
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
⊢ IsTotallyDisconnected s → TotallyDisconnectedSpace ↑s
Tactic:
intro h
Proof state after:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ TotallyDisconnectedSpace ↑s
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ TotallyDisconnectedSpace ↑s
Tactic:
refine ⟨?_⟩
Proof state after:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ IsTotallyDisconnected univ
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ IsTotallyDisconnected univ
Tactic:
apply embedding_subtype_val.isTotallyDisconnected
Proof state after:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ IsTotallyDisconnected (Subtype.val '' univ)
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ IsTotallyDisconnected (Subtype.val '' univ)
Tactic:
rw [Subtype.coe_image_univ]
Proof state after:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ IsTotallyDisconnected s
Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype
Proof state before:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ IsTotallyDisconnected s
Tactic:
exact h
Proof state after:
no goals
Theorem: not_countable_Ioo
Proof state before:
a b : ℝ
h : a < b
⊢ ¬(Ioo a b).Countable
Tactic:
rw [← Cardinal.le_aleph0_iff_set_countable, not_le, Cardinal.mk_Ioo_real h]
Proof state after:
a b : ℝ
h : a < b
⊢ Cardinal.aleph0 < Cardinal.continuum
Theorem: not_countable_Ioo
Proof state before:
a b : ℝ
h : a < b
⊢ Cardinal.aleph0 < Cardinal.continuum
Tactic:
apply Cardinal.cantor
Proof state after:
no goals
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
⊢ TotallyDisconnectedSpace X
Tactic:
generalize hR : {r | ∃ x y : X, dist x y = r} = R
Proof state after:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
⊢ TotallyDisconnectedSpace X
Theorem: Countable.totallyDisconnectedSpace
Proof 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 _
Proof 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
Theorem: Countable.totallyDisconnectedSpace
Proof 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 ⟨?_⟩
Proof 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
Theorem: Countable.totallyDisconnectedSpace
Proof 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
Proof 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
Theorem: Countable.totallyDisconnectedSpace
Proof 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
Proof 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
Theorem: Countable.totallyDisconnectedSpace
Proof 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
Proof 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
Theorem: Countable.totallyDisconnectedSpace
Proof 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)
Proof 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
Theorem: Countable.totallyDisconnectedSpace
Proof 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
Proof 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
Theorem: Countable.totallyDisconnectedSpace
Proof 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⟩
Proof 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
Theorem: Countable.totallyDisconnectedSpace
Proof 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)]
Proof 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
Theorem: Countable.totallyDisconnectedSpace
Proof 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⟩, ?_⟩
Proof 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