internlm/Lean-Github huggingface dataset:
Theorem: Nat.f_inj
Proof state before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : b 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
⊢ a 1 = b 1
Tactic:
exact (mul_right_inj' $ ne_zero_of_mem_finMulAntidiagonal hb 0).mp hfab1
Proof state after:
no goals
Theorem: Nat.f_surj
Proof state before:
n : ℕ
hn : n ≠ 0
⊢ ∀
    b ∈
      filter
        (fun x =>
          match x with
          | (x, y) => x.lcm y = n)
        (n.divisors ×ˢ n.divisors),
    ∃ a, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Tactic:
intro b hb
Proof state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb :
  b ∈
    filter
      (fun x =>
        match x with
        | (x, y) => x.lcm y = n)
      (n.divisors ×ˢ n.divisors)
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Theorem: Nat.f_surj
Proof state before:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb :
  b ∈
    filter
      (fun x =>
        match x with
        | (x, y) => x.lcm y = n)
      (n.divisors ×ˢ n.divisors)
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Tactic:
dsimp only at hb
Proof state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Theorem: Nat.f_surj
Proof state before:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Tactic:
let g := b.fst.gcd b.snd
Proof state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Theorem: Nat.f_surj
Proof state before:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Tactic:
let a := ![g, b.fst/g, b.snd/g]
Proof state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Theorem: Nat.f_surj
Proof state before:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiagonal 3 n
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Tactic:
use a
Proof state after:
case h
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiagonal 3 n
⊢ ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Theorem: Nat.f_surj
Proof state before:
case h
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiagonal 3 n
⊢ ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Tactic:
use ha
Proof state after:
case h
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiagonal 3 n
⊢ Nat.f a ha = b
Theorem: Nat.f_surj
Proof state before:
case h
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiagonal 3 n
⊢ Nat.f a ha = b
Tactic:
apply Prod.ext <;> simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
  <;> apply Nat.mul_div_cancel'
Proof state after:
case h.a.H
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 ∣ b.1

case h.a.H
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 ∣ b.2
Theorem: Nat.f_surj
Proof state before:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ a ∈ finMulAntidiagonal 3 n
Tactic:
rw [mem_finMulAntidiagonal]
Proof state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin (succ 0).succ.succ, a i = n ∧ n ≠ 0
Theorem: Nat.f_surj
Proof state before:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin (succ 0).succ.succ, a i = n ∧ n ≠ 0
Tactic:
rw [mem_filter, Finset.mem_product] at hb
Proof state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin (succ 0).succ.succ, a i = n ∧ n ≠ 0
Theorem: Nat.f_surj
Proof state before:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin (succ 0).succ.succ, a i = n ∧ n ≠ 0
Tactic:
refine ⟨?_, hn⟩
Proof state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin (succ 0).succ.succ, a i = n
Theorem: Nat.f_surj
Proof state before:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin (succ 0).succ.succ, a i = n
Tactic:
rw [Fin.prod_univ_three a]
Proof state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ a 0 * a 1 * a 2 = n
Theorem: Nat.f_surj
Proof state before:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ a 0 * a 1 * a 2 = n
Tactic:
unfold_let a
Proof state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ![g, b.1 / g, b.2 / g] 0 * ![g, b.1 / g, b.2 / g] 1 * ![g, b.1 / g, b.2 / g] 2 = n
Theorem: Nat.f_surj
Proof state before:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ![g, b.1 / g, b.2 / g] 0 * ![g, b.1 / g, b.2 / g] 1 * ![g, b.1 / g, b.2 / g] 2 = n
Tactic:
simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two,
  Matrix.tail_cons]
Proof state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ g * (b.1 / g) * (b.2 / g) = n
Theorem: Nat.f_surj
Proof state before:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ g * (b.1 / g) * (b.2 / g) = n
Tactic:
rw [Nat.mul_div_cancel_left' (Nat.gcd_dvd_left _ _), ←hb.2, lcm,
  Nat.mul_div_assoc b.fst (Nat.gcd_dvd_right b.fst b.snd)]
