internlm/Lean-Github huggingface dataset:
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha✝ : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
a✝ : p ∈ (i a ha✝).factorization.support
hp : p ∈ d.primeFactors
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 1 ≤ a a_1 h ∧ a a_1 h ≤ M
⊢ M • 1 ≤ M • d.factorization p
Tactic:
gcongr
Proof state after:
case hab
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha✝ : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
a✝ : p ∈ (i a ha✝).factorization.support
hp : p ∈ d.primeFactors
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 1 ≤ a a_1 h ∧ a a_1 h ≤ M
⊢ 1 ≤ d.factorization p
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case hab
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha✝ : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
a✝ : p ∈ (i a ha✝).factorization.support
hp : p ∈ d.primeFactors
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 1 ≤ a a_1 h ∧ a a_1 h ≤ M
⊢ 1 ≤ d.factorization p
Tactic:
rw [Nat.mem_primeFactors_of_ne_zero hd.ne_zero] at hp
Proof state after:
case hab
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha✝ : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
a✝ : p ∈ (i a ha✝).factorization.support
hp : p.Prime ∧ p ∣ d
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 1 ≤ a a_1 h ∧ a a_1 h ≤ M
⊢ 1 ≤ d.factorization p
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case hab
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha✝ : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
a✝ : p ∈ (i a ha✝).factorization.support
hp : p.Prime ∧ p ∣ d
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 1 ≤ a a_1 h ∧ a a_1 h ≤ M
⊢ 1 ≤ d.factorization p
Tactic:
rw [←Nat.Prime.dvd_iff_one_le_factorization hp.1 hd.ne_zero]
Proof state after:
case hab
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha✝ : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
a✝ : p ∈ (i a ha✝).factorization.support
hp : p.Prime ∧ p ∣ d
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 1 ≤ a a_1 h ∧ a a_1 h ≤ M
⊢ p ∣ d
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case hab
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha✝ : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
a✝ : p ∈ (i a ha✝).factorization.support
hp : p.Prime ∧ p ∣ d
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 1 ≤ a a_1 h ∧ a a_1 h ≤ M
⊢ p ∣ d
Tactic:
exact hp.2
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
a✝ : p ∈ (i a ha).factorization.support
hp : p ∉ d.primeFactors
⊢ (if hp : p ∈ d.primeFactors then a p hp else 0) ≤ (d ^ M).factorization p
Tactic:
rw [dif_neg hp]
Proof state after:
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
a✝ : p ∈ (i a ha).factorization.support
hp : p ∉ d.primeFactors
⊢ 0 ≤ (d ^ M).factorization p
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
a✝ : p ∈ (i a ha).factorization.support
hp : p ∉ d.primeFactors
⊢ 0 ≤ (d ^ M).factorization p
Tactic:
norm_num
Proof state after:
no goals
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case left.right
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
⊢ d ^ M ≠ 0
Tactic:
apply pow_ne_zero _ hd.ne_zero
Proof state after:
no goals
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case right
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
⊢ d.factorization ≤ (i a ha).factorization
Tactic:
rw [Finsupp.le_iff]
Proof state after:
case right
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
⊢ ∀ i_1 ∈ d.factorization.support, d.factorization i_1 ≤ (i a ha).factorization i_1
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case right
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
⊢ ∀ i_1 ∈ d.factorization.support, d.factorization i_1 ≤ (i a ha).factorization i_1
Tactic:
intro p hp
Proof state after:
case right
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.factorization.support
⊢ d.factorization p ≤ (i a ha).factorization p
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case right
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.factorization.support
⊢ d.factorization p ≤ (i a ha).factorization p
Tactic:
rw [Nat.support_factorization] at hp
Proof state after:
case right
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ d.factorization p ≤ (i a ha).factorization p
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case right
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ d.factorization p ≤ (i a ha).factorization p
Tactic:
rw [hfact_i a ha]
Proof state after:
case right
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ d.factorization p ≤ if hp : p ∈ d.primeFactors then a p hp else 0
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case right
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ d.factorization p ≤ if hp : p ∈ d.primeFactors then a p hp else 0
Tactic:
rw [dif_pos hp]
Proof state after:
case right
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ d.factorization p ≤ a p hp
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case right
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ d.factorization p ≤ a p hp
Tactic:
trans 1
Proof state after:
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ d.factorization p ≤ 1

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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ 1 ≤ a p hp
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ 1 ≤ a p hp
Tactic:
simp_rw [Finset.mem_pi, Finset.mem_Icc] at ha
Proof state after:
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
p : ℕ
hp : p ∈ d.primeFactors
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 1 ≤ a a_1 h ∧ a a_1 h ≤ M
⊢ 1 ≤ a p hp
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
p : ℕ
hp : p ∈ d.primeFactors
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 1 ≤ a a_1 h ∧ a a_1 h ≤ M
⊢ 1 ≤ a p hp
Tactic:
exact (ha p hp).1
Proof state after:
no goals
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ d.factorization p ≤ 1
Tactic:
exact hd.natFactorization_le_one p
Proof state after:
no goals