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
⊢ ∀ (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)
Tactic:
intro a 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
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
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)
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
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)
Tactic:
apply symm
Proof state after:
case a
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
⊢ f (i a ha) = ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯)
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case a
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
⊢ f (i a ha) = ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯)
Tactic:
apply hf.isMultiplicative.map_prod
Proof state after:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
⊢ (↑d.primeFactors.attach).Pairwise (Nat.Coprime on fun i => ↑i ^ a ↑i ⋯)
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
⊢ (↑d.primeFactors.attach).Pairwise (Nat.Coprime on fun i => ↑i ^ a ↑i ⋯)
Tactic:
intro x _ y _ hxy
Proof state after:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
⊢ (Nat.Coprime on fun i => ↑i ^ a ↑i ⋯) x y
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
⊢ (Nat.Coprime on fun i => ↑i ^ a ↑i ⋯) x y
Tactic:
simp_rw [Finset.mem_pi, Finset.mem_Icc, Nat.succ_le] at ha
Proof state after:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
⊢ (Nat.Coprime on fun i => ↑i ^ a ↑i ⋯) x y
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
⊢ (Nat.Coprime on fun i => ↑i ^ a ↑i ⋯) x y
Tactic:
apply (Nat.coprime_pow_left_iff (ha x x.2).1 ..).mpr
Proof state after:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
⊢ (↑x).Coprime ((fun i => ↑i ^ a ↑i ⋯) y)
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
⊢ (↑x).Coprime ((fun i => ↑i ^ a ↑i ⋯) y)
Tactic:
apply (Nat.coprime_pow_right_iff (ha y y.2).1 ..).mpr
Proof state after:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
⊢ (↑x).Coprime ↑y
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
⊢ (↑x).Coprime ↑y
Tactic:
have hxp := Nat.prime_of_mem_factors (List.mem_toFinset.mp x.2)
Proof state after:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
hxp : (↑x).Prime
⊢ (↑x).Coprime ↑y
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
hxp : (↑x).Prime
⊢ (↑x).Coprime ↑y
Tactic:
rw [Nat.Prime.coprime_iff_not_dvd hxp]
Proof state after:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
hxp : (↑x).Prime
⊢ ¬↑x ∣ ↑y
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
hxp : (↑x).Prime
⊢ ¬↑x ∣ ↑y
Tactic:
rw [Nat.prime_dvd_prime_iff_eq hxp $ Nat.prime_of_mem_factors (List.mem_toFinset.mp y.2)]
Proof state after:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
hxp : (↑x).Prime
⊢ ¬↑x = ↑y
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
case a.hs
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
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
hxp : (↑x).Prime
⊢ ¬↑x = ↑y
Tactic:
exact fun hc => hxy (Subtype.eq hc)
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
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)
⊢ ∀ (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
Tactic:
intro a ha b hb hiab
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)
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
hiab : i a ha = i b hb
⊢ a = b