[GOAL]
p q : ℚ
s t : Set ℚ
⊢ NeBot (cocompact ℚ ⊓ 𝓝 p)
[PROOFSTEP]
refine' (hasBasis_cocompact.inf (nhds_basis_opens _)).neBot_iff.2 _
[GOAL]
p q : ℚ
s t : Set ℚ
⊢ ∀ {i : Set ℚ × Set ℚ}, IsCompact i.fst ∧ p ∈ i.snd ∧ IsOpen i.snd → Set.Nonempty (i.fstᶜ ∩ i.snd)
[PROOFSTEP]
rintro ⟨s, o⟩ ⟨hs, hpo, ho⟩
[GOAL]
case mk.intro.intro
p q : ℚ
s✝ t s o : Set ℚ
hs : IsCompact (s, o).fst
hpo : p ∈ (s, o).snd
ho : IsOpen (s, o).snd
⊢ Set.Nonempty ((s, o).fstᶜ ∩ (s, o).snd)
[PROOFSTEP]
rw [inter_comm]
[GOAL]
case mk.intro.intro
p q : ℚ
s✝ t s o : Set ℚ
hs : IsCompact (s, o).fst
hpo : p ∈ (s, o).snd
ho : IsOpen (s, o).snd
⊢ Set.Nonempty ((s, o).snd ∩ (s, o).fstᶜ)
[PROOFSTEP]
exact (dense_compl_compact hs).inter_open_nonempty _ ho ⟨p, hpo⟩
[GOAL]
p q : ℚ
s t : Set ℚ
⊢ ¬IsCountablyGenerated (cocompact ℚ)
[PROOFSTEP]
intro H
[GOAL]
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
⊢ False
[PROOFSTEP]
rcases exists_seq_tendsto (cocompact ℚ ⊓ 𝓝 0) with ⟨x, hx⟩
[GOAL]
case intro
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ ⊓ 𝓝 0)
⊢ False
[PROOFSTEP]
rw [tendsto_inf] at hx 
[GOAL]
case intro
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
⊢ False
[PROOFSTEP]
rcases hx with ⟨hxc, hx0⟩
[GOAL]
case intro.intro
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
⊢ False
[PROOFSTEP]
obtain ⟨n, hn⟩ : ∃ n : ℕ, x n ∉ insert (0 : ℚ) (range x)
[GOAL]
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
⊢ ∃ n, ¬x n ∈ insert 0 (range x)
case intro.intro.intro
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
n : ℕ
hn : ¬x n ∈ insert 0 (range x)
⊢ False
[PROOFSTEP]
exact (hxc.eventually hx0.isCompact_insert_range.compl_mem_cocompact).exists
[GOAL]
case intro.intro.intro
p q : ℚ
s t : Set ℚ
H : IsCountablyGenerated (cocompact ℚ)
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
n : ℕ
hn : ¬x n ∈ insert 0 (range x)
⊢ False
[PROOFSTEP]
exact hn (Or.inr ⟨n, rfl⟩)
[GOAL]
p q : ℚ
s t : Set ℚ
⊢ ¬IsCountablyGenerated (𝓝 ∞)
[PROOFSTEP]
intro
[GOAL]
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
⊢ False
[PROOFSTEP]
have : IsCountablyGenerated (comap (OnePoint.some : ℚ → ℚ∞) (𝓝 ∞)) := by infer_instance
[GOAL]
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
⊢ IsCountablyGenerated (comap OnePoint.some (𝓝 ∞))
[PROOFSTEP]
infer_instance
[GOAL]
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
this : IsCountablyGenerated (comap OnePoint.some (𝓝 ∞))
⊢ False
[PROOFSTEP]
rw [OnePoint.comap_coe_nhds_infty, coclosedCompact_eq_cocompact] at this 
[GOAL]
p q : ℚ
s t : Set ℚ
a✝ : IsCountablyGenerated (𝓝 ∞)
this : IsCountablyGenerated (cocompact ℚ)
⊢ False
[PROOFSTEP]
exact not_countably_generated_cocompact this
[GOAL]
p q : ℚ
s t : Set ℚ
⊢ ¬FirstCountableTopology ℚ∞
[PROOFSTEP]
intro
[GOAL]
p q : ℚ
s t : Set ℚ
a✝ : FirstCountableTopology ℚ∞
⊢ False
[PROOFSTEP]
exact not_countably_generated_nhds_infty_opc inferInstance
[GOAL]
p q : ℚ
s t : Set ℚ
⊢ ¬SecondCountableTopology ℚ∞
[PROOFSTEP]
intro
[GOAL]
p q : ℚ
s t : Set ℚ
a✝ : SecondCountableTopology ℚ∞
⊢ False
[PROOFSTEP]
exact not_firstCountableTopology_opc inferInstance
[GOAL]
p q : ℚ
s t : Set ℚ
⊢ TotallyDisconnectedSpace ℚ
[PROOFSTEP]
refine' ⟨fun s hsu hs x hx y hy => _⟩
[GOAL]
p q : ℚ
s✝ t s : Set ℚ
hsu : s ⊆ univ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
⊢ x = y
[PROOFSTEP]
clear hsu
[GOAL]
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
⊢ x = y
[PROOFSTEP]
by_contra' H : x ≠ y
[GOAL]
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
⊢ False
[PROOFSTEP]
wlog hlt : x < y
[GOAL]
case inr
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this :
  ∀ {p q : ℚ} {s t : Set ℚ} (s : Set ℚ), IsPreconnected s → ∀ (x : ℚ), x ∈ s → ∀ (y : ℚ), y ∈ s → x ≠ y → x < y → False
