internlm/Lean-Github huggingface dataset:
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case neg
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : ¬(p.Prime ∧ p ∣ d ∧ d ≠ 0)
⊢ (¬p.Prime ∨ ¬p ∣ b) ∨ b = 0
Tactic:
left
Proof state after:
case neg.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : ¬(p.Prime ∧ p ∣ d ∧ d ≠ 0)
⊢ ¬p.Prime ∨ ¬p ∣ b
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case neg.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : ¬(p.Prime ∧ p ∣ d ∧ d ≠ 0)
⊢ ¬p.Prime ∨ ¬p ∣ b
Tactic:
push_neg at hp
Proof state after:
case neg.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
⊢ ¬p.Prime ∨ ¬p ∣ b
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case pos
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
hpp : p.Prime
⊢ ¬p.Prime ∨ ¬p ∣ b
Tactic:
right
Proof state after:
case pos.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
hpp : p.Prime
⊢ ¬p ∣ b
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case pos.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
hpp : p.Prime
⊢ ¬p ∣ b
Tactic:
intro h
Proof state after:
case pos.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝¹ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h✝ : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
hpp : p.Prime
h : p ∣ b
⊢ False
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case pos.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝¹ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h✝ : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
hpp : p.Prime
h : p ∣ b
⊢ False
Tactic:
apply absurd (hp hpp)
Proof state after:
case pos.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝¹ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h✝ : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
hpp : p.Prime
h : p ∣ b
⊢ ¬(p ∣ d → d = 0)
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case pos.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝¹ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h✝ : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
hpp : p.Prime
h : p ∣ b
⊢ ¬(p ∣ d → d = 0)
Tactic:
push_neg
Proof state after:
case pos.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝¹ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h✝ : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
hpp : p.Prime
h : p ∣ b
⊢ p ∣ d ∧ d ≠ 0
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case pos.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝¹ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h✝ : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
hpp : p.Prime
h : p ∣ b
⊢ p ∣ d ∧ d ≠ 0
Tactic:
exact ⟨hpp.dvd_of_dvd_pow (h.trans hb.1.1), hd.ne_zero⟩
Proof state after:
no goals
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case neg
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
hpp : ¬p.Prime
⊢ ¬p.Prime ∨ ¬p ∣ b
Tactic:
left
Proof state after:
case neg.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
hpp : ¬p.Prime
⊢ ¬p.Prime
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case neg.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h✝ :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
i_inj :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M)
    (b : (a : ℕ) → a ∈ d.primeFactors → ℕ) (hb : b ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = i b hb → a = b
b : ℕ
hb : (b ∣ d ^ M ∧ d ^ M ≠ 0) ∧ d ∣ b
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p.Prime → p ∣ d → d = 0
hpp : ¬p.Prime
⊢ ¬p.Prime
Tactic:
exact hpp
Proof state after:
no goals
Theorem: Sieve.prod_primes_dvd_of_dvd
Proof state before:
P : ℕ
s : Finset ℕ
h : ∀ p ∈ s, p ∣ P
h' : ∀ p ∈ s, p.Prime
⊢ ∏ p ∈ s, p ∣ P
Tactic:
simp_rw [Nat.prime_iff] at h'
Proof state after:
P : ℕ
s : Finset ℕ
h : ∀ p ∈ s, p ∣ P
h' : ∀ p ∈ s, Prime p
⊢ ∏ p ∈ s, p ∣ P
Theorem: Sieve.prod_primes_dvd_of_dvd
Proof state before:
P : ℕ
s : Finset ℕ
h : ∀ p ∈ s, p ∣ P
h' : ∀ p ∈ s, Prime p
⊢ ∏ p ∈ s, p ∣ P
Tactic:
apply Finset.prod_primes_dvd _ h' h
Proof state after:
no goals
Theorem: Sieve.sqrt_le_self
Proof state before:
x : ℝ
hx : 1 ≤ x
⊢ √x ≤ x
Tactic:
refine Iff.mpr Real.sqrt_le_iff ?_
Proof state after:
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x ∧ x ≤ x ^ 2
Theorem: Sieve.sqrt_le_self
Proof state before:
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x ∧ x ≤ x ^ 2
Tactic:
constructor
Proof state after:
case left
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x

case right
x : ℝ
hx : 1 ≤ x
⊢ x ≤ x ^ 2
Theorem: Sieve.sqrt_le_self
Proof state before:
case right
x : ℝ
hx : 1 ≤ x
⊢ x ≤ x ^ 2
Tactic:
refine le_self_pow hx ?right.h
Proof state after:
case right.h
x : ℝ
hx : 1 ≤ x
⊢ 2 ≠ 0
Theorem: Sieve.sqrt_le_self
Proof state before:
case right.h
x : ℝ
hx : 1 ≤ x
⊢ 2 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Sieve.sqrt_le_self
Proof state before:
case left
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: Sieve.Nat.squarefree_dvd_pow
Proof state before:
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
⊢ a ∣ b
Tactic:
by_cases hN : N=0
Proof state after:
case pos
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
hN : N = 0
⊢ a ∣ b

case neg
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
hN : ¬N = 0
⊢ a ∣ b
Theorem: Sieve.Nat.squarefree_dvd_pow
Proof state before:
case neg
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
hN : ¬N = 0
⊢ a ∣ b
Tactic:
rw [Squarefree.dvd_pow_iff_dvd ha hN] at hab
Proof state after:
case neg
a b N : ℕ
ha : Squarefree a
hab : a ∣ b
hN : ¬N = 0
⊢ a ∣ b
Theorem: Sieve.Nat.squarefree_dvd_pow
Proof state before:
case neg
a b N : ℕ
ha : Squarefree a
hab : a ∣ b
hN : ¬N = 0
⊢ a ∣ b
Tactic:
exact hab
Proof state after:
no goals
Theorem: Sieve.Nat.squarefree_dvd_pow
Proof state before:
case pos
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
hN : N = 0
⊢ a ∣ b
Tactic:
rw [hN, pow_zero, Nat.dvd_one] at hab
Proof state after:
case pos
a b N : ℕ
ha : Squarefree a
hab : a = 1
hN : N = 0
⊢ a ∣ b