Theorem: ZetaInvBnd_aux' (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
t : ℝ
logt_gt_one : 1 < |t|.log
⊢ |t|.log < |t|.log ^ 9
Tactic:
nth_rewrite 1 [← Real.rpow_one <| Real.log |t|]
State after:
t : ℝ
logt_gt_one : 1 < |t|.log
⊢ |t|.log ^ 1 < |t|.log ^ 9

State before:
t : ℝ
logt_gt_one : 1 < |t|.log
⊢ |t|.log ^ 1 < |t|.log ^ 9
Tactic:
exact mod_cast Real.rpow_lt_rpow_left_iff (y := 1) (z := 9) logt_gt_one |>.mpr (by norm_num)
State after:
no goals

State before:
t : ℝ
logt_gt_one : 1 < |t|.log
⊢ 1 < 9
Tactic:
norm_num
State after:
no goals