awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
calc :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) =
    HAdd.hAdd (α := ℝ) (↑((2 * N₀).smoothNumbersUpTo k).card : ℝ) (↑((2 * N₀).roughNumbersUpTo k).card : ℝ)
calc₁ :
  HAdd.hAdd (α := ℝ) (↑((2 * N₀).smoothNumbersUpTo k).card : ℝ) (↑((2 * N₀).roughNumbersUpTo k).card : ℝ) ≤
    HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + (↑((2 * N₀).roughNumbersUpTo k).card : ℝ)
calc₂ :
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + (↑((2 * N₀).roughNumbersUpTo k).card : ℝ) ≤
    HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
⊢ HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S

Tactic:
calc (2 * N₀ : ℝ)
    _ = ((2 * N₀).smoothNumbersUpTo k).card + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast ((2 * N₀).smoothNumbersUpTo_card_add_roughNumbersUpTo_card k).symm
    _ ≤ m * (2 * N₀).sqrt + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast Nat.add_le_add_right ((2 * N₀).smoothNumbersUpTo_card_le k) _
    _ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S := by grw [roughNumbersUpTo_card_le']; norm_cast

Premises used: Nat.roughNumbersUpTo, HMul.hMul, Nat.sqrt, Nat.cast, Finset.card, Nat.smoothNumbersUpTo, OfNat.ofNat
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
obtain :
  ∀ (k : ℕ)
    (hk :
      ∀ t ⊆ {n : ℕ | k ≤ n},
        ∑' (n : (↑t : Type)), indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑n : ℕ) ∈
          Iio (1 / 2)),
    False
⊢ False

Tactic:
obtain ⟨k, hk⟩ := h.nat_tsum_vanishing (Iio_mem_nhds one_half_pos : Iio (1 / 2 : ℝ) ∈ 𝓝 0)

Premises used: Iio_mem_nhds, Summable.nat_tsum_vanishing, one_half_pos
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∀ t ⊆ {n : ℕ | k ≤ n},
    ∑' (n : (↑t : Type)), indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑n : ℕ) ∈
      Iio (1 / 2)
⊢ ∑' (n : (↑({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) : Type)),
      indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑n : ℕ) ∈
    Iio (1 / 2)

Tactic:
specialize hk ({p | Nat.Prime p} ∩ {p | k ≤ p}) inter_subset_right

