Theorem: finsum_range_eq_sum_range' (PrimeNumberTheoremAnd/Consequences.lean)

State before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
⊢ ∑ᶠ (n : ℕ) (_ : ↑n ≤ x), f n = ∑ n ∈ Iic ⌊x⌋₊, f n
Tactic:
apply finsum_cond_eq_sum_of_cond_iff f
State after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
⊢ ∀ {x_1 : ℕ}, f x_1 ≠ 0 → (↑x_1 ≤ x ↔ x_1 ∈ Iic ⌊x⌋₊)

State before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
⊢ ∀ {x_1 : ℕ}, f x_1 ≠ 0 → (↑x_1 ≤ x ↔ x_1 ∈ Iic ⌊x⌋₊)
Tactic:
intro n h
State after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
n : ℕ
h : f n ≠ 0
⊢ ↑n ≤ x ↔ n ∈ Iic ⌊x⌋₊

State before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
n : ℕ
h : f n ≠ 0
⊢ ↑n ≤ x ↔ n ∈ Iic ⌊x⌋₊
Tactic:
simp only [mem_Iic]
State after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
n : ℕ
h : f n ≠ 0
⊢ ↑n ≤ x ↔ n ≤ ⌊x⌋₊

State before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
n : ℕ
h : f n ≠ 0
⊢ ↑n ≤ x ↔ n ≤ ⌊x⌋₊
Tactic:
exact Iff.symm <| Nat.le_floor_iff'
  fun (hc : n = 0) ↦ (h : f n ≠ 0) <| (congrArg f hc).trans ArithmeticFunction.map_zero
State after:
no goals