theorem target : ¬ (fcTypeOfName% "Erdos726.erdos_726") := by
  intro h
  have hiff := h.mp trivial
  have hmod : ∀ (n p : ℕ), (p : ℝ) ≠ 0 → (n : ℝ) % (p : ℝ) = 0 := fun n p hp0 => by
    rw [Field.mod_eq, mul_div_assoc, div_self hp0, mul_one, sub_self]
  have hzero : (fun n : ℕ ↦ ∑ p ∈ (Finset.range (n + 1)).filter
      (fun p : ℕ ↦ p.Prime ∧ (p : ℝ) / 2 < (n % p : ℝ)), (1 : ℝ) / (p : ℝ))
      = (fun _ : ℕ ↦ (0 : ℝ)) := by
    funext n
    rw [Finset.filter_false_of_mem, Finset.sum_empty]
    rintro p - ⟨hp, hlt⟩
    have hp0 : (p : ℝ) ≠ 0 := by exact_mod_cast hp.pos.ne'
    rw [hmod n p hp0] at hlt
    have hpp : (0 : ℝ) < (p : ℝ) := by exact_mod_cast hp.pos
    linarith
  rw [hzero] at hiff
  have h1 : Filter.Tendsto (fun n : ℕ ↦ Real.log (Real.log (n : ℝ)))
      Filter.atTop Filter.atTop :=
    Real.tendsto_log_atTop.comp (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop)
  have hg : Filter.Tendsto (fun n : ℕ ↦ Real.log (Real.log (n : ℝ)) / 2)
      Filter.atTop Filter.atTop := h1.atTop_div_const (by norm_num)
  have h0 : Filter.Tendsto (fun _ : ℕ ↦ (0 : ℝ)) Filter.atTop Filter.atTop :=
    hiff.symm.tendsto_atTop hg
  exact not_tendsto_atTop_of_tendsto_nhds tendsto_const_nhds h0