Theorem: one_lt_re_of_pos (EulerProducts/PNT.lean)

State before:
x y : ℝ
hx : 0 < x
⊢ 1 < (1 + ↑x).re ∧ 1 < (1 + ↑x + I * ↑y).re ∧ 1 < (1 + ↑x + 2 * I * ↑y).re
Tactic:
simp only [add_re, one_re, ofReal_re, lt_add_iff_pos_right, hx, mul_re, I_re, zero_mul, I_im,
  ofReal_im, mul_zero, sub_self, add_zero, re_ofNat, im_ofNat, mul_one, mul_im, and_self]
State after:
no goals