internlm/Lean-Github huggingface dataset:
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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)
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof state after:
no goals
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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 _
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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)
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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)
Proof state after:
no goals
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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)]
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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 _
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof state after:
no goals
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof 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)
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof state after:
no goals
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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!
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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)
Proof state after:
no goals
Theorem: SelbergSieve.sum_mul_subst
Proof 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!
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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 _
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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⟩
Proof state after:
no goals
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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 _
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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]
Proof state after:
no goals
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof 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
Theorem: SelbergSieve.sum_mul_subst
Proof 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
Proof state after:
no goals
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof state before:
s : SelbergSieve
d : ℕ
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
by_cases h_dvd : d ∣ P
Proof state after:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0

case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof state before:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0

case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
swap
Proof state after:
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0

case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Theorem: SelbergSieve.selbergWeights_eq_dvds_sum
Proof state before:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ ν d * s.selbergWeights d = S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0
Tactic:
dsimp only [selbergWeights]
Proof state after:
case pos
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
⊢ (ν d *
      if d ∣ P then (ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
      else 0) =
    S⁻¹ * ↑(μ d) * ∑ l ∈ P.divisors, if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0