Theorem: atInf_eq_cocompact (Ray/Misc/AtInf.lean)

State before:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
⊢ atInf = Filter.cocompact X
Tactic:
apply le_antisymm atInf_le_cocompact
State after:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
⊢ Filter.cocompact X ≤ atInf

State before:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
⊢ Filter.cocompact X ≤ atInf
Tactic:
rw [Filter.le_def]
State after:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
⊢ ∀ x ∈ atInf, x ∈ Filter.cocompact X

State before:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
⊢ ∀ x ∈ atInf, x ∈ Filter.cocompact X
Tactic:
intro s m
State after:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
⊢ s ∈ Filter.cocompact X

State before:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
⊢ s ∈ Filter.cocompact X
Tactic:
rcases mem_atInf_iff.mp m with ⟨r, h⟩
State after:
case intro
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ s ∈ Filter.cocompact X

State before:
case intro
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ s ∈ Filter.cocompact X
Tactic:
rw [Filter.mem_cocompact]
State after:
case intro
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

State before:
case intro
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s
Tactic:
use closedBall 0 r, isCompact_closedBall _ _
State after:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ (closedBall 0 r)ᶜ ⊆ s

State before:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ (closedBall 0 r)ᶜ ⊆ s
Tactic:
refine _root_.trans ?_ h
State after:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ (closedBall 0 r)ᶜ ⊆ {x | ‖x‖ > r}

State before:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ (closedBall 0 r)ᶜ ⊆ {x | ‖x‖ > r}
Tactic:
intro x xs
State after:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
x : X
xs : x ∈ (closedBall 0 r)ᶜ
⊢ x ∈ {x | ‖x‖ > r}

State before:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
x : X
xs : x ∈ (closedBall 0 r)ᶜ
⊢ x ∈ {x | ‖x‖ > r}
Tactic:
simp only [mem_compl_iff, mem_closedBall_zero_iff, not_le] at xs
State after:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
x : X
xs : r < ‖x‖
⊢ x ∈ {x | ‖x‖ > r}

State before:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
x : X
xs : r < ‖x‖
⊢ x ∈ {x | ‖x‖ > r}
Tactic:
exact xs
State after:
no goals