Theorem: xpos_of_uIcc (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a b : ℕ
ha : a ∈ Ioo 0 b
x : ℝ
x_in : x ∈ [[↑a, ↑b]]
⊢ 0 < x
Tactic:
rw [uIcc_of_le (by exact_mod_cast ha.2.le), mem_Icc] at x_in
State after:
a b : ℕ
ha : a ∈ Ioo 0 b
x : ℝ
x_in : ↑a ≤ x ∧ x ≤ ↑b
⊢ 0 < x

State before:
a b : ℕ
ha : a ∈ Ioo 0 b
x : ℝ
x_in : ↑a ≤ x ∧ x ≤ ↑b
⊢ 0 < x
Tactic:
linarith [(by exact_mod_cast ha.1 : (0 : ℝ) < a)]
State after:
no goals

State before:
a b : ℕ
ha : a ∈ Ioo 0 b
x : ℝ
x_in : x ∈ [[↑a, ↑b]]
⊢ ↑a ≤ ↑b
Tactic:
exact_mod_cast ha.2.le
State after:
no goals

State before:
a b : ℕ
ha : a ∈ Ioo 0 b
x : ℝ
x_in : ↑a ≤ x ∧ x ≤ ↑b
⊢ 0 < ↑a
Tactic:
exact_mod_cast ha.1
State after:
no goals