Proof state after:
no goals
Theorem: Nat.f_surj
Proof state before:
case h.a.H
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 ∣ b.1
Tactic:
apply Nat.gcd_dvd_left
Proof state after:
no goals
Theorem: Nat.f_surj
Proof state before:
case h.a.H
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 ∣ b.2
Tactic:
apply Nat.gcd_dvd_right
Proof state after:
no goals
Theorem: Nat.card_lcm_eq
Proof state before:
n : ℕ
hn : Squarefree n
⊢ (filter
        (fun x =>
          match x with
          | (x, y) => x.lcm y = n)
        (n.divisors ×ˢ n.divisors)).card =
    3 ^ ω n
Tactic:
rw [← card_finMulAntidiagonal hn, eq_comm]
Proof state after:
n : ℕ
hn : Squarefree n
⊢ (finMulAntidiagonal 3 n).card =
    (filter
        (fun x =>
          match x with
          | (x, y) => x.lcm y = n)
        (n.divisors ×ˢ n.divisors)).card
Theorem: Nat.card_lcm_eq
Proof state before:
n : ℕ
hn : Squarefree n
⊢ (finMulAntidiagonal 3 n).card =
    (filter
        (fun x =>
          match x with
          | (x, y) => x.lcm y = n)
        (n.divisors ×ˢ n.divisors)).card
Tactic:
exact Finset.card_bij f (f_img hn) f_inj (f_surj hn.ne_zero)
Proof state after:
no goals
Theorem: finsum_range_eq_sum_range
Proof state before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
⊢ ∑ᶠ (n : ℕ) (_ : ↑n < x), f n = ∑ n ∈ range ⌈x⌉₊, f n
Tactic:
apply finsum_cond_eq_sum_of_cond_iff f
Proof state after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
⊢ ∀ {x_1 : ℕ}, f x_1 ≠ 0 → (↑x_1 < x ↔ x_1 ∈ range ⌈x⌉₊)
Theorem: finsum_range_eq_sum_range
Proof state before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
⊢ ∀ {x_1 : ℕ}, f x_1 ≠ 0 → (↑x_1 < x ↔ x_1 ∈ range ⌈x⌉₊)
Tactic:
intros
Proof state after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
x✝ : ℕ
a✝ : f x✝ ≠ 0
⊢ ↑x✝ < x ↔ x✝ ∈ range ⌈x⌉₊
Theorem: finsum_range_eq_sum_range
Proof state before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
x✝ : ℕ
a✝ : f x✝ ≠ 0
⊢ ↑x✝ < x ↔ x✝ ∈ range ⌈x⌉₊
Tactic:
simp only [mem_range]
Proof state after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
x✝ : ℕ
a✝ : f x✝ ≠ 0
⊢ ↑x✝ < x ↔ x✝ < ⌈x⌉₊
Theorem: finsum_range_eq_sum_range
Proof state before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
x✝ : ℕ
a✝ : f x✝ ≠ 0
⊢ ↑x✝ < x ↔ x✝ < ⌈x⌉₊
Tactic:
exact Iff.symm Nat.lt_ceil
Proof state after:
no goals
Theorem: finsum_range_eq_sum_range'
Proof 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
Proof 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⌋₊)
Theorem: finsum_range_eq_sum_range'
Proof 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
Proof state after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
n : ℕ
h : f n ≠ 0
⊢ ↑n ≤ x ↔ n ∈ Iic ⌊x⌋₊
Theorem: finsum_range_eq_sum_range'
Proof 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]
Proof state after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
n : ℕ
h : f n ≠ 0
⊢ ↑n ≤ x ↔ n ≤ ⌊x⌋₊
Theorem: finsum_range_eq_sum_range'
Proof 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
Proof state after:
no goals
Theorem: chebyshev_asymptotic
Proof state before:
⊢ (fun x => ∑ p ∈ filter Nat.Prime (range ⌈x⌉₊), (↑p).log) ~[atTop] fun x => x
Tactic:
sorry
Proof state after:
no goals
Theorem: chebyshev_asymptotic_finsum
Proof state before:
⊢ (fun x => ∑ᶠ (p : ℕ) (_ : p ≤ x) (_ : p.Prime), (↑p).log) ~[atTop] fun x => ↑x
Tactic:
sorry
Proof state after:
no goals
Theorem: primorial_bounds
Proof state before:
⊢ ∃ E, (E =o[atTop] fun x => x) ∧ ∀ (x : ℝ), ↑(∏ p ∈ filter Nat.Prime (range ⌊x⌋₊), p) = rexp (x + E x)
Tactic:
sorry
Proof state after:
no goals
Theorem: primorial_bounds_finprod
Proof state before:
⊢ ∃ E, (E =o[atTop] fun x => x) ∧ ∀ (x : ℝ), ↑(∏ᶠ (p : ℕ) (_ : ↑p ≤ x) (_ : p.Prime), p) = rexp (x + E x)
Tactic:
sorry
Proof state after:
no goals
Theorem: pi_asymp
Proof state before:
⊢ ∃ c, (c =o[atTop] fun x => 1) ∧ ∀ (x : ℝ), ↑(π ⌊x⌋₊) = (1 + c x) * ∫ (t : ℝ) in Set.Icc 2 x, 1 / t.log
Tactic:
sorry
Proof state after:
no goals
Theorem: pi_alt
Proof state before:
⊢ ∃ c, (c =o[atTop] fun x => 1) ∧ ∀ (x : ℝ), ↑(π ⌊x⌋₊) = (1 + c x) * x / x.log
Tactic:
sorry
Proof state after:
no goals
Theorem: pn_asymptotic
Proof state before:
⊢ ∃ c, (c =o[atTop] fun x => 1) ∧ ∀ (n : ℕ), ↑(nth Nat.Prime n) = (1 + c n) * ↑n * (↑n).log
Tactic:
sorry
Proof state after:
no goals
Theorem: pn_pn_plus_one
Proof state before:
⊢ ∃ c, (c =o[atTop] fun x => 1) ∧ ∀ (n : ℕ), ↑(nth Nat.Prime (n + 1)) - ↑(nth Nat.Prime n) = c n * ↑(nth Nat.Prime n)
Tactic:
sorry
Proof state after:
no goals
Theorem: prime_between
Proof state before:
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (x : ℝ) in atTop, ∃ p, p.Prime ∧ x < ↑p ∧ ↑p < (1 + ε) * x
Tactic:
sorry
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof state before:
N : ℕ
⊢ |∑ n ∈ range N, ↑(μ n) / ↑n| ≤ 1
Tactic:
cases' N with N
Proof state after:
case zero

