Theorem: SelbergSieve.sum_mul_subst (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean)

State before:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0
Tactic:
by_cases hn: n = 0
State after:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : n = 0
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0

case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0

State before:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0
Tactic:
by_cases hkn : k ∣ n
State after:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0

case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0

State before:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0

case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0
Tactic:
swap
State after:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0

case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0

State before:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0
Tactic:
trans (∑ l in n.divisors, ∑ m in n.divisors, if l=k*m then f l else 0)
State after:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ ∑ l ∈ n.divisors, f l = ∑ l ∈ n.divisors, ∑ m ∈ n.divisors, if l = k * m then f l else 0

s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ (∑ l ∈ n.divisors, ∑ m ∈ n.divisors, if l = k * m then f l else 0) =
    ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0

State before:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : n = 0
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0
Tactic:
simp [hn]
State after:
no goals

State before:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
⊢ ∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0
Tactic:
rw [sum_eq_zero, sum_eq_zero]
State after:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
⊢ ∀ x ∈ n.divisors, (if k * x ∣ n then f (k * x) else 0) = 0

case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
⊢ ∀ x ∈ n.divisors, f x = 0

State before:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
⊢ ∀ x ∈ n.divisors, (if k * x ∣ n then f (k * x) else 0) = 0
Tactic:
rintro m _
State after:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
⊢ (if k * m ∣ n then f (k * m) else 0) = 0

State before:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
⊢ (if k * m ∣ n then f (k * m) else 0) = 0
Tactic:
rw [if_neg]
State after:
case neg.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
⊢ ¬k * m ∣ n

State before:
case neg.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
⊢ ¬k * m ∣ n
Tactic:
rintro h
State after:
case neg.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h✝ : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
h : k * m ∣ n
⊢ False

State before:
case neg.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h✝ : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
h : k * m ∣ n
⊢ False
Tactic:
apply hkn
State after:
case neg.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h✝ : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
h : k * m ∣ n
⊢ k ∣ n

State before:
case neg.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h✝ : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
h : k * m ∣ n
⊢ k ∣ n
Tactic:
exact (Nat.dvd_mul_right k m).trans h
State after:
no goals

State before:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
⊢ ∀ x ∈ n.divisors, f x = 0
Tactic:
intro l hl
State after:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ f l = 0

State before:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ f l = 0
Tactic:
apply h l (dvd_of_mem_divisors hl)
State after:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ ¬k ∣ l

State before:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ ¬k ∣ l
Tactic:
apply fun hkl => hkn <| hkl.trans (dvd_of_mem_divisors hl)
State after:
no goals

State before:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ ∑ l ∈ n.divisors, f l = ∑ l ∈ n.divisors, ∑ m ∈ n.divisors, if l = k * m then f l else 0
Tactic:
rw [sum_congr rfl]
State after:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ ∀ x ∈ n.divisors, f x = ∑ m ∈ n.divisors, if x = k * m then f x else 0

State before:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ ∀ x ∈ n.divisors, f x = ∑ m ∈ n.divisors, if x = k * m then f x else 0
Tactic:
intro l hl
State after:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ f l = ∑ m ∈ n.divisors, if l = k * m then f l else 0

State before:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ f l = ∑ m ∈ n.divisors, if l = k * m then f l else 0
Tactic:
by_cases hkl : k ∣ l
State after:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ f l = ∑ m ∈ n.divisors, if l = k * m then f l else 0

case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : ¬k ∣ l
⊢ f l = ∑ m ∈ n.divisors, if l = k * m then f l else 0

State before:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ f l = ∑ m ∈ n.divisors, if l = k * m then f l else 0

case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : ¬k ∣ l
⊢ f l = ∑ m ∈ n.divisors, if l = k * m then f l else 0
Tactic:
swap
State after:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : ¬k ∣ l
⊢ f l = ∑ m ∈ n.divisors, if l = k * m then f l else 0

case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ f l = ∑ m ∈ n.divisors, if l = k * m then f l else 0

State before:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ f l = ∑ m ∈ n.divisors, if l = k * m then f l else 0
Tactic:
rw [sum_eq_single (l/k)]
State after:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ f l = if l = k * (l / k) then f l else 0

case pos.h₀
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ ∀ b ∈ n.divisors, b ≠ l / k → (if l = k * b then f l else 0) = 0

case pos.h₁
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ l / k ∉ n.divisors → (if l = k * (l / k) then f l else 0) = 0

State before:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : ¬k ∣ l
⊢ f l = ∑ m ∈ n.divisors, if l = k * m then f l else 0
Tactic:
rw [h l (dvd_of_mem_divisors hl) hkl, sum_eq_zero]
State after:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : ¬k ∣ l
⊢ ∀ x ∈ n.divisors, (if l = k * x then 0 else 0) = 0

State before:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : ¬k ∣ l
⊢ ∀ x ∈ n.divisors, (if l = k * x then 0 else 0) = 0
Tactic:
intro m _
State after:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : ¬k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
⊢ (if l = k * m then 0 else 0) = 0

State before:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : ¬k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
⊢ (if l = k * m then 0 else 0) = 0
Tactic:
rw [ite_id]
State after:
no goals

State before:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ f l = if l = k * (l / k) then f l else 0
Tactic:
rw[if_pos]
State after:
case pos.hc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ l = k * (l / k)

