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
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)
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m
Tactic:
have i_inj : ∀ a ha b hb, i a ha = i b hb → a = b := by
  intro a ha b hb hiab
  apply_fun Nat.factorization at hiab
  ext p hp
  obtain hiabp := DFunLike.ext_iff.mp hiab p
  rw [hfact_i a ha, hfact_i b hb, dif_pos hp, dif_pos hp] at hiabp
  exact hiabp
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
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
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m
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
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
i_surj :
  ∀ b ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors,
    ∃ a, ∃ (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M), i a ha = b
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m
Tactic:
exact Finset.sum_bij i hi i_inj i_surj h
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 ⋯
⊢ ∀ (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
Tactic:
intro a ha p
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 ⋯
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
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 ⋯
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
Tactic:
by_cases hp : p ∈ d.primeFactors
Proof state after:
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0

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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∉ d.primeFactors
⊢ (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
Tactic:
rw [dif_pos hp, Nat.factorization_prod, Finset.sum_apply',
  Finset.sum_eq_single ⟨p, hp⟩, Nat.factorization_pow, Finsupp.smul_apply,
  Nat.Prime.factorization_self (Nat.prime_of_mem_factors $ List.mem_toFinset.mp hp)]
Proof state after:
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ a ↑⟨p, hp⟩ ⋯ • 1 = a p hp

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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ ∀ b ∈ d.primeFactors.attach, b ≠ ⟨p, hp⟩ → (↑b ^ a ↑b ⋯).factorization p = 0

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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ ⟨p, hp⟩ ∉ d.primeFactors.attach → (↑⟨p, hp⟩ ^ a ↑⟨p, hp⟩ ⋯).factorization p = 0

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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ ∀ x ∈ d.primeFactors.attach, ↑x ^ a ↑x ⋯ ≠ 0
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ a ↑⟨p, hp⟩ ⋯ • 1 = a p hp
Tactic:
ring
Proof state after:
no goals
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
⊢ ∀ b ∈ d.primeFactors.attach, b ≠ ⟨p, hp⟩ → (↑b ^ a ↑b ⋯).factorization p = 0
Tactic:
intro q _ hq
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ (↑q ^ a ↑q ⋯).factorization p = 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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ (↑q ^ a ↑q ⋯).factorization p = 0
Tactic:
rw [Nat.factorization_pow, Finsupp.smul_apply, smul_eq_zero]
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ a ↑q ⋯ = 0 ∨ (↑q).factorization p = 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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ a ↑q ⋯ = 0 ∨ (↑q).factorization p = 0
Tactic:
right
Proof state after:
case pos.h₀.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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ (↑q).factorization p = 0
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case pos.h₀.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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ (↑q).factorization p = 0
Tactic:
apply Nat.factorization_eq_zero_of_not_dvd
Proof state after:
case pos.h₀.h.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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ ¬p ∣ ↑q
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case pos.h₀.h.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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ ¬p ∣ ↑q
Tactic:
rw [Nat.Prime.dvd_iff_eq, ← exists_eq_subtype_mk_iff]
Proof state after:
case pos.h₀.h.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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ ¬∃ (h : p ∈ d.primeFactors), q = ⟨p, h⟩

case pos.h₀.h.h.hp
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ (↑q).Prime

case pos.h₀.h.h.a1
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ p ≠ 1
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case pos.h₀.h.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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ ¬∃ (h : p ∈ d.primeFactors), q = ⟨p, h⟩

case pos.h₀.h.h.hp
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ (↑q).Prime

case pos.h₀.h.h.a1
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ p ≠ 1
Tactic:
push_neg
Proof state after:
case pos.h₀.h.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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ ∀ (h : p ∈ d.primeFactors), q ≠ ⟨p, h⟩

case pos.h₀.h.h.hp
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ (↑q).Prime

case pos.h₀.h.h.a1
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ p ≠ 1
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case pos.h₀.h.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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ ∀ (h : p ∈ d.primeFactors), q ≠ ⟨p, h⟩

case pos.h₀.h.h.hp
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ (↑q).Prime

case pos.h₀.h.h.a1
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ p ≠ 1
Tactic:
exact fun _ => hq
Proof state after:
case pos.h₀.h.h.hp
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ (↑q).Prime

case pos.h₀.h.h.a1
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ p ≠ 1
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case pos.h₀.h.h.hp
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ (↑q).Prime

case pos.h₀.h.h.a1
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ p ≠ 1
Tactic:
exact Nat.prime_of_mem_factors $ List.mem_toFinset.mp q.2
Proof state after:
case pos.h₀.h.h.a1
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ p ≠ 1
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case pos.h₀.h.h.a1
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 ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∈ d.primeFactors
q : { x // x ∈ d.primeFactors }
a✝ : q ∈ d.primeFactors.attach
hq : q ≠ ⟨p, hp⟩
⊢ p ≠ 1
Tactic:
exact (Nat.prime_of_mem_factors $ List.mem_toFinset.mp hp).ne_one
Proof state after:
no goals