internlm/Lean-Github huggingface dataset:
Theorem: Aux.conv_lambda_sq_larger_sum
Proof state before:
f : ℕ → ℕ → ℕ → ℝ
n : ℕ
⊢ (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d ∈ n.divisors, ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Tactic:
apply sum_congr rfl
Proof state after:
f : ℕ → ℕ → ℕ → ℝ
n : ℕ
⊢ ∀ x ∈ n.divisors,
    (∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then f d1 d2 x else 0) =
      ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = d1.lcm d2 then f d1 d2 x else 0
Theorem: Aux.conv_lambda_sq_larger_sum
Proof state before:
f : ℕ → ℕ → ℕ → ℝ
n : ℕ
⊢ ∀ x ∈ n.divisors,
    (∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then f d1 d2 x else 0) =
      ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = d1.lcm d2 then f d1 d2 x else 0
Tactic:
intro d hd
Proof state after:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∈ n.divisors
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Theorem: Aux.conv_lambda_sq_larger_sum
Proof state before:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∈ n.divisors
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Tactic:
rw [mem_divisors] at hd
Proof state after:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Theorem: Aux.conv_lambda_sq_larger_sum
Proof state before:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Tactic:
simp_rw [←Nat.divisors_filter_dvd_of_dvd hd.2 hd.1, sum_filter, ←ite_and, ite_sum_zero, ←ite_and]
Proof state after:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
⊢ (∑ x ∈ n.divisors, ∑ x_1 ∈ n.divisors, if x ∣ d ∧ x_1 ∣ d ∧ d = x.lcm x_1 then f x x_1 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Theorem: Aux.conv_lambda_sq_larger_sum
Proof state before:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
⊢ (∑ x ∈ n.divisors, ∑ x_1 ∈ n.divisors, if x ∣ d ∧ x_1 ∣ d ∧ d = x.lcm x_1 then f x x_1 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Tactic:
congr with d1
Proof state after:
case e_f.h
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 : ℕ
⊢ (∑ x ∈ n.divisors, if d1 ∣ d ∧ x ∣ d ∧ d = d1.lcm x then f d1 x d else 0) =
    ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Theorem: Aux.conv_lambda_sq_larger_sum
Proof state before:
case e_f.h
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 : ℕ
⊢ (∑ x ∈ n.divisors, if d1 ∣ d ∧ x ∣ d ∧ d = d1.lcm x then f d1 x d else 0) =
    ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Tactic:
congr with d2
Proof state after:
case e_f.h.e_f.h
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ (if d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2 then f d1 d2 d else 0) = if d = d1.lcm d2 then f d1 d2 d else 0
Theorem: Aux.conv_lambda_sq_larger_sum
Proof state before:
case e_f.h.e_f.h
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ (if d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2 then f d1 d2 d else 0) = if d = d1.lcm d2 then f d1 d2 d else 0
Tactic:
congr
Proof state after:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)
Theorem: Aux.conv_lambda_sq_larger_sum
Proof state before:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)
Tactic:
rw [eq_iff_iff]
Proof state after:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2 ↔ d = d1.lcm d2
Theorem: Aux.conv_lambda_sq_larger_sum
Proof state before:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2 ↔ d = d1.lcm d2
Tactic:
refine ⟨fun ⟨_, _, h⟩ ↦ h, ?_⟩
Proof state after:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ d = d1.lcm d2 → d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2
Theorem: Aux.conv_lambda_sq_larger_sum
Proof state before:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ d = d1.lcm d2 → d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2
Tactic:
rintro rfl
Proof state after:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d1 d2 : ℕ
hd : d1.lcm d2 ∣ n ∧ n ≠ 0
⊢ d1 ∣ d1.lcm d2 ∧ d2 ∣ d1.lcm d2 ∧ d1.lcm d2 = d1.lcm d2
Theorem: Aux.conv_lambda_sq_larger_sum
Proof state before:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d1 d2 : ℕ
hd : d1.lcm d2 ∣ n ∧ n ≠ 0
⊢ d1 ∣ d1.lcm d2 ∧ d2 ∣ d1.lcm d2 ∧ d1.lcm d2 = d1.lcm d2
Tactic:
exact ⟨Nat.dvd_lcm_left d1 d2, Nat.dvd_lcm_right d1 d2, rfl⟩
Proof state after:
no goals
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
l m : ℕ
hm : Squarefree m
⊢ (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0
Tactic:
have hm_pos : 0 < m := Nat.pos_of_ne_zero $ Squarefree.ne_zero hm
Proof state after:
l m : ℕ
hm : Squarefree m
hm_pos : 0 < m
⊢ (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
l m : ℕ
hm : Squarefree m
hm_pos : 0 < m
⊢ (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0
Tactic:
revert hm
Proof state after:
l m : ℕ
hm_pos : 0 < m
⊢ Squarefree m → (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
l m : ℕ
hm_pos : 0 < m
⊢ Squarefree m → (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0
Tactic:
revert m
Proof state after:
l : ℕ
⊢ ∀ (m : ℕ), 0 < m → Squarefree m → (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
l : ℕ
⊢ ∀ (m : ℕ), 0 < m → Squarefree m → (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0
Tactic:
apply (ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on {n | Squarefree n} (fun _ _ => Squarefree.squarefree_of_dvd)).mpr
Proof state after:
l : ℕ
⊢ ∀ n > 0,
    n ∈ {n | Squarefree n} →
      (∑ x ∈ n.divisorsAntidiagonal, μ x.1 • if l = x.2 then μ l else 0) = if l ∣ n then μ n else 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
l : ℕ
⊢ ∀ n > 0,
    n ∈ {n | Squarefree n} →
      (∑ x ∈ n.divisorsAntidiagonal, μ x.1 • if l = x.2 then μ l else 0) = if l ∣ n then μ n else 0
Tactic:
intro m hm_pos hm
Proof state after:
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
⊢ (∑ x ∈ m.divisorsAntidiagonal, μ x.1 • if l = x.2 then μ l else 0) = if l ∣ m then μ m else 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
⊢ (∑ x ∈ m.divisorsAntidiagonal, μ x.1 • if l = x.2 then μ l else 0) = if l ∣ m then μ m else 0
Tactic:
rw [sum_divisorsAntidiagonal' (f:= fun x y => μ x • if l=y then μ l else 0)]
Proof state after:
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0
Tactic:
by_cases hl : l ∣ m
Proof state after:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0

case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0
Tactic:
rw [if_pos hl, sum_eq_single l]
Proof state after:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ (μ (m / l) • if l = l then μ l else 0) = μ m

case pos.h₀
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ ∀ b ∈ m.divisors, b ≠ l → (μ (m / b) • if l = b then μ l else 0) = 0

case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ l ∉ m.divisors → (μ (m / l) • if l = l then μ l else 0) = 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ (μ (m / l) • if l = l then μ l else 0) = μ m
Tactic:
have hmul : m / l * l = m := Nat.div_mul_cancel hl
Proof state after:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ (μ (m / l) • if l = l then μ l else 0) = μ m
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ (μ (m / l) • if l = l then μ l else 0) = μ m
Tactic:
rw [if_pos rfl, smul_eq_mul, ←isMultiplicative_moebius.map_mul_of_coprime,
  hmul]
Proof state after:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ (m / l).Coprime l
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ (m / l).Coprime l
Tactic:
apply coprime_of_squarefree_mul
Proof state after:
case pos.h
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ Squarefree (m / l * l)
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case pos.h
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ Squarefree (m / l * l)
Tactic:
rw [hmul]
Proof state after:
case pos.h
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ Squarefree m
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case pos.h
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ Squarefree m
Tactic:
exact hm
Proof state after:
no goals
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case pos.h₀
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ ∀ b ∈ m.divisors, b ≠ l → (μ (m / b) • if l = b then μ l else 0) = 0
Tactic:
intro d _ hdl
Proof state after:
case pos.h₀
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
d : ℕ
a✝ : d ∈ m.divisors
hdl : d ≠ l
⊢ (μ (m / d) • if l = d then μ l else 0) = 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case pos.h₀
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
d : ℕ
a✝ : d ∈ m.divisors
hdl : d ≠ l
⊢ (μ (m / d) • if l = d then μ l else 0) = 0
Tactic:
rw[if_neg $ hdl.symm, smul_zero]
Proof state after:
no goals
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ l ∉ m.divisors → (μ (m / l) • if l = l then μ l else 0) = 0
Tactic:
intro h
Proof state after:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : l ∉ m.divisors
⊢ (μ (m / l) • if l = l then μ l else 0) = 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : l ∉ m.divisors
⊢ (μ (m / l) • if l = l then μ l else 0) = 0
Tactic:
rw[mem_divisors] at h
Proof state after:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : ¬(l ∣ m ∧ m ≠ 0)
⊢ (μ (m / l) • if l = l then μ l else 0) = 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : ¬(l ∣ m ∧ m ≠ 0)
⊢ (μ (m / l) • if l = l then μ l else 0) = 0
Tactic:
exfalso
Proof state after:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : ¬(l ∣ m ∧ m ≠ 0)
⊢ False
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : ¬(l ∣ m ∧ m ≠ 0)
⊢ False
Tactic:
exact h ⟨hl, (Nat.ne_of_lt hm_pos).symm⟩
Proof state after:
no goals
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0
Tactic:
rw [if_neg hl, sum_eq_zero]
Proof state after:
case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
⊢ ∀ x ∈ m.divisors, (μ (m / x) • if l = x then μ l else 0) = 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
⊢ ∀ x ∈ m.divisors, (μ (m / x) • if l = x then μ l else 0) = 0
Tactic:
intro d hd
Proof state after:
case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
⊢ (μ (m / d) • if l = d then μ l else 0) = 0
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
⊢ (μ (m / d) • if l = d then μ l else 0) = 0
Tactic:
rw [if_neg, smul_zero]
Proof state after:
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
⊢ ¬l = d
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
⊢ ¬l = d
Tactic:
by_contra h
Proof state after:
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
h : l = d
⊢ False
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
h : l = d
⊢ False
Tactic:
rw [←h] at hd
Proof state after:
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : l ∈ m.divisors
h : l = d
⊢ False
Theorem: Aux.moebius_inv_dvd_lower_bound
Proof state before:
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : l ∈ m.divisors
h : l = d
⊢ False
Tactic:
exact hl (dvd_of_mem_divisors hd)
Proof state after:
no goals
Theorem: Aux.moebius_inv_dvd_lower_bound'
Proof state before:
P : ℕ
hP : Squarefree P
l m : ℕ
hm : m ∣ P
⊢ (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ m then μ d else 0) = if l = m then μ l else 0
Tactic:
rw [←moebius_inv_dvd_lower_bound _ _ (Squarefree.squarefree_of_dvd hm hP),
  sum_over_dvd_ite hP.ne_zero hm]
Proof state after:
P : ℕ
hP : Squarefree P
l m : ℕ
hm : m ∣ P
⊢ (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ m then μ d else 0) = ∑ d ∈ P.divisors, if d ∣ m then if l ∣ d then μ d else 0 else 0
Theorem: Aux.moebius_inv_dvd_lower_bound'
Proof state before:
P : ℕ
hP : Squarefree P
l m : ℕ
hm : m ∣ P
⊢ (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ m then μ d else 0) = ∑ d ∈ P.divisors, if d ∣ m then if l ∣ d then μ d else 0 else 0
Tactic:
simp_rw[ite_and, ←sum_filter, filter_comm]
Proof state after:
no goals
Theorem: Aux.moebius_inv_dvd_lower_bound_real
Proof state before:
P : ℕ
hP : Squarefree P
l m : ℕ
hm : m ∣ P
⊢ (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ m then ↑(μ d) else 0) = if l = m then ↑(μ l) else 0
Tactic:
norm_cast
Proof state after:
P : ℕ
hP : Squarefree P
l m : ℕ
hm : m ∣ P
⊢ (∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ m then μ x else 0) = if l = m then μ l else 0
Theorem: Aux.moebius_inv_dvd_lower_bound_real
Proof state before:
P : ℕ
hP : Squarefree P
l m : ℕ
hm : m ∣ P
⊢ (∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ m then μ x else 0) = if l = m then μ l else 0
Tactic:
apply moebius_inv_dvd_lower_bound' hP l m hm
Proof state after:
no goals
Theorem: Aux.gcd_dvd_mul
Proof state before:
m n : ℕ
⊢ m.gcd n ∣ m * n
Tactic:
calc
  m.gcd n ∣ m := Nat.gcd_dvd_left m n
  _ ∣ m * n := ⟨n, rfl⟩
Proof state after:
no goals
Theorem: Aux.multiplicative_zero_of_zero_dvd
Proof state before:
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
m n : ℕ
h_sq : Squarefree n
hmn : m ∣ n
h_zero : f m = 0
⊢ f n = 0
Tactic:
rcases hmn with ⟨k, rfl⟩
Proof state after:
case intro
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
m : ℕ
h_zero : f m = 0
k : ℕ
h_sq : Squarefree (m * k)
⊢ f (m * k) = 0
Theorem: Aux.multiplicative_zero_of_zero_dvd
Proof state before:
case intro
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
m : ℕ
h_zero : f m = 0
k : ℕ
h_sq : Squarefree (m * k)
⊢ f (m * k) = 0
Tactic:
simp only [MulZeroClass.zero_mul, eq_self_iff_true, h_mult.map_mul_of_coprime
  (coprime_of_squarefree_mul h_sq), h_zero]
Proof state after:
no goals
Theorem: Aux.primeDivisors_nonempty
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ n.primeFactors.Nonempty
Tactic:
unfold Finset.Nonempty
Proof state after:
n : ℕ
hn : 2 ≤ n
⊢ ∃ x, x ∈ n.primeFactors
Theorem: Aux.primeDivisors_nonempty
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ ∃ x, x ∈ n.primeFactors
Tactic:
simp_rw[Nat.mem_primeFactors_of_ne_zero (by positivity)]
Proof state after:
n : ℕ
hn : 2 ≤ n
⊢ ∃ x, x.Prime ∧ x ∣ n
Theorem: Aux.primeDivisors_nonempty
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ ∃ x, x.Prime ∧ x ∣ n
Tactic:
apply Nat.exists_prime_and_dvd (by linarith)
Proof state after:
no goals
Theorem: Aux.primeDivisors_nonempty
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ ?m.33651 ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: Aux.primeDivisors_nonempty
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ n ≠ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Aux.div_mult_of_dvd_squarefree
Proof state before:
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ f l / f d = f (l / d)
Tactic:
apply div_eq_of_eq_mul hd
Proof state after:
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ f l = f (l / d) * f d
Theorem: Aux.div_mult_of_dvd_squarefree
Proof state before:
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ f l = f (l / d) * f d
Tactic:
rw [← h_mult.right, Nat.div_mul_cancel hdl]
Proof state after:
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ (l / d).Coprime d
Theorem: Aux.div_mult_of_dvd_squarefree
Proof state before:
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ (l / d).Coprime d
Tactic:
apply coprime_of_squarefree_mul
Proof state after:
case h
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ Squarefree (l / d * d)
Theorem: Aux.div_mult_of_dvd_squarefree
Proof state before:
case h
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ Squarefree (l / d * d)
Tactic:
convert hl
Proof state after:
case h.e'_3
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ l / d * d = l
Theorem: Aux.div_mult_of_dvd_squarefree
Proof state before:
case h.e'_3
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ l / d * d = l
Tactic:
exact Nat.div_mul_cancel hdl
Proof state after:
no goals
Theorem: Aux.inv_sub_antitoneOn_gt
Proof state before:
R : Type u_1
inst✝ : LinearOrderedField R
c : R
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Ioi c)
Tactic:
refine antitoneOn_iff_forall_lt.mpr ?_
Proof state after:
R : Type u_1
inst✝ : LinearOrderedField R
c : R
⊢ ∀ ⦃a : R⦄, a ∈ Set.Ioi c → ∀ ⦃b : R⦄, b ∈ Set.Ioi c → a < b → (b - c)⁻¹ ≤ (a - c)⁻¹
Theorem: Aux.inv_sub_antitoneOn_gt
Proof state before:
R : Type u_1
inst✝ : LinearOrderedField R
c : R
⊢ ∀ ⦃a : R⦄, a ∈ Set.Ioi c → ∀ ⦃b : R⦄, b ∈ Set.Ioi c → a < b → (b - c)⁻¹ ≤ (a - c)⁻¹
Tactic:
intro a ha b hb hab
Proof state after:
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : a ∈ Set.Ioi c
b : R
hb : b ∈ Set.Ioi c
hab : a < b
⊢ (b - c)⁻¹ ≤ (a - c)⁻¹
Theorem: Aux.inv_sub_antitoneOn_gt
Proof state before:
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : a ∈ Set.Ioi c
b : R
hb : b ∈ Set.Ioi c
hab : a < b
⊢ (b - c)⁻¹ ≤ (a - c)⁻¹
Tactic:
rw [Set.mem_Ioi] at ha hb
Proof state after:
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : c < a
b : R
hb : c < b
hab : a < b
⊢ (b - c)⁻¹ ≤ (a - c)⁻¹
Theorem: Aux.inv_sub_antitoneOn_gt
Proof state before:
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : c < a
b : R
hb : c < b
hab : a < b
⊢ (b - c)⁻¹ ≤ (a - c)⁻¹
Tactic:
gcongr
Proof state after:
case ha
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : c < a
b : R
hb : c < b
hab : a < b
⊢ 0 < a - c
Theorem: Aux.inv_sub_antitoneOn_gt
Proof state before:
case ha
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : c < a
b : R
hb : c < b
hab : a < b
⊢ 0 < a - c
Tactic:
linarith
Proof state after:
no goals
Theorem: Aux.inv_sub_antitoneOn_Icc
Proof state before:
R : Type u_1
inst✝ : LinearOrderedField R
a b c : R
ha : c < a
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
Tactic:
by_cases hab : a ≤ b
Proof state after:
case pos
R : Type u_1
inst✝ : LinearOrderedField R
a b c : R
ha : c < a
hab : a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)

case neg
R : Type u_1
inst✝ : LinearOrderedField R
a b c : R
ha : c < a
hab : ¬a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
Theorem: Aux.inv_sub_antitoneOn_Icc
Proof state before:
case pos
R : Type u_1
inst✝ : LinearOrderedField R
a b c : R
ha : c < a
hab : a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
Tactic:
exact inv_sub_antitoneOn_gt c |>.mono <| (Set.Icc_subset_Ioi_iff hab).mpr ha
Proof state after:
no goals
Theorem: Aux.inv_sub_antitoneOn_Icc
Proof state before:
case neg
R : Type u_1
inst✝ : LinearOrderedField R
a b c : R
ha : c < a
hab : ¬a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
Tactic:
simp [hab, Set.Subsingleton.antitoneOn]
Proof state after:
no goals
Theorem: Aux.inv_antitoneOn_pos
Proof state before:
R : Type u_1
inst✝ : LinearOrderedField R
⊢ AntitoneOn (fun x => x⁻¹) (Set.Ioi 0)
Tactic:
convert inv_sub_antitoneOn_gt (R:=R) 0
Proof state after:
case h.e'_5.h.h.e'_3
R : Type u_1
inst✝ : LinearOrderedField R
x✝ : R
⊢ x✝ = x✝ - 0
Theorem: Aux.inv_antitoneOn_pos
Proof state before:
case h.e'_5.h.h.e'_3
R : Type u_1
inst✝ : LinearOrderedField R
x✝ : R
⊢ x✝ = x✝ - 0
Tactic:
ring
Proof state after:
no goals
Theorem: Aux.inv_antitoneOn_Icc
Proof state before:
R : Type u_1
inst✝ : LinearOrderedField R
a b : R
ha : 0 < a
⊢ AntitoneOn (fun x => x⁻¹) (Set.Icc a b)
Tactic:
convert inv_sub_antitoneOn_Icc a b 0 ha
Proof state after:
case h.e'_5.h.h.e'_3
R : Type u_1
inst✝ : LinearOrderedField R
a b : R
ha : 0 < a
x✝ : R
⊢ x✝ = x✝ - 0
Theorem: Aux.inv_antitoneOn_Icc
Proof state before:
case h.e'_5.h.h.e'_3
R : Type u_1
inst✝ : LinearOrderedField R
a b : R
ha : 0 < a
x✝ : R
⊢ x✝ = x✝ - 0
Tactic:
ring
Proof state after:
no goals
Theorem: Aux.log_add_one_le_sum_inv
Proof state before:
n : ℕ
⊢ (↑(n + 1)).log ≤ ∑ d ∈ Icc 1 n, (↑d)⁻¹
Tactic:
calc _ = ∫ x in (1)..↑(n+1), x⁻¹ := ?_
     _ = ∫ x in (1:ℕ)..↑(n+1), x⁻¹ := ?_
     _ ≤ _ := ?_
Proof state after:
case calc_1
n : ℕ
⊢ (↑(n + 1)).log = ∫ (x : ℝ) in 1 ..↑(n + 1), x⁻¹

case calc_2
n : ℕ
⊢ ∫ (x : ℝ) in 1 ..↑(n + 1), x⁻¹ = ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹

case calc_3
n : ℕ
⊢ ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹ ≤ ∑ d ∈ Icc 1 n, (↑d)⁻¹
Theorem: Aux.log_add_one_le_sum_inv
Proof state before:
case calc_1
n : ℕ
⊢ (↑(n + 1)).log = ∫ (x : ℝ) in 1 ..↑(n + 1), x⁻¹
Tactic:
rw[integral_inv (by simp[(show ¬ (1:ℝ) ≤ 0 by norm_num)] )]
Proof state after:
case calc_1
n : ℕ
⊢ (↑(n + 1)).log = (↑(n + 1) / 1).log
Theorem: Aux.log_add_one_le_sum_inv
Proof state before:
case calc_1
n : ℕ
⊢ (↑(n + 1)).log = (↑(n + 1) / 1).log
Tactic:
congr
Proof state after:
case calc_1.e_x
n : ℕ
⊢ ↑(n + 1) = ↑(n + 1) / 1
Theorem: Aux.log_add_one_le_sum_inv
Proof state before:
case calc_1.e_x
n : ℕ
⊢ ↑(n + 1) = ↑(n + 1) / 1
Tactic:
ring
Proof state after:
no goals
Theorem: Aux.log_add_one_le_sum_inv
Proof state before:
n : ℕ
⊢ 0 ∉ Set.uIcc 1 ↑(n + 1)
Tactic:
simp[(show ¬ (1:ℝ) ≤ 0 by norm_num)]
Proof state after:
no goals
Theorem: Aux.log_add_one_le_sum_inv
Proof state before:
n : ℕ
⊢ ¬1 ≤ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Aux.log_add_one_le_sum_inv
Proof state before:
case calc_2
n : ℕ
⊢ ∫ (x : ℝ) in 1 ..↑(n + 1), x⁻¹ = ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹
Tactic:
congr
Proof state after:
case calc_2.e_a
n : ℕ
⊢ 1 = ↑1