⊢ 0.3678794412⁻¹ < exp 1


⊢ 0 < 0.3678794412
⊢ exp (-1) < 0.3678794412
rw [exp_neg, inv_lt (exp_pos _)]
⊢ 0.3678794412⁻¹ < 2244083 / 825552 - 1 / 10 ^ 10


⊢ 0 < 0.3678794412
⊢ 0.3678794412⁻¹ < exp 1


⊢ 0 < 0.3678794412
refine' lt_of_lt_of_le _ (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2)
no goals
⊢ 0.3678794412⁻¹ < 2244083 / 825552 - 1 / 10 ^ 10


⊢ 0 < 0.3678794412
all_goals norm_num
no goals
⊢ 0 < 0.3678794412
norm_num