Erdős problem 15

theorem target : ¬ (fcTypeOfName% "Erdos15.erdos_15") := by
  intro h
  have hS := h.mp trivial
  -- Transport the summability along the continuous ring hom `ℚ → ℝ`.
  have h1 : Summable (fun k : ℕ =>
      (((-1 : ℚ) ^ (k + 1) * (k + 1) / (k.nth Nat.Prime) : ℚ) : ℝ)) :=
    (hS.map (Rat.castHom ℝ).toAddMonoidHom Rat.continuous_coe_real).congr fun _ => rfl
  -- Over `ℝ`, `Summable` is unconditional, hence absolute.
  have h2 := h1.abs
  -- `|(-1)^(k+1) * (k+1) / p k| = (k+1)/p k ≥ 1 / p k`.
  have h3 : Summable (fun k : ℕ => (1 : ℝ) / (k.nth Nat.Prime)) := by
    refine Summable.of_nonneg_of_le (fun k => by positivity) (fun k => ?_) h2
    have hp : (0 : ℝ) < (k.nth Nat.Prime : ℝ) := by
      exact_mod_cast (Nat.prime_nth_prime k).pos
    push_cast
    rw [abs_div, abs_mul, abs_pow, abs_neg, abs_one, one_pow, one_mul,
      abs_of_nonneg hp.le, abs_of_nonneg (by positivity : (0 : ℝ) ≤ (k : ℝ) + 1)]
    gcongr
    linarith [Nat.cast_nonneg (α := ℝ) k]
  -- `k ↦ p k` is a bijection `ℕ ≃ Nat.Primes`, so this contradicts Euler's theorem
  -- that the sum of prime reciprocals diverges.
  have hinf : {p | Nat.Prime p}.Infinite := Nat.infinite_setOf_prime
  have hbij : Function.Bijective
      (fun k : ℕ => (⟨k.nth Nat.Prime, Nat.prime_nth_prime k⟩ : Nat.Primes)) := by
    refine ⟨fun a b hab => Nat.nth_injective hinf (congrArg Subtype.val hab), ?_⟩
    rintro ⟨p, hp⟩
    have hmem : p ∈ Set.range (Nat.nth Nat.Prime) := by
      rw [Nat.range_nth_of_infinite hinf]; exact hp
    obtain ⟨k, hk⟩ := hmem
    exact ⟨k, by simp [hk]⟩
  exact Nat.Primes.not_summable_one_div
    ((Equiv.ofBijective _ hbij).summable_iff.mp (by simpa [Function.comp] using h3))