Theorem: Ioi_union_Iio_mem_cocompact (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a : ℝ
ha : 0 ≤ a
⊢ Ioi a ∪ Iio (-a) ∈ cocompact ℝ
Tactic:
simp only [Filter.mem_cocompact]
State after:
a : ℝ
ha : 0 ≤ a
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ Ioi a ∪ Iio (-a)

State before:
a : ℝ
ha : 0 ≤ a
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ Ioi a ∪ Iio (-a)
Tactic:
use Icc (-a) a
State after:
case h
a : ℝ
ha : 0 ≤ a
⊢ IsCompact (Icc (-a) a) ∧ (Icc (-a) a)ᶜ ⊆ Ioi a ∪ Iio (-a)

State before:
case h
a : ℝ
ha : 0 ≤ a
⊢ IsCompact (Icc (-a) a) ∧ (Icc (-a) a)ᶜ ⊆ Ioi a ∪ Iio (-a)
Tactic:
constructor
State after:
case h.left
a : ℝ
ha : 0 ≤ a
⊢ IsCompact (Icc (-a) a)

case h.right
a : ℝ
ha : 0 ≤ a
⊢ (Icc (-a) a)ᶜ ⊆ Ioi a ∪ Iio (-a)

State before:
case h.left
a : ℝ
ha : 0 ≤ a
⊢ IsCompact (Icc (-a) a)
Tactic:
exact isCompact_Icc
State after:
no goals

State before:
case h.right
a : ℝ
ha : 0 ≤ a
⊢ (Icc (-a) a)ᶜ ⊆ Ioi a ∪ Iio (-a)
Tactic:
rw [@compl_subset_iff_union, ← union_assoc, Icc_union_Ioi_eq_Ici, union_comm, Iio_union_Ici]
State after:
case h.right
a : ℝ
ha : 0 ≤ a
⊢ -a ≤ a

State before:
case h.right
a : ℝ
ha : 0 ≤ a
⊢ -a ≤ a
Tactic:
linarith
State after:
no goals