Theorem: lt_abs_mem_cocompact (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a : ℝ
ha : 0 ≤ a
⊢ {t | a < |t|} ∈ cocompact ℝ
Tactic:
convert Ioi_union_Iio_mem_cocompact ha using 1
State after:
case h.e'_4
a : ℝ
ha : 0 ≤ a
⊢ {t | a < |t|} = Ioi a ∪ Iio (-a)

State before:
case h.e'_4
a : ℝ
ha : 0 ≤ a
⊢ {t | a < |t|} = Ioi a ∪ Iio (-a)
Tactic:
ext t
State after:
case h.e'_4.h
a : ℝ
ha : 0 ≤ a
t : ℝ
⊢ t ∈ {t | a < |t|} ↔ t ∈ Ioi a ∪ Iio (-a)

State before:
case h.e'_4.h
a : ℝ
ha : 0 ≤ a
t : ℝ
⊢ t ∈ {t | a < |t|} ↔ t ∈ Ioi a ∪ Iio (-a)
Tactic:
simp only [mem_setOf_eq, mem_union, mem_Ioi, mem_Iio, lt_abs, lt_neg]
State after:
no goals