State before:
case pos.hc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ l = k * (l / k)
Tactic:
rw [Nat.mul_div_cancel' hkl]
State after:
no goals

State before:
case pos.h₀
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ ∀ b ∈ n.divisors, b ≠ l / k → (if l = k * b then f l else 0) = 0
Tactic:
intro m _ hmlk
State after:
case pos.h₀
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
hmlk : m ≠ l / k
⊢ (if l = k * m then f l else 0) = 0

State before:
case pos.h₀
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
hmlk : m ≠ l / k
⊢ (if l = k * m then f l else 0) = 0
Tactic:
apply if_neg
State after:
case pos.h₀.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
hmlk : m ≠ l / k
⊢ ¬l = k * m

State before:
case pos.h₀.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
hmlk : m ≠ l / k
⊢ ¬l = k * m
Tactic:
revert hmlk
State after:
case pos.h₀.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
⊢ m ≠ l / k → ¬l = k * m

State before:
case pos.h₀.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
⊢ m ≠ l / k → ¬l = k * m
Tactic:
contrapose!
State after:
case pos.h₀.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
⊢ l = k * m → m = l / k

State before:
case pos.h₀.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
⊢ l = k * m → m = l / k
Tactic:
intro hlkm
State after:
case pos.h₀.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
hlkm : l = k * m
⊢ m = l / k

State before:
case pos.h₀.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
hlkm : l = k * m
⊢ m = l / k
Tactic:
rw [hlkm, mul_comm, Nat.mul_div_cancel]
State after:
case pos.h₀.hnc.H
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
hlkm : l = k * m
⊢ 0 < k

State before:
case pos.h₀.hnc.H
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
m : ℕ
a✝ : m ∈ n.divisors
hlkm : l = k * m
⊢ 0 < k
Tactic:
apply Nat.pos_of_dvd_of_pos hkn (Nat.pos_of_ne_zero hn)
State after:
no goals

State before:
case pos.h₁
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ l / k ∉ n.divisors → (if l = k * (l / k) then f l else 0) = 0
Tactic:
contrapose!
State after:
case pos.h₁
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ (if l = k * (l / k) then f l else 0) ≠ 0 → l / k ∈ n.divisors

State before:
case pos.h₁
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ (if l = k * (l / k) then f l else 0) ≠ 0 → l / k ∈ n.divisors
Tactic:
intro _
State after:
case pos.h₁
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
a✝ : (if l = k * (l / k) then f l else 0) ≠ 0
⊢ l / k ∈ n.divisors

State before:
case pos.h₁
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
a✝ : (if l = k * (l / k) then f l else 0) ≠ 0
⊢ l / k ∈ n.divisors
Tactic:
rw [mem_divisors]
State after:
case pos.h₁
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
a✝ : (if l = k * (l / k) then f l else 0) ≠ 0
⊢ l / k ∣ n ∧ n ≠ 0

State before:
case pos.h₁
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
a✝ : (if l = k * (l / k) then f l else 0) ≠ 0
⊢ l / k ∣ n ∧ n ≠ 0
Tactic:
exact ⟨Trans.trans (Nat.div_dvd_of_dvd hkl) (dvd_of_mem_divisors hl), hn⟩
State after:
no goals

State before:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ (∑ l ∈ n.divisors, ∑ m ∈ n.divisors, if l = k * m then f l else 0) =
    ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0
Tactic:
rw [sum_comm, sum_congr rfl]
State after:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ ∀ x ∈ n.divisors, (∑ x_1 ∈ n.divisors, if x_1 = k * x then f x_1 else 0) = if k * x ∣ n then f (k * x) else 0

State before:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ ∀ x ∈ n.divisors, (∑ x_1 ∈ n.divisors, if x_1 = k * x then f x_1 else 0) = if k * x ∣ n then f (k * x) else 0
Tactic:
intro m _
State after:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
⊢ (∑ x ∈ n.divisors, if x = k * m then f x else 0) = if k * m ∣ n then f (k * m) else 0

State before:
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
⊢ (∑ x ∈ n.divisors, if x = k * m then f x else 0) = if k * m ∣ n then f (k * m) else 0
Tactic:
split_ifs with hdvd
State after:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : k * m ∣ n
⊢ (∑ x ∈ n.divisors, if x = k * m then f x else 0) = f (k * m)

case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
⊢ (∑ x ∈ n.divisors, if x = k * m then f x else 0) = 0

State before:
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : k * m ∣ n
⊢ (∑ x ∈ n.divisors, if x = k * m then f x else 0) = f (k * m)
Tactic:
rw [←Aux.sum_intro]
State after:
case pos.hd
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : k * m ∣ n
⊢ k * m ∈ n.divisors

State before:
case pos.hd
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : k * m ∣ n
⊢ k * m ∈ n.divisors
Tactic:
simp only [mem_divisors, hdvd, ne_eq, hn, not_false_eq_true, and_self]
State after:
no goals

State before:
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
⊢ (∑ x ∈ n.divisors, if x = k * m then f x else 0) = 0
Tactic:
apply sum_eq_zero
State after:
case neg.h
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
⊢ ∀ x ∈ n.divisors, (if x = k * m then f x else 0) = 0

State before:
case neg.h
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
⊢ ∀ x ∈ n.divisors, (if x = k * m then f x else 0) = 0
Tactic:
intro l hl
State after:
case neg.h
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ (if l = k * m then f l else 0) = 0

State before:
case neg.h
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ (if l = k * m then f l else 0) = 0
Tactic:
apply if_neg
State after:
case neg.h.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ ¬l = k * m

State before:
case neg.h.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ ¬l = k * m
Tactic:
rintro rfl
State after:
case neg.h.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
hl : k * m ∈ n.divisors
⊢ False

State before:
case neg.h.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
hl : k * m ∈ n.divisors
⊢ False
Tactic:
simp only [mem_divisors, ne_eq] at hl
State after:
case neg.h.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
hl : k * m ∣ n ∧ ¬n = 0
⊢ False

State before:
case neg.h.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
hl : k * m ∣ n ∧ ¬n = 0
⊢ False
Tactic:
exact hdvd hl.1
State after:
no goals