-- Mathlib/NumberTheory/SumPrimeReciprocals.lean
theorem not_summable_one_div_on_primes :
    ¬ Summable (indicator {p | p.Prime} (fun n : ℕ ↦ (1 : ℝ) / n))

Proof state:
case intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (n : ↑({p | Nat.Prime p} ∩ {p | k ≤ p})), {p | Nat.Prime p}.indicator (fun n => 1 / ↑n) ↑n ∈ Iio (1 / 2)
⊢ False

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

Result:
case intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
⊢ False

Proof state:
case h.e'_3.a.intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
⊢ 1 / ↑p = ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) p

Tactic:
have hpp := prime_of_mem_primesBelow hp₁

Result:
case h.e'_3.a.intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ 1 / ↑p = ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) p

Proof state:
case intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
⊢ False

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

Result:
case intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
⊢ ∑ p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow, 1 / ↑p ≤
    ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x

Proof state:
case h.e'_3.a.intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ p ∈ {p | k ≤ p}

Tactic:
exact not_lt.mp <| (not_and_or.mp <| (not_congr mem_primesBelow).mp hp₂).neg_resolve_right hpp

Result:
no goals

Proof state:
⊢ ¬Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)

Tactic:
intro h

Result:
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
⊢ False

Proof state:
case h.e'_3.a.intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ 1 / ↑p = ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) p

Tactic:
refine (indicator_of_mem (mem_def.mpr ⟨hpp, ?_⟩) fun n : ℕ ↦ (1 / n : ℝ)).symm

Result:
case h.e'_3.a.intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ p ∈ {p | k ≤ p}

Proof state:
case intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
⊢ False

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]

Result:
case intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
⊢ False

Proof state:
case h.e'_5
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
⊢ (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n) =
    {n | k ≤ n}.indicator ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)

Tactic:
simp only [indicator_indicator, inter_comm]

Result:
no goals

Proof state:
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
n : ℕ
x✝¹ : n ∉ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
p : ℕ
x✝ : p ∈ {p | Nat.Prime p} ∩ {p | k ≤ p}
⊢ 0 ≤ 1 / ↑p

Tactic:
positivity

Result:
no goals

Proof state:
case h.e'_3.a
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
⊢ 1 / ↑p = ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) p

Tactic:
obtain ⟨hp₁, hp₂⟩ := mem_setOf_eq ▸ Finset.mem_sdiff.mp hp

Result:
case h.e'_3.a.intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
⊢ 1 / ↑p = ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) p

Proof state:
case intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
⊢ ∑ p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow, 1 / ↑p ≤
    ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x

Tactic:
convert 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

Result:
case h.e'_3.a
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
⊢ 1 / ↑p = ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) p