awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
k : ℤ
n : ℕ
zero :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k 0) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k 0 : S)
one :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k 1) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k 1 : S)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k n) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k n : S)
have even : ∀ (m : ℕ)
  (ih :
    ∀ k_1 < 2 * (m + 1),
      Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k k_1) : S)
        (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k k_1 : S)),
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k (2 * (m + 1))) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (2 * (m + 1)) : S)
Tactic: induction n using complEDSRec' with
  | zero => simp
  | one => simp
  | _ _ ih =>
    simp only [complEDS'_even, complEDS'_odd, map_normEDS, map_complEDS₂, map_pow, map_mul, map_sub]
    repeat rw [ih _ <| by linarith only]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
k : ℤ
n : ℕ
zero :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k 0) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k 0 : S)
one :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k 1) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k 1 : S)
even :
  ∀ (m : ℕ)
    (ih :
      ∀ k_1 < 2 * (m + 1),
        Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k k_1) : S)
          (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k k_1 : S)),
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k (2 * (m + 1))) : S)
      (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (2 * (m + 1)) : S)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k n) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k n : S)
have odd : ∀ (m : ℕ)
  (ih :
    ∀ k_1 < 2 * (m + 1) + 1,
      Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k k_1) : S)
        (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k k_1 : S)),
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k (2 * (m + 1) + 1)) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (2 * (m + 1) + 1) : S)
Tactic: induction n using complEDSRec' with
  | zero => simp
  | one => simp
  | _ _ ih =>
    simp only [complEDS'_even, complEDS'_odd, map_normEDS, map_complEDS₂, map_pow, map_mul, map_sub]
    repeat rw [ih _ <| by linarith only]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
