Theorem: Aux.log_le_sum_inv (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
y : ℝ
hy : 1 ≤ y
⊢ y.log ≤ ∑ d ∈ Icc 1 ⌊y⌋₊, (↑d)⁻¹
Tactic:
calc _ ≤ Real.log ↑(Nat.floor y + 1) := ?_
     _ ≤ _ := ?_
State after:
case calc_1
y : ℝ
hy : 1 ≤ y
⊢ y.log ≤ (↑(⌊y⌋₊ + 1)).log

case calc_2
y : ℝ
hy : 1 ≤ y
⊢ (↑(⌊y⌋₊ + 1)).log ≤ ∑ d ∈ Icc 1 ⌊y⌋₊, (↑d)⁻¹

State before:
case calc_1
y : ℝ
hy : 1 ≤ y
⊢ y.log ≤ (↑(⌊y⌋₊ + 1)).log
Tactic:
gcongr
State after:
case calc_1.hxy
y : ℝ
hy : 1 ≤ y
⊢ y ≤ ↑(⌊y⌋₊ + 1)

State before:
case calc_1.hxy
y : ℝ
hy : 1 ≤ y
⊢ y ≤ ↑(⌊y⌋₊ + 1)
Tactic:
apply (le_ceil y).trans
State after:
case calc_1.hxy
y : ℝ
hy : 1 ≤ y
⊢ ↑⌈y⌉₊ ≤ ↑(⌊y⌋₊ + 1)

State before:
case calc_1.hxy
y : ℝ
hy : 1 ≤ y
⊢ ↑⌈y⌉₊ ≤ ↑(⌊y⌋₊ + 1)
Tactic:
norm_cast
State after:
case calc_1.hxy
y : ℝ
hy : 1 ≤ y
⊢ ⌈y⌉₊ ≤ ⌊y⌋₊ + 1

State before:
case calc_1.hxy
y : ℝ
hy : 1 ≤ y
⊢ ⌈y⌉₊ ≤ ⌊y⌋₊ + 1
Tactic:
exact ceil_le_floor_add_one y
State after:
no goals

State before:
case calc_2
y : ℝ
hy : 1 ≤ y
⊢ (↑(⌊y⌋₊ + 1)).log ≤ ∑ d ∈ Icc 1 ⌊y⌋₊, (↑d)⁻¹
Tactic:
apply log_add_one_le_sum_inv
State after:
no goals