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

State before:
y : ℝ
hy : 1 ≤ y
⊢ ∑ d ∈ Icc 1 ⌊y⌋₊, (↑d)⁻¹ ≤ 1 + y.log
Tactic:
trans (1 + Real.log (⌊y⌋₊))
State after:
y : ℝ
hy : 1 ≤ y
⊢ ∑ d ∈ Icc 1 ⌊y⌋₊, (↑d)⁻¹ ≤ 1 + (↑⌊y⌋₊).log

y : ℝ
hy : 1 ≤ y
⊢ 1 + (↑⌊y⌋₊).log ≤ 1 + y.log

State before:
y : ℝ
hy : 1 ≤ y
⊢ 1 + (↑⌊y⌋₊).log ≤ 1 + y.log
Tactic:
gcongr
State after:
case bc.hx
y : ℝ
hy : 1 ≤ y
⊢ 0 < ↑⌊y⌋₊

case bc.hxy
y : ℝ
hy : 1 ≤ y
⊢ ↑⌊y⌋₊ ≤ y

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

State before:
y : ℝ
hy : 1 ≤ y
⊢ 1 ≤ ⌊y⌋₊
Tactic:
apply le_floor
State after:
case h
y : ℝ
hy : 1 ≤ y
⊢ ↑1 ≤ y

State before:
case h
y : ℝ
hy : 1 ≤ y
⊢ ↑1 ≤ y
Tactic:
norm_cast
State after:
no goals

State before:
case bc.hx
y : ℝ
hy : 1 ≤ y
⊢ 0 < ↑⌊y⌋₊
Tactic:
norm_cast
State after:
case bc.hx
y : ℝ
hy : 1 ≤ y
⊢ 0 < ⌊y⌋₊

State before:
case bc.hx
y : ℝ
hy : 1 ≤ y
⊢ 0 < ⌊y⌋₊
Tactic:
apply Nat.lt_of_succ_le
State after:
case bc.hx.h
y : ℝ
hy : 1 ≤ y
⊢ succ 0 ≤ ⌊y⌋₊

State before:
case bc.hx.h
y : ℝ
hy : 1 ≤ y
⊢ succ 0 ≤ ⌊y⌋₊
Tactic:
apply le_floor
State after:
case bc.hx.h.h
y : ℝ
hy : 1 ≤ y
⊢ ↑(succ 0) ≤ y

State before:
case bc.hx.h.h
y : ℝ
hy : 1 ≤ y
⊢ ↑(succ 0) ≤ y
Tactic:
norm_cast
State after:
no goals

State before:
case bc.hxy
y : ℝ
hy : 1 ≤ y
⊢ ↑⌊y⌋₊ ≤ y
Tactic:
apply floor_le
State after:
case bc.hxy.ha
y : ℝ
hy : 1 ≤ y
⊢ 0 ≤ y

State before:
case bc.hxy.ha
y : ℝ
hy : 1 ≤ y
⊢ 0 ≤ y
Tactic:
linarith
State after:
no goals