hlt : ¬x < y
⊢ False
[PROOFSTEP]
refine' this s hs y hy x hx H.symm <| H.lt_or_lt.resolve_left hlt
[GOAL]
case inr.refine'_1
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this :
  ∀ {p q : ℚ} {s t : Set ℚ} (s : Set ℚ), IsPreconnected s → ∀ (x : ℚ), x ∈ s → ∀ (y : ℚ), y ∈ s → x ≠ y → x < y → False
hlt : ¬x < y
⊢ ℚ
[PROOFSTEP]
assumption
[GOAL]
case inr.refine'_2
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this :
  ∀ {p q : ℚ} {s t : Set ℚ} (s : Set ℚ), IsPreconnected s → ∀ (x : ℚ), x ∈ s → ∀ (y : ℚ), y ∈ s → x ≠ y → x < y → False
hlt : ¬x < y
⊢ ℚ
[PROOFSTEP]
assumption
[GOAL]
case inr.refine'_3
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this :
  ∀ {p q : ℚ} {s t : Set ℚ} (s : Set ℚ), IsPreconnected s → ∀ (x : ℚ), x ∈ s → ∀ (y : ℚ), y ∈ s → x ≠ y → x < y → False
hlt : ¬x < y
⊢ Set ℚ
[PROOFSTEP]
assumption
[GOAL]
case inr.refine'_4
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this :
  ∀ {p q : ℚ} {s t : Set ℚ} (s : Set ℚ), IsPreconnected s → ∀ (x : ℚ), x ∈ s → ∀ (y : ℚ), y ∈ s → x ≠ y → x < y → False
hlt : ¬x < y
⊢ Set ℚ
[PROOFSTEP]
assumption
[GOAL]
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
⊢ False
[PROOFSTEP]
rcases exists_irrational_btwn (Rat.cast_lt.2 hlt) with ⟨z, hz, hxz, hzy⟩
[GOAL]
case intro.intro.intro
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : ↑x < z
hzy : z < ↑y
⊢ False
[PROOFSTEP]
have := hs.image _ continuous_coe_real.continuousOn
[GOAL]
case intro.intro.intro
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : ↑x < z
hzy : z < ↑y
this : IsPreconnected (Rat.cast '' s)
⊢ False
[PROOFSTEP]
rw [isPreconnected_iff_ordConnected] at this 
[GOAL]
case intro.intro.intro
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : ↑x < z
hzy : z < ↑y
this✝ : IsPreconnected (Rat.cast '' s)
this : OrdConnected (Rat.cast '' s)
⊢ False
[PROOFSTEP]
have : z ∈ Rat.cast '' s := this.out (mem_image_of_mem _ hx) (mem_image_of_mem _ hy) ⟨hxz.le, hzy.le⟩
[GOAL]
case intro.intro.intro
p q : ℚ
s✝ t s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : ↑x < z
hzy : z < ↑y
this✝¹ : IsPreconnected (Rat.cast '' s)
this✝ : OrdConnected (Rat.cast '' s)
this : z ∈ Rat.cast '' s
⊢ False
[PROOFSTEP]
exact hz (image_subset_range _ _ this)