Premises used: Nat.Prime, setOf, LE.le, Inter.inter, Set.inter_subset_right
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (n : (↑({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) : Type)),
      indicator {p : ℕ | Nat.Prime p} (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑n : ℕ) ∈
    Iio (1 / 2)
⊢ ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2

Tactic:
rw [tsum_subtype, indicator_indicator, inter_eq_left.mpr fun n hn ↦ hn.1, mem_Iio] at hk

Premises used: Set.inter_eq_left, Iff.mpr, Set.mem_Iio, tsum_subtype, Set.indicator_indicator
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
⊢ Summable (α := ℝ)
    (indicator {n : ℕ | k ≤ n} (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))

Tactic:
h.indicator {n : ℕ | k ≤ n}

Premises used: setOf, LE.le, Summable.indicator
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h₁ :
  Eq (α := ℕ → ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
    (indicator {n : ℕ | k ≤ n} (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
⊢ Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
convert! h.indicator {n : ℕ | k ≤ n} using 1

Premises used: setOf, LE.le, Summable.indicator
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
⊢ Eq (α := ℕ → ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
    (indicator {n : ℕ | k ≤ n} (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))

Tactic:
simp only [indicator_indicator, inter_comm]

Premises used: Set.inter_comm, Set.indicator_indicator
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
⊢ Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
have h' : Summable (indicator ({p | Nat.Prime p} ∩ {p | k ≤ p}) fun n ↦ (1 : ℝ) / n) := by
    convert! h.indicator {n : ℕ | k ≤ n} using 1
    simp only [indicator_indicator, inter_comm]
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ False

Tactic:
((one_half_le_sum_primes_ge_one_div k).trans_lt <| LE.le.trans_lt ?_ hk).false

Premises used: LT.lt.false, LE.le.trans_lt, one_half_le_sum_primes_ge_one_div
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
refine :
  LE.le (α := ℝ)
    (∑ p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow,
      HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
    (∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x)
⊢ False

Tactic:
refine ((one_half_le_sum_primes_ge_one_div k).trans_lt <| LE.le.trans_lt ?_ hk).false

Premises used: LT.lt.false, LE.le.trans_lt, one_half_le_sum_primes_ge_one_div
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
n : ℕ
h_1 : n ∉ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
p : ℕ
h_2 : Membership.mem (γ := Set ℕ) ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) p
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
h₁ :
  ∀ (p : ℕ) (hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow),
    HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) =
      indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) p
⊢ LE.le (α := ℝ)
    (∑ p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow,
      HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
    (∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x)

Tactic:
convert!
    Summable.sum_le_tsum (primesBelow ((4 ^ (k.primesBelow.card + 1)).succ) \ primesBelow k)
      (fun n _ ↦ indicator_nonneg (fun p _ ↦ by positivity) _) h' using
    2 with p hp

Premises used: SDiff.sdiff, Summable.sum_le_tsum, Set.indicator_nonneg, Nat.primesBelow
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
p : ℕ
hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
⊢ p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow.val

Tactic:
obtain ⟨hp₁, hp₂⟩ := mem_setOf_eq ▸ Finset.mem_sdiff.mp hp
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
p : ℕ
hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow.val
⊢ p ∉ k.primesBelow

Tactic:
obtain ⟨hp₁, hp₂⟩ := mem_setOf_eq ▸ Finset.mem_sdiff.mp hp
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
p : ℕ
hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
⊢ Nat.Prime p

Tactic:
have hpp := prime_of_mem_primesBelow hp₁
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
p : ℕ
hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) =
    indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) p

Tactic:
(indicator_of_mem ?_ fun n : ℕ ↦ (1 / n : ℝ)).symm

Premises used: HDiv.hDiv, Nat.cast, Set.indicator_of_mem, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
p : ℕ
hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
h₁ : Membership.mem (γ := Set ℕ) ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) p
⊢ HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) =
    indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) p

Tactic:
refine (indicator_of_mem ?_ fun n : ℕ ↦ (1 / n : ℝ)).symm

Premises used: HDiv.hDiv, Nat.cast, Set.indicator_of_mem, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
p : ℕ
hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ Membership.mem (γ := Set ℕ) {p : ℕ | k ≤ p} p

Tactic:
simpa [primesBelow, hpp] using hp₂