⊢ |∑ n ∈ range 0, ↑(μ n) / ↑n| ≤ 1

case succ
N : ℕ
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case zero

⊢ |∑ n ∈ range 0, ↑(μ n) / ↑n| ≤ 1

case succ
N : ℕ
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
simp only [range_zero, sum_empty, abs_zero, zero_le_one]
Proof state after:
case succ
N : ℕ
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case succ
N : ℕ
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
by_cases hN : 1 ≤ N
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

case neg
N : ℕ
hN : ¬1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

case neg
N : ℕ
hN : ¬1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
swap
Proof state after:
case neg
N : ℕ
hN : ¬1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

case pos
N : ℕ
hN : 1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
rw [sum_congr rfl (g := fun d ↦ (μ d : ℚ) * ⌊(N : ℚ) / (d : ℚ)⌋)] at h_sum
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
⊢ ∀ x ∈ range (N + 1), ↑(μ x) * ↑(N / x) = ↑(μ x) * ↑⌊↑N / ↑x⌋
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
⊢ ∀ x ∈ range (N + 1), ↑(μ x) * ↑(N / x) = ↑(μ x) * ↑⌊↑N / ↑x⌋
Tactic:
swap
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
⊢ ∀ x ∈ range (N + 1), ↑(μ x) * ↑(N / x) = ↑(μ x) * ↑⌊↑N / ↑x⌋

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
⊢ ∀ x ∈ range (N + 1), ↑(μ x) * ↑(N / x) = ↑(μ x) * ↑⌊↑N / ↑x⌋

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
intros
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
x✝ : ℕ
a✝ : x✝ ∈ range (N + 1)
⊢ ↑(μ x✝) * ↑(N / x✝) = ↑(μ x✝) * ↑⌊↑N / ↑x✝⌋

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
x✝ : ℕ
a✝ : x✝ ∈ range (N + 1)
⊢ ↑(μ x✝) * ↑(N / x✝) = ↑(μ x✝) * ↑⌊↑N / ↑x✝⌋

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
rw [show (N : ℚ) = ((N : ℤ) : ℚ) by norm_cast, Rat.floor_int_div_nat_eq_div]
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
x✝ : ℕ
a✝ : x✝ ∈ range (N + 1)
⊢ ↑(μ x✝) * ↑(N / x✝) = ↑(μ x✝) * ↑(↑N / ↑x✝)

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
x✝ : ℕ
a✝ : x✝ ∈ range (N + 1)
⊢ ↑(μ x✝) * ↑(N / x✝) = ↑(μ x✝) * ↑(↑N / ↑x✝)

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
congr
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
have hf' (d : ℕ) : |Int.fract ((N : ℚ) / d)| < 1 := by
  rw [abs_of_nonneg (Int.fract_nonneg _)]
  exact Int.fract_lt_one _
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
have h_bound : |∑ d in range (N + 1), μ d * Int.fract ((N : ℚ) / d)| ≤ N - 1 := by
  
  rw [range_eq_Ico, ← Ico_insert_succ_left, sum_insert, ArithmeticFunction.map_zero,
    Int.cast_zero, zero_mul, zero_add, Ico_succ_right]
  all_goals simp
  
  rw [← Ico_insert_right, sum_insert, div_self, Int.fract_one, mul_zero]
  all_goals simp [hN, Nat.pos_iff_ne_zero.mp hN]
  
  have (d : ℕ) : |μ d * Int.fract ((N : ℚ) / d)| ≤ 1 := by
    rw [abs_mul, ← one_mul 1]
    apply mul_le_mul ?_ (hf' _).le (abs_nonneg _) zero_le_one
    norm_cast
    simp [moebius]
    split_ifs <;> simp only [abs_zero, zero_le_one, abs_pow, abs_neg, abs_one, one_pow, le_refl]
  apply (abs_sum_le_sum_abs _ _).trans
  apply (sum_le_sum fun d _ ↦ this d).trans
  all_goals simp [sum_ite, cast_sub hN]
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
rw [sum_congr rfl (g := fun d : ℕ ↦ μ d * ((N : ℚ) / d - Int.fract ((N : ℚ) / d)))
  fun d _ ↦ by simp only [Int.fract, sub_sub_self]] at h_sum
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * (↑N / ↑d - Int.fract (↑N / ↑d))
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * (↑N / ↑d - Int.fract (↑N / ↑d))
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
simp_rw (config := {singlePass := true}) [mul_sub] at h_sum
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : 1 = ∑ x ∈ range (N + 1), (↑(μ x) * (↑N / ↑x) - ↑(μ x) * Int.fract (↑N / ↑x))
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : 1 = ∑ x ∈ range (N + 1), (↑(μ x) * (↑N / ↑x) - ↑(μ x) * Int.fract (↑N / ↑x))
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
simp_rw [← mul_comm_div, sum_sub_distrib, ← sum_mul] at h_sum
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : 1 = (∑ i ∈ range (N + 1), ↑(μ i) / ↑i) * ↑N - ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : 1 = (∑ i ∈ range (N + 1), ↑(μ i) / ↑i) * ↑N - ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
rw [eq_sub_iff_add_eq, eq_comm, ← eq_div_iff (by norm_num [Nat.pos_iff_ne_zero.mp hN])] at h_sum
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : ∑ i ∈ range (N + 1), ↑(μ i) / ↑i = (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : ∑ i ∈ range (N + 1), ↑(μ i) / ↑i = (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
rw [h_sum, abs_le]
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : ∑ i ∈ range (N + 1), ↑(μ i) / ↑i = (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N
⊢ -1 ≤ (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ∧
    (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : ∑ i ∈ range (N + 1), ↑(μ i) / ↑i = (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N
⊢ -1 ≤ (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ∧
    (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ≤ 1
Tactic:
rw [abs_le, neg_sub] at h_bound
Proof state after:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound :
  1 - ↑N ≤ ∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d) ∧
    ∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d) ≤ ↑N - 1
h_sum : ∑ i ∈ range (N + 1), ↑(μ i) / ↑i = (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N
⊢ -1 ≤ (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ∧
    (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ≤ 1