Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case 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 ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
⊢ i (fun p x => b.factorization p) h = b
Tactic:
apply Nat.eq_of_factorization_eq
Proof state after:
case h.ha
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 ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
⊢ i (fun p x => b.factorization p) h ≠ 0

case h.hb
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 ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
⊢ b ≠ 0

case 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 ⋯
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 ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h : (fun p x => b.factorization p) ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
⊢ ∀ (p : ℕ), (i (fun p x => b.factorization p) h).factorization p = b.factorization p