F : Type u_1
inst : NormedDivisionRing F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
p : ℕ
hp : 1 < p
⊢ norm (E := F) ((f : (a : ℕ) → F) p : F) < 1
have refine : Summable.{u_1, 0} (α := F) fun (n : ℕ) ↦ HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n
Tactic: refine summable_geometric_iff_norm_lt_one.mp ?_
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
F : Type u_1
inst : NormedDivisionRing F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
p : ℕ
hp : 1 < p
⊢ Summable.{u_1, 0} (α := F) fun (n : ℕ) ↦ HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n
have simp_rw : Summable.{u_1, 0} (α := F) fun (n : ℕ) ↦ (f : (a : ℕ) → F) (p ^ n)
Tactic: simp_rw [← map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers ∅) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers ∅) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ ∅ with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
have empty : (Summable (α := ℝ) fun (m : (↑{1} : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
  HasSum.{u_1, 0} (α := R) (fun (m : (↑{1} : Type)) ↦ f (↑m : ℕ)) (∏ p ∈ ∅ with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
Tactic: rw [factoredNumbers_empty]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
⊢ (Summable (α := ℝ) fun (m : (↑{1} : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑{1} : Type)) ↦ f (↑m : ℕ)) (∏ p ∈ ∅ with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
have empty : (Summable (α := ℝ) fun (m : (↑{1} : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
  HasSum.{u_1, 0} (α := R) (fun (m : (↑{1} : Type)) ↦ f (↑m : ℕ)) 1
Tactic: simp only [notMem_empty, IsEmpty.forall_iff, forall_const, filter_true_of_mem, prod_empty]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ insert p s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
have insert : (Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
  HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
    (∏ p ∈ if Nat.Prime p then insert p ({p ∈ s | Nat.Prime p}) else {p ∈ s | Nat.Prime p}, ∑' (n : ℕ), f (p ^ n))
Tactic: rw [filter_insert]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ if Nat.Prime p then insert p ({p ∈ s | Nat.Prime p}) else {p ∈ s | Nat.Prime p}, ∑' (n : ℕ), f (p ^ n))
have pos : ∀ (hpp : Nat.Prime p),
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
      (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))
Tactic: split_ifs with hpp
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
pos :
  ∀ (hpp : Nat.Prime p),
    (Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
      HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
        (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ if Nat.Prime p then insert p ({p ∈ s | Nat.Prime p}) else {p ∈ s | Nat.Prime p}, ∑' (n : ℕ), f (p ^ n))
have neg : ∀ (hpp : ¬Nat.Prime p),
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
      (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n))
Tactic: split_ifs with hpp
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
      (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))
have pos : Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
pos : Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
      (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))
have pos₁ : HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
  (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖
have pos : Summable (α := ℝ) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ ‖f (p ^ x.1) * f (↑x.2 : ℕ)‖
Tactic: simp only [← (equivProdNatFactoredNumbers hpp hp).summable_iff, Function.comp_def,
          equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ Summable (α := ℝ) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ ‖f (p ^ x.1) * f (↑x.2 : ℕ)‖
have pos : Summable (α := ℝ) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ ‖f (p ^ x.1)‖ * ‖f (↑x.2 : ℕ)‖
Tactic: refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_mul_le ..) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ Summable (α := ℝ) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ ‖f (p ^ x.1)‖ * ‖f (↑x.2 : ℕ)‖
have pos : LE.le (α := ℕ → ℝ) 0 fun (n : ℕ) ↦ ‖f (p ^ n)‖
Tactic: apply Summable.mul_of_nonneg (hsum hpp) ih.1
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
pos : LE.le (α := ℕ → ℝ) 0 fun (n : ℕ) ↦ ‖f (p ^ n)‖
⊢ Summable (α := ℝ) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ ‖f (p ^ x.1)‖ * ‖f (↑x.2 : ℕ)‖
have pos₁ : LE.le (α := (↑(factoredNumbers s) : Type) → ℝ) 0 fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖
Tactic: apply Summable.mul_of_nonneg (hsum hpp) ih.1
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
    (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))
have hp' : p ∉ {p ∈ s | Nat.Prime p}
Tactic: have hp' : p ∉ {p ∈ s | p.Prime} := mt (mem_of_mem_filter p) hp
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
⊢ HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
    (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))
have pos : HasSum
  (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦
    f
      (↑((equivProdNatFactoredNumbers hpp hp :
              (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
            x) :
        ℕ))
  (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))
Tactic: rw [prod_insert hp', ← (equivProdNatFactoredNumbers hpp hp).hasSum_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
| HasSum
    (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦
      f
        (↑((equivProdNatFactoredNumbers hpp hp :
                (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
              x) :
          ℕ))
    (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))
have h : ∀ (x : ℕ × (↑(factoredNumbers s) : Type)),
  f
    (↑((equivProdNatFactoredNumbers hpp hp :
            (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
          x) :
      ℕ)
Tactic: enter [1, x]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
x : ℕ × (↑(factoredNumbers s) : Type)
| f
    (↑((equivProdNatFactoredNumbers hpp hp :
            (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
          x) :
      ℕ)
have h : f (p ^ x.1) * f (↑x.2 : ℕ)
Tactic: rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
| HasSum
    (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦
      f
        (↑((equivProdNatFactoredNumbers hpp hp :
                (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
              x) :
          ℕ))
    (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))
have h : ∀ (x : ℕ × (↑(factoredNumbers s) : Type)), f (p ^ x.1) * f (↑x.2 : ℕ)
Tactic: enter [1, x]
          rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
⊢ HasSum
    (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦
      f
        (↑((equivProdNatFactoredNumbers hpp hp :
                (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
              x) :
          ℕ))
    (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))
have pos : HasSum (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ f (p ^ x.1) * f (↑x.2 : ℕ))
  (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))
Tactic: conv =>
          enter [1, x]
          rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
⊢ HasSum (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ f (p ^ x.1) * f (↑x.2 : ℕ))
    (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))
have this : T3Space R
Tactic: have : T3Space R := instT3Space
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
this : T3Space R
⊢ HasSum (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ f (p ^ x.1) * f (↑x.2 : ℕ))
    (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))
have pos : Summable.{u_1, 0} (α := R) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ f (p ^ x.1) * f (↑x.2 : ℕ)
Tactic: apply (hsum hpp).of_norm.hasSum.mul ih.2