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

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

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

State before:
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
⊢ s ∈ atInf
Tactic:
rcases Filter.mem_cocompact.mp m with ⟨t, tc, ts⟩
State after:
case intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
⊢ s ∈ atInf

State before:
case intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
⊢ s ∈ atInf
Tactic:
rcases tc.bddAbove_image continuousOn_id.norm with ⟨r, rh⟩
State after:
case intro.intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : r ∈ upperBounds ((fun x => ‖id x‖) '' t)
⊢ s ∈ atInf

State before:
case intro.intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : r ∈ upperBounds ((fun x => ‖id x‖) '' t)
⊢ s ∈ atInf
Tactic:
simp only [id_eq, mem_upperBounds, mem_image, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂] at rh
State after:
case intro.intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
⊢ s ∈ atInf

State before:
case intro.intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
⊢ s ∈ atInf
Tactic:
rw [mem_atInf_iff]
State after:
case intro.intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
⊢ ∃ r, {x | ‖x‖ > r} ⊆ s

State before:
case intro.intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
⊢ ∃ r, {x | ‖x‖ > r} ⊆ s
Tactic:
use r
State after:
case h
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
⊢ {x | ‖x‖ > r} ⊆ s

State before:
case h
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
⊢ {x | ‖x‖ > r} ⊆ s
Tactic:
intro x m
State after:
case h
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ {x | ‖x‖ > r}
⊢ x ∈ s

State before:
case h
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ {x | ‖x‖ > r}
⊢ x ∈ s
Tactic:
apply ts
State after:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ {x | ‖x‖ > r}
⊢ x ∈ tᶜ

State before:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ {x | ‖x‖ > r}
⊢ x ∈ tᶜ
Tactic:
contrapose m
State after:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∉ tᶜ
⊢ x ∉ {x | ‖x‖ > r}

State before:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∉ tᶜ
⊢ x ∉ {x | ‖x‖ > r}
Tactic:
simp only [mem_compl_iff, not_not_mem] at m
State after:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ t
⊢ x ∉ {x | ‖x‖ > r}

State before:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ t
⊢ x ∉ {x | ‖x‖ > r}
Tactic:
simp only [mem_setOf_eq, not_lt]
State after:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ t
⊢ ‖x‖ ≤ r

State before:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ t
⊢ ‖x‖ ≤ r
Tactic:
exact rh _ m
State after:
no goals