Premises used: Nat.primesBelow
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
h : Summable (α := ℝ) (indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
k : ℕ
hk :
  ∑' (x : ℕ), indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) x <
    1 / 2
h' : Summable (α := ℝ) (indicator ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
p : ℕ
hp : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (HPow.hPow (α := ℕ) 4 (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ Membership.mem (γ := Set ℕ) ({p : ℕ | Nat.Prime p} ∩ {p : ℕ | k ≤ p}) p

Tactic:
exact ⟨hpp, by simpa [primesBelow, hpp] using hp₂⟩
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
⊢ ¬Summable (α := ℝ) (β := (↑{p : ℕ | Prime p} : Type))
      ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ∘
        Subtype.val (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {p : ℕ | Prime p} x))

Tactic:
summable_subtype_iff_indicator.mp.mt not_summable_one_div_on_primes

Premises used: Function.mt, Iff.mp, summable_subtype_iff_indicator, not_summable_one_div_on_primes
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
⊢ ¬Summable (α := ℝ) fun (p : Primes) ↦ HDiv.hDiv (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)

Tactic:
convert! summable_subtype_iff_indicator.mp.mt not_summable_one_div_on_primes

Premises used: Function.mt, Iff.mp, summable_subtype_iff_indicator, not_summable_one_div_on_primes
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
r : ℝ
pos : ∀ (h : r < -1), (Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) ↔ r < -1
neg : ∀ (h : ¬r < -1), (Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) ↔ r < -1
⊢ (Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) ↔ r < -1

Tactic:
by_cases h : r < -1
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
r : ℝ
h : r < -1
pos : Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
⊢ (Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) ↔ r < -1

Tactic:
simp only [h, iff_true]

Premises used: iff_true
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
r : ℝ
h : r < -1
⊢ Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r

Tactic:
(Real.summable_nat_rpow.mpr h).subtype _

Premises used: Iff.mpr, Summable.subtype, Nat.Primes, Real.summable_nat_rpow
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
r : ℝ
h : r < -1
⊢ Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r

Tactic:
exact (Real.summable_nat_rpow.mpr h).subtype _

Premises used: Iff.mpr, Summable.subtype, Real.summable_nat_rpow
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
r : ℝ
h : ¬r < -1
neg : ¬Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
⊢ (Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) ↔ r < -1

Tactic:
simp only [h, iff_false]

Premises used: iff_false
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
r : ℝ
h : ¬r < -1
H : Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
x : Primes
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑(↑x : ℕ) : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
r : ℝ
h : ¬r < -1
neg :
  ∀ (H : Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r) (b : Primes),
    HDiv.hDiv (α := ℝ) 1 (↑(↑b : ℕ) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(↑b : ℕ) : ℝ) r
⊢ ¬Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r

Tactic:
refine fun H ↦ Nat.Primes.not_summable_one_div <| H.of_nonneg_of_le (fun _ ↦ by positivity) ?_

Premises used: Nat.Primes.not_summable_one_div
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
r : ℝ
h : ¬r < -1
H : Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
p : Primes
neg : HPow.hPow (α := ℝ) (β := ℝ) (↑(↑p : ℕ) : ℝ) (-1) ≤ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
⊢ HDiv.hDiv (α := ℝ) 1 (↑(↑p : ℕ) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r

Tactic:
rw [one_div, ← Real.rpow_neg_one]

Premises used: Real.rpow_neg_one, one_div
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
r : ℝ
h : ¬r < -1
H : Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
p : Primes
⊢ LE.le (α := ℝ) 1 (↑(↑p : ℕ) : ℝ)

Tactic:
exact_mod_cast p.prop.one_lt.le

Premises used: Nat.Prime.one_lt, LT.lt.le, Subtype.prop
-- Module: Mathlib.NumberTheory.SumPrimeReciprocals
Goal:
r : ℝ
h : ¬r < -1
H : Summable (α := ℝ) fun (p : Primes) ↦ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r
p : Primes
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑(↑p : ℕ) : ℝ) (-1) ≤ HPow.hPow (α := ℝ) (↑(↑p : ℕ) : ℝ) r

Tactic:
exact Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast p.prop.one_lt.le) <| not_lt.mp h

Premises used: not_lt, Iff.mp, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
p : ℕ
inst : Fact (Prime p)
hp : p % 4 ≠ 3
apply : ¬Irreducible (M := GaussianInt) (↑p : GaussianInt)
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = p

Tactic:
apply sq_add_sq_of_nat_prime_of_not_irreducible p

Premises used: GaussianInt.sq_add_sq_of_nat_prime_of_not_irreducible
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
p : ℕ
inst : Fact (Prime p)
hp : p % 4 ≠ 3
rwa : ¬_root_.Prime (M := GaussianInt) (↑p : GaussianInt)
rwa₁ rwa₂ rwa₃ rwa₄ : ¬p % 4 = 3
⊢ ¬Irreducible (M := GaussianInt) (↑p : GaussianInt)

Tactic:
rwa [_root_.irreducible_iff_prime, prime_iff_mod_four_eq_three_of_nat_prime p]

Premises used: irreducible_iff_prime, GaussianInt.prime_iff_mod_four_eq_three_of_nat_prime
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
R : Type u_1
inst : CommRing R
a b x y u v : R
ha : a = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hb : b = HPow.hPow (β := ℕ) u 2 + HPow.hPow (β := ℕ) v 2
rw :
  (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) * (HPow.hPow (β := ℕ) u 2 + HPow.hPow (β := ℕ) v 2) =
    HPow.hPow (β := ℕ) (x * u - y * v) 2 + HPow.hPow (β := ℕ) (x * v + y * u) 2
⊢ a * b = HPow.hPow (β := ℕ) (x * u - y * v) 2 + HPow.hPow (β := ℕ) (x * v + y * u) 2

Tactic:
rw [ha, hb]
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
R : Type u_1
inst : CommRing R
a b x y u v : R
ha : a = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hb : b = HPow.hPow (β := ℕ) u 2 + HPow.hPow (β := ℕ) v 2
⊢ (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) * (HPow.hPow (β := ℕ) u 2 + HPow.hPow (β := ℕ) v 2) =
    HPow.hPow (β := ℕ) (x * u - y * v) 2 + HPow.hPow (β := ℕ) (x * v + y * u) 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
a b x y u v : ℕ
ha : a = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hb : b = HPow.hPow (β := ℕ) u 2 + HPow.hPow (β := ℕ) v 2
zify :
  ∀ (ha : (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2)
    (hb : (↑b : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑u : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑v : ℤ) 2),
    ∃ (r : ℕ) (s : ℕ),
      HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
        HPow.hPow (α := ℤ) (β := ℕ) (↑r : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑s : ℤ) 2
⊢ ∃ (r : ℕ) (s : ℕ), a * b = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2

Tactic:
zify at ha hb ⊢
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
a b x y u v : ℕ
ha : (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2
hb : (↑b : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑u : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑v : ℤ) 2
obtain :
  ∀ (r s : ℤ) (h : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2),
    ∃ (r : ℕ) (s : ℕ),
      HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
        HPow.hPow (α := ℤ) (β := ℕ) (↑r : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑s : ℤ) 2
⊢ ∃ (r : ℕ) (s : ℕ),
    HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑r : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑s : ℤ) 2

Tactic:
obtain ⟨r, s, h⟩ := _root_.sq_add_sq_mul ha hb

Premises used: sq_add_sq_mul
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
a b x y u v : ℕ
ha : (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2
hb : (↑b : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑u : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑v : ℤ) 2
r s : ℤ
h : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
⊢ ∃ (r : ℕ) (s : ℕ),
    HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑r : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑s : ℤ) 2

Tactic:
⟨r.natAbs, s.natAbs, ?_⟩

Premises used: Int.natAbs, Exists.intro
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
a b x y u v : ℕ
ha : (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2
hb : (↑b : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑u : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑v : ℤ) 2
r s : ℤ
h : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
refine :
  HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑r.natAbs : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑s.natAbs : ℤ) 2
⊢ ∃ (r : ℕ) (s : ℕ),
    HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
      HPow.hPow (α := ℤ) (β := ℕ) (↑r : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑s : ℤ) 2

Tactic:
refine ⟨r.natAbs, s.natAbs, ?_⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
a b x y u v : ℕ
ha : (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2
hb : (↑b : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑u : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑v : ℤ) 2
r s : ℤ
h : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) s 2
⊢ HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑r.natAbs : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑s.natAbs : ℤ) 2

Tactic:
simpa only [Int.natCast_natAbs, sq_abs]

Premises used: sq_abs, Int.natCast_natAbs
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
m n : ℕ
hd : m ∣ n
hs : IsSquare (α := ZMod n) (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
rw : IsSquare (α := ZMod m) ((f : (a : ZMod n) → ZMod m) (-1))
⊢ IsSquare (α := ZMod m) (-1)

Tactic:
rw [← map_one f, ← map_neg]

Premises used: map_neg, map_one
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
m n : ℕ
hd : m ∣ n
hs : IsSquare (α := ZMod n) (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (α := ZMod m) ((f : (a : ZMod n) → ZMod m) (-1))

Tactic:
hs.map f

Premises used: IsSquare.map