Theorem: ArithmeticFunction.sum_range_mul_zeta (PrimeNumberTheoremAnd/Mathlib/NumberTheory/ArithmeticFunction.lean)

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ d ∈ filter (fun d => d.2 ∈ d.1.divisors) (range (N + 1) ×ˢ range (N + 1)), f d.2
Tactic:
simp_rw [sum_filter, sum_product]
State after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ x ∈ range (N + 1), ∑ x_1 ∈ range (N + 1), if x_1 ∈ x.divisors then f x_1 else 0

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ x ∈ range (N + 1), ∑ x_1 ∈ range (N + 1), if x_1 ∈ x.divisors then f x_1 else 0
Tactic:
apply sum_congr rfl (fun x hx ↦ ?_)
State after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
⊢ (f * ↑ζ) x = ∑ x_1 ∈ range (N + 1), if x_1 ∈ x.divisors then f x_1 else 0

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
⊢ (f * ↑ζ) x = ∑ x_1 ∈ range (N + 1), if x_1 ∈ x.divisors then f x_1 else 0
Tactic:
rw [← sum_filter, sum_congr (s₂ := divisors x) ?_ fun _ _ ↦ rfl, coe_mul_zeta_apply]
State after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
⊢ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1)) = x.divisors

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
⊢ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1)) = x.divisors
Tactic:
refine Subset.antisymm ?_ ?_ <;> intro d hd
State after:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))
⊢ d ∈ x.divisors

case refine_2
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
⊢ d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))

State before:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))
⊢ d ∈ x.divisors
Tactic:
exact (mem_filter.mp hd).right
State after:
no goals

State before:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
⊢ d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))
Tactic:
have h : d ≤ x := by
  rw [divisors, mem_filter] at hd
  exact lt_succ.mp (mem_Ico.mp hd.left).right
State after:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
h : d ≤ x
⊢ d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))

State before:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
h : d ≤ x
⊢ d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))
Tactic:
exact mem_filter.mpr ⟨mem_range.mpr (lt_of_le_of_lt h $ mem_range.mp hx), hd⟩
State after:
no goals

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
⊢ d ≤ x
Tactic:
rw [divisors, mem_filter] at hd
State after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ Ico 1 (x + 1) ∧ d ∣ x
⊢ d ≤ x

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ Ico 1 (x + 1) ∧ d ∣ x
⊢ d ≤ x
Tactic:
exact lt_succ.mp (mem_Ico.mp hd.left).right
State after:
no goals

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ filter (fun d => d.2 ∈ d.1.divisors) (range (N + 1) ×ˢ range (N + 1)), f d.2 =
    ∑ d ∈ range (N + 1), ∑ _m ∈ filter (fun x => d ∈ x.divisors) (range (N + 1)), f d
Tactic:
rw [sum_filter, sum_product_right]
State after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ (∑ y ∈ range (N + 1), ∑ x ∈ range (N + 1), if (x, y).2 ∈ (x, y).1.divisors then f (x, y).2 else 0) =
    ∑ d ∈ range (N + 1), ∑ _m ∈ filter (fun x => d ∈ x.divisors) (range (N + 1)), f d

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ (∑ y ∈ range (N + 1), ∑ x ∈ range (N + 1), if (x, y).2 ∈ (x, y).1.divisors then f (x, y).2 else 0) =
    ∑ d ∈ range (N + 1), ∑ _m ∈ filter (fun x => d ∈ x.divisors) (range (N + 1)), f d
Tactic:
refine sum_congr rfl (fun y _ ↦ by simp only [← sum_filter])
State after:
no goals

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (∑ x ∈ range (N + 1), if (x, y).2 ∈ (x, y).1.divisors then f (x, y).2 else 0) =
    ∑ _m ∈ filter (fun x => y ∈ x.divisors) (range (N + 1)), f y
Tactic:
simp only [← sum_filter]
State after:
no goals

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ range (N + 1), ∑ _m ∈ filter (fun x => d ∈ x.divisors) (range (N + 1)), f d = ∑ d ∈ range (N + 1), (N / d) • f d
Tactic:
rw [sum_congr rfl fun y _ ↦ ?_]
State after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ ∑ _m ∈ filter (fun x => y ∈ x.divisors) (range (N + 1)), f y = (N / y) • f y

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ ∑ _m ∈ filter (fun x => y ∈ x.divisors) (range (N + 1)), f y = (N / y) • f y
Tactic:
rw [sum_const]
State after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (filter (fun x => y ∈ x.divisors) (range (N + 1))).card • f y = (N / y) • f y

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (filter (fun x => y ∈ x.divisors) (range (N + 1))).card • f y = (N / y) • f y
Tactic:
congr
State after:
case e_a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (filter (fun x => y ∈ x.divisors) (range (N + 1))).card = N / y

State before:
case e_a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (filter (fun x => y ∈ x.divisors) (range (N + 1))).card = N / y
Tactic:
simp_rw [mem_divisors, and_comm (b := _ ≠ 0), ← filter_filter]
State after:
case e_a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (filter (fun a => y ∣ a) (filter (fun a => a ≠ 0) (range (N + 1)))).card = N / y

State before:
case e_a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
this : filter (fun x => x ≠ 0) (range (N + 1)) = Ioc 0 N
⊢ (filter (fun a => y ∣ a) (filter (fun a => a ≠ 0) (range (N + 1)))).card = N / y
Tactic:
rw [this, Nat.Ioc_filter_dvd_card_eq_div]
State after:
no goals

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ filter (fun x => x ≠ 0) (range (N + 1)) = Ioc 0 N
Tactic:
ext a
State after:
case a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
a : ℕ
⊢ a ∈ filter (fun x => x ≠ 0) (range (N + 1)) ↔ a ∈ Ioc 0 N

State before:
case a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
a : ℕ
⊢ a ∈ filter (fun x => x ≠ 0) (range (N + 1)) ↔ a ∈ Ioc 0 N
Tactic:
rw [mem_filter, mem_Ioc, mem_range, pos_iff_ne_zero, lt_succ, and_comm]
State after:
no goals