theorem81.lean

/-
Copyright (c) 2021 Vladimir Goryachev, Stepan Nesterov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Vladimir Goryachev, Stepan Nesterov
-/

import data.nat.prime
import topology.algebra.infinite_sum
import algebra.squarefree
import ring_theory.unique_factorization_domain
import data.multiset.basic
import data.nat.parity
import algebra.associated
import data.pnat.factors
import algebra.big_operators.basic

open finset
open order
open_locale classical
open_locale big_operators

def nextprime (n : ℕ) : ℕ := nat.find (nat.exists_infinite_primes n)

def primecount : ℕ → ℕ
| 0 := 2
| (n + 1) := nextprime ((primecount n).succ)

def firstprimes : ℕ → set ℕ := λ n, {p : ℕ | ∃ k : ℕ, p = primecount k ∧ k ≤ n}

noncomputable def primerec : ℕ → ℝ := λ n, 1/(primecount n)

noncomputable def primerec_shift : ℕ → ℕ → ℝ := λ m, λ n, 1/(primecount m+n)

def add_inj : ℕ → ℕ ↪ ℕ := 
begin
  intro n,
  split,
  have h: function.injective (λ m, m + n),
  {
    rw function.injective,
    intros k t H,
    exact (add_left_inj n).mp H
  },
  exact h,
end

def primes : ℕ → finset ℕ :=
λ n, filter nat.prime (range (primecount n))

noncomputable def smooth_numbers : ℕ → ℕ → finset ℕ := 
λ n, λ x, filter (λ y, (∀ p : ℕ, nat.prime p → p ∣ y → p < primecount n )) (range x) --{y : ℕ | y ≤ x ∧ (∀ p : ℕ, p ∈ factors y → p ≤ primecount n )}

def set_of_multiples (n x : ℕ) : finset ℕ := finset.filter (λ y, (primecount n)∣y ∧ 0 < y) (range x)

def number_of_prime (p : ℕ) : ℕ := (finset.filter nat.prime (range p)).card

lemma picking_a_cutoff (H : summable primerec) : (∃ n : ℕ, ∑' (i : ℕ), primerec (i + n) < 1/2) :=
begin
  have H' := summable.has_sum H,
  have ha1 := has_sum.tendsto_sum_nat H',
  rw metric.tendsto_at_top at ha1,
  specialize ha1 (1/2),
  have f : 1/2 > (0:ℝ) := by linarith,
  specialize ha1 f,
  cases ha1 with n hn,
  specialize hn n (le_refl n),
  dsimp at hn,
  have H := sum_add_tsum_nat_add n H,
  dsimp at H,
  use n,
  rw real.dist_eq at hn,
  rw abs_lt at hn,
  linarith,
end

lemma ind_prime: ∀ n k : ℕ, (nat.prime n) → (n < primecount k.succ) → (n ≤ primecount k) :=
begin
  intros p k hp psmall,
  set q := primecount k.succ with defq,
  rw primecount at defq,
  erw nat.find_eq_iff at defq,
  cases defq with hOrd hneg,
  cases hOrd with hOrd hprime,
  simp at *,
  rw <- primecount at *,
  by_contra,
  apply hneg,
    exact psmall,
  {
    apply le_of_not_lt,
    rw nat.lt_succ_iff,
    exact h,
  },
    exact hp,
end

lemma ord_primes {k: ℕ}: primecount k < primecount k.succ :=
begin
  set q := primecount k.succ with defq,
  rw primecount at defq,
  erw nat.find_eq_iff at defq,
  cases defq with left,
  cases left with hle,
  rw ← nat.succ_le_iff,
  exact hle,
end

lemma primecount_prime: ∀ k : ℕ, nat.prime (primecount k)
| 0 := 
begin
  rw primecount,
  norm_num,
end
|(nat.succ k) :=
begin
  set q := primecount k.succ with defq,
  rw primecount at defq,
  erw nat.find_eq_iff at defq,
  cases defq with left,
  cases left with left hprime,
  exact hprime,
end

lemma primes_succ {k : ℕ}: primes (k.succ) = primes k ∪ {primecount k} :=
begin
  ext x,
  rw primes,
  simp,
  split,
  {
    intro h,
    cases h with xsmall xpr,
    by_cases hxbig: x = primecount k,
    {
      right,
      exact hxbig,
    },
    {
      left,
      split,
      {
        
        refine (ne.le_iff_lt hxbig).mp _,
        apply ind_prime,
          exact xpr,
          exact xsmall,
      },
      exact xpr,
    }
  },
  {
    intro h,
    cases h with xsmall xbig,
    {
      cases xsmall with xsmall xprime,
      split,
      {
        apply trans,
        {
          exact xsmall,
        },
        {
          rw primecount,
          apply ord_primes,
        }
      },
      {
        exact xprime,
      },
    },
    rw xbig,
    split,
      apply ord_primes,
      apply primecount_prime,
  }
end

lemma prime_image_succ{k : ℕ}: image primecount (range k.succ) = image primecount (range k) ∪ {primecount k} :=
begin
  ext n,
  split,
  {
    simp,
    intros m msmall hpmn,
    rw nat.lt_succ_iff at msmall,
    rw le_iff_eq_or_lt at msmall,
    cases msmall,
    {
      right,
      rw ← msmall,
      tauto,
    },
    {
      left,
      use m,
      split,
        exact msmall,
        exact hpmn,
    }
  },
  {
    simp,
    intro h,
    cases h,
    {
      cases h with m h,
      use m,
      cases h with msmall hpmn,
      split,
      {
        apply trans,
          exact msmall,
          exact lt_add_one k,
      },
        exact hpmn,
    },
    {
      use k,
      split,
        exact lt_add_one k,
        tauto,
    }
  }
end

lemma primecount_exhaust': ∀ n : ℕ, primes n = image primecount (range n)
| 0 :=
begin
  rw primes,
  simp,
  have p02: primecount 0 = 2 := by refl,
  rw p02,
  rw range,
  rw finset.filter,
  ext x,
  simp,
  intro x01,
  intro xpr,
  cases xpr with xbig,
  cases x01,
  {
    rw x01 at xbig,
    have h12: 1 < 2 := by norm_num,
    linarith,
  },
  {
    rw x01 at xbig,
    have h02: 0 < 2 := by norm_num,
    linarith,
  }
end
|(nat.succ k) := 
begin
  rw primes_succ,
  rw prime_image_succ,
  rw primecount_exhaust',
end

lemma primecount_exhaust (n : ℕ) : (primes n = image primecount (range n)) :=
begin
  apply primecount_exhaust',
end

lemma getting_the_index: ∀ n : ℕ, number_of_prime (primecount n) = n
| 0 :=
begin
  rw number_of_prime,
  rw primecount,
  simp,
  ext a,
  split,
  {
    simp,
    rw nat.prime,
    simp,
    intros ha2 h2a h,
    linarith,
  },
    simp,
end
| (m + 1) :=
begin
  rw number_of_prime,
  have hstep: filter nat.prime (range (primecount (m + 1))) = insert (primecount m) (filter nat.prime (range (primecount m))),
  {
    ext p,
    simp,
    split,
    {
      intro h,
      cases h with hple hpp,
      by_cases hpm: p = primecount m,
      {
        left,
        exact hpm,
      },
      {
        right,
        split,
        {
          have hle: p ≤ primecount m,
          {
            apply ind_prime,
              exact hpp,
              apply hple,
          },
          exact (ne.le_iff_lt hpm).mp hle,
        },
        exact hpp,
      },
    },
    {
      intro h,
      cases h,
      {
        rw h,
        split,
          apply ord_primes,
          apply primecount_prime,
      },
      {
        cases h with hpm hpp,
        split,
        {
          apply lt_trans,
            exact hpm,
            apply ord_primes,
        },
          exact hpp,
      },
    },
  },
  have hh: (filter nat.prime (range (primecount (m + 1)))).card = (filter nat.prime (range (primecount m))).card + 1,
  {
    rw hstep,
    apply card_insert_of_not_mem,
    simp,
  },
  rw hh,
  simp,
  rw ← number_of_prime,
  apply getting_the_index,
end


lemma n_of_prime_str_monotone {p q: ℕ} (hp: nat.prime p) (hq: nat.prime q) (hlt: p < q) : number_of_prime p < number_of_prime q :=
begin
  rw number_of_prime,
  rw number_of_prime,
  apply card_lt_card,
  split,
  {
    intro a,
    simp,
    intros hap hprime,
    split,
      apply lt_trans hap hlt,
      exact hprime,
  },
  {
    rw subset_iff,
    simp,
    use p,
    split,
      exact hlt,
    split,
      exact hp,
      simp,
  },
end

lemma n_of_prime_injective {p q: ℕ} (hp: nat.prime p) (hq: nat.prime q) (hpq: number_of_prime p = number_of_prime q): p = q :=
begin
  by_contra,
  have hneq: p < q ∨ q < p := ne.lt_or_lt h,
  cases hneq,
  {
    have hlt: number_of_prime p < number_of_prime q := by apply n_of_prime_str_monotone hp hq hneq,
    linarith,
  },
  {
    have hlt: number_of_prime q < number_of_prime p := by apply n_of_prime_str_monotone hq hp hneq,
    linarith,
  },
end

lemma primecount_every {p : ℕ} (hp: nat.prime p): primecount (number_of_prime p) = p:=
begin
  have h: number_of_prime (primecount (number_of_prime p)) = number_of_prime p := by apply getting_the_index,
  apply n_of_prime_injective,
    apply primecount_prime,
    exact hp,
    exact h,
end

lemma n_of_prime_monotone {p q: ℕ} (hp: nat.prime p) (hq: nat.prime q) (hle: p ≤ q) : number_of_prime p ≤ number_of_prime q :=
begin
  rw number_of_prime,
  rw number_of_prime,
  apply card_le_of_subset,
  intro a,
  simp,
  intros hap hprime,
  split,
    apply lt_of_lt_of_le hap hle,
    exact hprime,
end

lemma n_of_prime_monotone_reverse {p q: ℕ} (hp: nat.prime p) (hq: nat.prime q) (hle: number_of_prime p ≤ number_of_prime q) : p ≤ q :=
begin
  by_contra,
  simp at h,
  have hnlt: ¬ number_of_prime q < number_of_prime p := by linarith,
  apply hnlt,
  apply n_of_prime_str_monotone hq hp h,
end

lemma primecount_monotone {m n: ℕ} (h: m ≤ n): primecount m ≤ primecount n :=
begin
  have hp: number_of_prime (primecount m) ≤ number_of_prime (primecount n),
  {
    rw getting_the_index,
    rw getting_the_index,
    exact h,
  },
  apply n_of_prime_monotone_reverse,
    apply primecount_prime,
    apply primecount_prime,
    exact hp,
end

lemma index_le_prime {p: ℕ} (hp: nat.prime p): number_of_prime p ≤ p :=
begin
  rw number_of_prime,
  have h := card_filter_le,
  specialize h (range p),
  specialize h nat.prime,
  convert h,
  simp,
end

lemma not_smooth_zero {n x : ℕ}: 0 ∉ smooth_numbers n x :=
begin
  rw smooth_numbers,
  simp,
  intro h,
  use primecount (n.succ),
  split,
    apply primecount_prime,
    {
      apply has_lt.lt.le,
      apply ord_primes,
    }
end

lemma smooth_not_zero {n x m: ℕ} : m ∈ smooth_numbers n x → ¬ m = 0 :=
begin
  intros h hm0,
  rw hm0 at h,
  have hn := not_smooth_zero,
  apply hn,
  exact h,
end

lemma factor_smooth {a b n x: ℕ } (hba: a ∣ b) (hs: b ∈ smooth_numbers n x): a ∈ smooth_numbers n x :=
begin
  have hb0 : ¬ b = 0 := smooth_not_zero hs,
  rw smooth_numbers at *,
  simp at *,
  cases hs with hbx hp,
  split,
  {
    cases hba with k hba,
    rw hba at hbx hb0,
    have hk0 : ¬ k = 0 := not.imp hb0 (congr_arg (λ (k : ℕ), a * k)),
    have hk1 : 1 ≤ k := nat.pos_of_ne_zero hk0,
    rw ← not_le,
    intro hxa,
    have hxka : 1 * x ≤ k * a := mul_le_mul' hk1 hxa,
    simp at hxka,
    linarith,
  },
  {
    intros p hprime hpa,
    apply hp,
      exact hprime,
      exact dvd.trans hpa hba,
  }
end

lemma Sup_mem {s : set ℕ} (h1 : s.nonempty) (h2 : ∃ n, ∀ a ∈ s, a ≤ n) : Sup s ∈ s :=
begin
  rw [nat.Sup_def h2],
  rcases h1 with ⟨n, hn⟩,
  cases h : nat.find h2 with m,
  { convert hn, rw [eq_comm, ← nonpos_iff_eq_zero], convert nat.find_spec h2 n hn, rw h },
  { by_contra h',
    apply nat.find_min h2 ((nat.lt_succ_self m).trans_le h.ge),
    intros k hk,
    rw [← nat.lt_succ_iff], rw [← h] at *,
    exact lt_of_le_of_ne (nat.find_spec h2 k hk) (mt (by { rintro rfl, exact hk }) h') }
end

noncomputable def max_sq : ℕ → ℕ := 
begin
  intro n,
  by_cases h : n = 0,
    exact 1,
    exact Sup{b : ℕ | (b^2 ∣ n)}
end

noncomputable def sep_primes : ℕ → ℕ := λ n, n / (max_sq n)^2


lemma max_sq' {n : ℕ} (h : ¬ n = 0): max_sq n = Sup{b : ℕ | (b^2 ∣ n)} :=
begin
  rw max_sq,
  simp,
  intro hnot,
  rw hnot at h,
  simp at h,
  by_contra hsup,
  exact h,
end

lemma bdd_sq_div {n : ℕ} (h: ¬ n = 0): ∃ (m : ℕ), ∀ (a : ℕ), a ∈ {b : ℕ | b ^ 2 ∣ n} → a ≤ m :=
begin
  use n,
  intros a ha,
  simp at ha,
  by_contra hna,
  apply nat.not_dvd_of_pos_of_lt,
  {
    rw zero_lt_iff,
    exact h,
  },
  {
    rw ← not_le,
    exact hna,
  },
  {
    cases ha with k ha,
    use a*k,
    rw ha,
    ring,
  }
end

lemma max_sq_non_zero {n : ℕ} : ¬ max_sq n = 0 :=
begin
  by_cases n = 0,
  {
    rw max_sq,
    rw h,
    simp,
  },
  {
    rw max_sq' h,
    intro hSup,
    have h10 : 1 ≤ 0,
    {
      rw ← hSup,
      apply le_cSup,
      {
        rw bdd_above,
        rw upper_bounds,
        apply bdd_sq_div h,
      },
      {
        simp,
      },
    },
    simp at h10,
    exact h10,
  }
end

lemma max_sq_divs {n : ℕ} : ((max_sq n)^2) ∣ n :=
begin
  have ans : max_sq n ∈ {b : ℕ | (b^2 ∣ n)},
  {
    by_cases h: n = 0,
    {
      rw h,
      simp,
    },
    {
      have hn: max_sq n = Sup{b : ℕ | (b^2 ∣ n)} := by apply max_sq' h,
      rw hn,
      apply Sup_mem,
      {
        use 1,
        simp,
      },
      {
        apply bdd_sq_div h,
      }
    }
  },
  simp at ans,
  exact ans,
end

lemma sq_sep {n : ℕ} : n = (sep_primes n) * (max_sq n)^2 :=
begin
  rw sep_primes,
  simp,
  apply nat.eq_mul_of_div_eq_left,
    exact max_sq_divs,
    refl,
end

lemma sep_divs {n : ℕ} : sep_primes n ∣ n :=
begin
  use (max_sq n)^2,
  exact sq_sep,
end

lemma sq_free {n: ℕ} (hn: ¬ n = 0): squarefree (sep_primes n) :=
begin
  rw squarefree,
  intros x hxn,
  rw nat.is_unit_iff,
  cases hxn with k hxn,
  have hmax: (max_sq n) * x ∈ {b : ℕ | (b^2 ∣ n)},
  {
    simp,
    use k,
    have h := sq_sep,
    rw hxn at h,
    apply eq.trans,
      exact h,
    {
      rw sq,
      rw sq,
      ring,
    }
  },
  have hmaxn: max_sq n = Sup{b : ℕ | (b^2 ∣ n)} := by apply max_sq' hn,
  have hmaxx: (max_sq n) * x ≤ max_sq n,
  {
    rw max_sq' hn,
    apply le_cSup,
    {
      rw bdd_above,
      rw upper_bounds,
      apply bdd_sq_div hn,
    },
    {
      rw ← max_sq' hn,
      exact hmax,
    },
  },
  have hx1: x ≤ 1,
  {
    by_contra,
    rw not_le at h,
    rw ← not_lt at hmaxx,
    apply hmaxx,
    have hmm : max_sq n ≤ max_sq n := by refl,
    have h1mx: (max_sq n) * 1 < (max_sq n) * x,
    {
      refine nat.mul_lt_mul' hmm h _,
      rw zero_lt_iff,
      exact max_sq_non_zero,
    },
    convert h1mx,
    simp,
  },
  have hx0: ¬ x = 0,
  {
    by_contra,
    rw h at hxn,
    simp at hxn,
    have hss := sq_sep,
    rw hxn at hss,
    simp at hss,
    apply hn,
    exact hss,
  },
  have hx0: x ≠ 0 := by tauto,
  rw ← zero_lt_iff at hx0,
  rw ← nat.succ_le_iff at hx0,
  linarith,
end

noncomputable def separate : ℕ → ℕ × ℕ := λ n, ⟨max_sq n, sep_primes n⟩


lemma base': ∑ x in {1}, 2 * x = 2 :=
begin
  simp,
end

lemma test : separate 1 = ⟨1, 1⟩ :=
begin
  
  rw separate,
  simp,
  rw sep_primes,
  rw max_sq,
  simp,
  have hsup : Sup {b : ℕ | b ^ 2 = 1} = 1,
  {
    have h: {b|b^2 = 1} = {1},
    {
      ext a,
      simp,
      split,
      {
        intro h,
        rw sq at h,
        exact nat.eq_one_of_mul_eq_one_left h,
      },
      {
        intro h,
        rw h,
        simp,
      }
    },
    rw h,
    simp,
  },
  split,
    exact hsup,
    rw hsup,
    simp,
end

lemma dvds_le {a b : ℕ} (hab: a ∣ b) (hb0: b ≠ 0): a ≤ b :=
begin
  cases hab with k hab,
  rw hab,
  have hk0: k ≠ 0,
  {
    intro hk,
    rw hk at hab,
    simp at *,
    apply hb0,
    exact hab,
  },
  have h0k: 0 < k := zero_lt_iff.mpr hk0,
  have h1k: 1 ≤ k := nat.succ_le_iff.mpr h0k,
  exact le_mul_of_one_le_right' h1k,
end

lemma sep_codomain (n x : ℕ) : image separate (smooth_numbers n x) ⊆ finset.product (erase (range (1 + nat.sqrt x)) 0)  (finset.filter squarefree (smooth_numbers n x)) :=
begin
  intros a h,
  cases a with a b,
  simp at h,
  simp,
  cases h with m h,
  cases h with hm hab,
  rw separate at hab,
  simp at hab,
  cases hab with ha hb,
  split,
  split,
  {
    intro ha0,
    rw ha0 at ha,
    have hss := sq_sep,
    rw ha at hss,
    simp at hss,
    rw hss at hm,
    have hn := not_smooth_zero,
    apply hn,
    exact hm,
  },
  {
    have hm0: ¬ m = 0 := by apply smooth_not_zero hm,
    rw nat.add_comm,
    rw nat.lt_add_one_iff,
    rw smooth_numbers at *,
    simp at *,
    cases hm with hmx,
    have ham : a^2 ≤ m,
    {
      apply dvds_le,
      {
        rw ← ha,
        exact max_sq_divs,
      },
      {
        exact hm0,
      }
    },
    have hax': a^2 < x := gt_of_gt_of_ge hmx ham,
    have hax: a^2 ≤ x := le_of_lt hax',
    have hsqrt: nat.sqrt (a^2) ≤ nat.sqrt x := nat.sqrt_le_sqrt hax,
    have hasqrt: nat.sqrt(a*a) = a := by apply nat.sqrt_eq,
    rw ← sq at hasqrt,
    rw hasqrt at hsqrt,
    exact hsqrt,
  },
  split,
  {
    apply factor_smooth,
    {
      have hs: sep_primes m ∣ m := by exact sep_divs,
      convert hs,
      apply eq.symm,
      exact hb,
    },
    exact hm,
  },
  {
    rw ← hb,
    apply sq_free,
    apply smooth_not_zero,
    exact hm,
  }
end

lemma sep_injective : function.injective separate :=
begin 
  rw function.injective,
  rw separate,
  simp,
  intros m n hmax hsep,
  have hn : n = (sep_primes n) * (max_sq n)^2 := sq_sep,
  have hm : m = (sep_primes m) * (max_sq m)^2 := sq_sep,
  rw hn,
  rw hm,
  rw hmax,
  rw hsep,
end

lemma card_of_sqfree_base {x a: ℕ}: a ∈ smooth_numbers 0 x → a = 1:=
begin
  intro h,
  rw smooth_numbers at h,
  simp at h,
  cases h with hax h,
  set b := nat.min_fac a with hb,
  specialize h b,
  rw hb at h,
  have hmin: a ≠ 1 → nat.min_fac a < primecount 0,
  {
    intro ha1,
    apply h,
    {
      apply nat.min_fac_prime,
      exact ha1,
    },
    apply nat.min_fac_dvd,
  },
  rw primecount at hmin,
  by_contra,
  specialize hmin h,
  rw nat.lt_add_one_iff at hmin,
  apply h,
  have hpos: 0 < a.min_fac := by apply nat.min_fac_pos,
  rw nat.lt_iff_add_one_le at hpos,
  simp at hpos,
  have ha1: a.min_fac = 1 := by linarith,
  simp at ha1,
  exact ha1,
end

lemma smooth_squarefree_reduce_n {n x a: ℕ} (h: a ∈ smooth_numbers (n + 1) x) (hsq: squarefree a) (hna: primecount n ∣ a): ∃ (k : ℕ), (k ∈ smooth_numbers n x ∧ squarefree k) ∧ primecount n * k = a := 
begin
  cases hna with k hna,
  use k,
  split,
    split,
    {
      rw smooth_numbers,
      simp at *,
      split,
      {
        apply lt_of_le_of_lt,
        apply dvds_le,
        use primecount n,
        rw mul_comm,
        rw ← hna,
        apply smooth_not_zero,
        exact h,
        rw mul_comm,
        rw ← hna,
        rw smooth_numbers at h,
        simp at h,
        cases h with first h,
        exact first,
      },
      intros p hp hpk,
      have hpnone: p < primecount (n+1),
      {
        rw smooth_numbers at h,
        simp at h,
        cases h with hax h,
        apply h,
          exact hp,
          apply dvd_trans,
            exact hpk,
            use primecount n,
            rw hna,
            apply mul_comm,
      },
      have hpnone': p ≠ primecount n,
      {
        cases hpk with m hpk,
        by_contra hpn,
        simp at hpn,
        rw ← hpn at hna,
        rw hpk at hna,
        rw squarefree at hsq,
        specialize hsq p,
        rw nat.prime at hp,
        cases hp with h2p hp,
        rw ← not_lt at h2p,
        apply h2p,
        rw nat.lt_succ_iff,
        have hp1: p = 1,
        {
          rw ← nat.is_unit_iff,
          apply hsq,
          rw hna,
          use m,
          rw mul_assoc,
        },
        rw hp1,
      },
      have hpneq: p ≤ primecount n,
      {
        apply ind_prime,
          exact hp,
          apply hpnone,
      },
      rw ← ne.le_iff_lt,
        exact hpneq,
        exact hpnone',
    },
    {
      rw squarefree,
      intros x hxk,
      apply hsq,
      apply dvd_trans,
        exact hxk,
        use primecount n,
        rw hna,
        rw mul_comm,
    },
  apply eq.symm,
  exact hna,
end

lemma card_of_sqfree_step {n x: ℕ}: filter squarefree (smooth_numbers (n+1) x) ⊆ (filter squarefree(smooth_numbers n x)) ∪ (finset.image (λ m, (primecount n) * m) (filter squarefree  (smooth_numbers n x))) :=
begin
  intros a h,
  simp at *,
  cases h with h hsq,

  by_cases hna: primecount n ∣ a,
  {
    right,
    apply smooth_squarefree_reduce_n h hsq hna,
  },
  {
    left,
    split,
    {
      rw smooth_numbers,
      simp,
      rw smooth_numbers at h,
      simp at h,
      split,
        {
          cases h with h,
          exact h,
        },
        {
          intros p hp hpa,
          cases h with hax h,
          specialize h p hp hpa,
          rw ← ne.le_iff_lt,
          {
            apply ind_prime,
              apply hp,
              apply h,
          },
          {
            intro hpeq,
            rw ← hpeq at hna,
            apply hna,
            exact hpa,
          }
        },
    },
    exact hsq,
  },
end

lemma card_of_squarefree : ∀ n, ∀ x, (filter squarefree (smooth_numbers n x)).card ≤ 2^n
| 0 :=
begin
  simp,
  intro x,
  have h1: finset.card {1} = 1,
  {
    rw card_eq_one,
    use 1,
  },
  rw ← h1,
  apply card_le_of_subset,
  intro a,
  simp,
  intros hs hsq,
  apply card_of_sqfree_base,
  exact hs,
end
| (nat.succ k) :=
begin
  intro x,
  have h: (filter squarefree (smooth_numbers (k.succ) x)).card ≤ (filter squarefree(smooth_numbers k x)).card + ((finset.image (λ m, (primecount k) * m) (filter squarefree (smooth_numbers k x)))).card,
  {
    have hstep: (filter squarefree (smooth_numbers (k.succ) x)).card ≤ ((filter squarefree(smooth_numbers k x)) ∪ ((finset.image (λ m, (primecount k) * m) (filter squarefree (smooth_numbers k x))))).card,
    {
      apply card_le_of_subset,
      apply card_of_sqfree_step,
    },
    apply le_trans hstep,
    apply card_union_le,
  },
  apply le_trans,
    exact h,
  {
    have hleft: (filter squarefree (smooth_numbers k x)).card ≤ 2 ^ k,
    {
      apply card_of_squarefree,
    },
    have hright: ((finset.image (λ m, (primecount k) * m)(filter squarefree (smooth_numbers k x)))).card ≤ 2^k,
    {
      apply le_trans card_image_le,
        apply card_of_squarefree,
    },
    have h2k: 2 ^ k.succ = 2 ^ k + 2 ^ k,
      ring_nf,
    linarith,
  }
end

lemma upper_estimate (n x : ℕ)  : card (smooth_numbers n x) ≤ 2^n * nat.sqrt(x) :=
begin 
  have f := finset.card_le_of_subset (sep_codomain n x),
  rw finset.card_image_of_injective (smooth_numbers n x) sep_injective at f,
  have k := card_of_squarefree n x,
  have g := (1 + nat.sqrt x).pred.mul_le_mul_left k,
  rw finset.card_product (erase (range (1 + nat.sqrt x)) 0) (filter squarefree (smooth_numbers n x)) at f,
  rw card_erase_of_mem at f,
  rw card_range _ at f,
  rw (nat.sqrt x).pred_one_add at f g,
  rw mul_comm,
  exact le_trans f g,
  rw range,
  simp,
  exact (nat.sqrt x).zero_lt_one_add,
end

--lemma rough_numbers_cover (n x : ℕ) : ∃ k: ℕ, (finset.filter (λ n, ¬ (n ∈ (smooth_numbers n x))) (range x)) = (bUnion (finset.filter (λ y, y > n) (range k)) (λ y, set_of_multiples y x)) :=

lemma to_r_monotone_le {m n: ℕ} (m ≤ n) : (m:ℝ) ≤ (n:ℝ) :=
begin
  exact nat.cast_le.mpr H,
end

lemma to_r_monotone_lt {m n: ℕ} (m < n) : (m:ℝ) < (n:ℝ) :=
begin
  exact nat.cast_lt.mpr H,
end

def to_r (n : ℕ) : ℝ := (n:ℝ)

lemma to_r_homo {m n: ℕ} : to_r (m + n) = to_r m + to_r n :=
begin
  rw to_r,
  rw to_r,
  rw to_r,
  simp,
end

lemma to_r_homo'': ∀ k: ℕ, ∀ f: ℕ → ℕ, to_r ∑ i in (range k), f i = ∑ i in (range k), (f i: ℝ)
| 0 :=
begin
  simp,
  rw to_r,
  simp,
end
| (nat.succ t) :=
begin
  intro f,
  rw to_r,
  rw sum_eq_fold,
  rw sum_eq_fold,
  rw fold,
  rw fold,
  simp,
  apply to_r_homo'',
end

lemma to_r_homo'{k: ℕ} {f: ℕ → ℕ}: to_r ∑ i in (range k), f i = ∑ i in (range k), (f i: ℝ) :=
begin
  apply to_r_homo'',
end

lemma to_r_mul {m n: ℕ} : to_r (m * n) = to_r m * to_r n :=
begin
  rw to_r,
  rw to_r,
  rw to_r,
  simp,
end

lemma smooth_obvious_bound {n x : ℕ}: (smooth_numbers n x).card ≤ x :=
begin
  have h: (smooth_numbers n x).card ≤ (range x).card,
  {
    apply card_le_of_subset,
    intros a ha,
    rw smooth_numbers at ha,
    simp at ha,
    simp,
    cases ha with left right,
    exact left,
  },
  convert h,
  simp,
end

lemma rough_numbers_cover {n x : ℕ} : (finset.filter (λ m, ¬ (m ∈ (smooth_numbers n x))) (range x))\{0} = (finset.bUnion (finset.filter (λ y, n ≤ y) (range (x + n))) (λ y, set_of_multiples y x)) :=
begin
  ext a,
  simp,
  split,
  {
    intro h,
    cases h with h ha0,
    cases h with hax has,
    rw smooth_numbers at has,
    simp at has,
    specialize has hax,
    cases has with p hp,
    use number_of_prime p,
    cases hp with hpp hp,
    cases hp with hpa hnp,
    split,
    split,
    {
      apply lt_of_le_of_lt,
        apply index_le_prime hpp,
      apply lt_of_le_of_lt,
      {
        apply nat.le_of_dvd,
        {
          rw zero_lt_iff,
          exact ha0,
        },
          exact hpa,
      },
      apply lt_of_lt_of_le,
        exact hax,
        apply nat.le.intro,
        refl,
    },
    {
      have h: number_of_prime (primecount n) ≤ number_of_prime p,
      {
        apply n_of_prime_monotone,
          apply primecount_prime,
          exact hpp,
          exact hnp,
      },
      rw getting_the_index at h,
      exact h,
    },
    {
      rw set_of_multiples,
      simp,
      split,
        exact hax,
      split,
      {
        rw primecount_every,
          exact hpa,
          exact hpp,
      },
      {
        rw zero_lt_iff,
        exact ha0,
      },
    },
  },
  {
    intro h,
    cases h with i h,
    cases h with hi hai,
    cases hi with hixn hni,
    rw set_of_multiples at hai,
    simp at hai,
    cases hai with hax hai,
    cases hai with hpa h0a,
    rw smooth_numbers,
    simp,

    split,
    split,
      exact hax,
    {
      intro hax,
      use primecount i,
      split,
        apply primecount_prime,
      split,
        exact hpa,
        apply primecount_monotone hni,
    },
    linarith,
  }
end

lemma covercard_nat {n x: ℕ} (H: (finset.filter (λ m, ¬ (m ∈ (smooth_numbers n x))) (range x))\{0} = (finset.bUnion (finset.filter (λ y, n ≤ y) (range (x + n))) (λ y, set_of_multiples y x))): x - (smooth_numbers n x).card ≤ ∑ i in (range x),card (set_of_multiples (i+n) x)+1 :=
begin
  by_cases hx0: x = 0,
  {
    rw hx0,
    simp,
  },
  {
    have h: x - (smooth_numbers n x).card = (finset.filter (λ m, ¬ (m ∈ (smooth_numbers n x))) (range x)).card,
    {
      apply nat.sub_eq_of_eq_add,
      have h := filter_card_add_filter_neg_card_eq_card,
      set p: ℕ → Prop := λ k, k ∈ smooth_numbers n x with defp,
      specialize h p,
      apply eq.symm,
      convert h,
      {
        ext a,
        simp,
        rw defp,
        simp,
        rw smooth_numbers,
        simp,
      },
      simp,
    },
    rw h,
    have hrnc := rough_numbers_cover,
    have hrnc': filter (λ (m : ℕ), m ∉ smooth_numbers n x) (range x) \ {0} ∪ {0} = (filter (λ (y : ℕ), n ≤ y) (range (x + n))).bUnion (λ (y : ℕ), set_of_multiples y x) ∪ {0} := by rw hrnc,
    simp at hrnc',
    have h0: filter (λ (m : ℕ), m ∉ smooth_numbers n x) (range x) ∪ {0} = filter (λ (m : ℕ), m ∉ smooth_numbers n x) (range x),
    {
      rw union_comm,
      rw ← insert_eq,
      apply insert_eq_of_mem,
      simp,
      split,
        exact zero_lt_iff.mpr hx0,
        exact not_smooth_zero,
    },
    rw h0 at hrnc',
    rw hrnc',
    have hadd0: ((filter (has_le.le n) (range (x + n))).bUnion (λ (y : ℕ), set_of_multiples y x) ∪ {0}).card = ((filter (has_le.le n) (range (x + n))).bUnion (λ (y : ℕ), set_of_multiples y x)).card + 1,
    {
      rw union_comm,
      rw ← insert_eq,
      rw card_insert_of_not_mem,
      simp,
      intros y h1 h2,
      rw set_of_multiples,
      simp,
    },
    rw hadd0,
    simp,
    have hri: ∑ (i : ℕ) in filter (has_le.le n) (range (x + n)), (set_of_multiples i x).card = ∑ (i : ℕ) in range x, (set_of_multiples (i + n) x).card,
    {
      have hmap: filter (has_le.le n) (range (x + n)) = finset.map (add_inj n) (range x),
      {
        ext a,
        simp,
        split,
        {
          intros ha,
          use a - n,
          cases ha with hax hna,
          split,
          {
            rw nat.sub_lt_right_iff_lt_add,
              exact hax,
              exact hna,
          },
          {
            rw add_inj,
            simp,
            rw add_comm,
            rw nat.add_sub_cancel',
            exact hna,
          }
        },
        {
          intro hk,
          cases hk with k hk,
          cases hk with hkx hnk,
          rw add_inj at hnk,
          simp at hnk,
          rw ← hnk,
          split,
            exact add_lt_add_right hkx n,
            exact nat.le_add_left n k,
        }
      },
      rw hmap,
      apply sum_map,
    },
    rw ← hri,
    apply card_bUnion_le,
  },
  

end
def spread_multiples: ℕ × ℕ → ℕ := λ a, (a.1 - a.2)

lemma test2: spread_multiples ⟨5, 3⟩ = 2 :=
begin
  rw spread_multiples,
  simp,
end

lemma altc {a b c d p : ℕ} (hpa: p ∣ a) (hpc: p ∣ c) (hd: d < p) (haltc: a < c): a + d < c + b :=
begin
  have hadp: a + d < a + p,
  {
    simp,
    exact hd,
  },
  apply lt_of_lt_of_le hadp,
  have hapb: a + p ≤ c,
  {
    rw add_comm,
    have hpac: p ≤ c - a,
    {
      apply nat.le_of_dvd,
      {
        rw nat.lt_sub_right_iff_add_lt,
        simp,
        exact haltc,
      },
        apply nat.dvd_sub' hpc hpa,
    },
    rw ← nat.le_sub_right_iff_add_le,
      exact hpac,
      apply le_of_lt haltc,
  },
  apply le_trans hapb,
  norm_num,
end


lemma spread_injective {i x : ℕ}: set.inj_on spread_multiples ↑((set_of_multiples i x).product (range (primecount i))) :=
begin
  rw set.inj_on,
  intro a,
  cases a with a b,
  intros hab c,
  cases c with c d,
  intros hcd hf,
  rw finset.product at hab,
  simp at hab,
  cases hab with ha hb,
  rw finset.product at hcd,
  simp at hcd,
  cases hcd with hc hd,
  rw spread_multiples at hf,
  simp at hf,
  rw set_of_multiples at ha,
  simp at ha,
  rw set_of_multiples at hc,
  simp at hc,
  cases ha with hax hpa,
  cases hpa with hpa h0a,
  cases hc with hcx hpc,
  cases hpc with hpc h0c,
  have hap: primecount i ≤ a,
  {
    apply nat.le_of_dvd,
      exact h0a,
      exact hpa,
  },
  have hcp: primecount i ≤ c,
  {
    apply nat.le_of_dvd,
      exact h0c,
      exact hpc,
  },
  have hba: b ≤ a,
  {
    apply le_trans,
      apply le_of_lt hb,
      exact hap,
  },
  have hdc: d ≤ c,
  {
    apply le_trans,
      apply le_of_lt hd,
      exact hcp,
  },
  have hbb: a - b + b = a,
  {
    rw add_comm,
    apply nat.add_sub_cancel' hba,
  },
  have hdd: c - d + d = c,
  {
    rw add_comm,
    apply nat.add_sub_cancel' hdc,
  },
  have hadcb: a + d = c + b,
  {
    rw ← hbb,
    rw hf,
    rw add_assoc,
    rw add_comm,
    rw add_assoc,
    rw add_comm,
    simp,
    rw add_comm,
    exact hdd,
  },
  have hac: a = c,
  {
    by_contra,
    have haltc: a < c ∨ c < a := ne.lt_or_lt h,
    cases haltc,
    {
      have hlt: a + d < c + b := by apply altc hpa hpc hd haltc,
      linarith,
    },
    {
      have hlt: c + b < a + d := by apply altc hpc hpa hb haltc,
      linarith,
    },
  },
  ext,
  {
    simp,
    exact hac,
  },
  {
    simp,
    rw hac at hadcb,
    simp at hadcb,
    apply eq.symm,
    exact hadcb,
  },
end

lemma card_image_eq {i x: ℕ} : (finset.product (set_of_multiples i x) (range (primecount i))).card = (image spread_multiples (finset.product (set_of_multiples i x) (range (primecount i)))).card :=
begin
  apply eq.symm,
  apply card_image_of_inj_on,
  apply spread_injective,
end

lemma set_of_multiples_bound_nat' {i x: ℕ} : (finset.product (set_of_multiples i x) (range (primecount i))).card  ≤ (range x).card :=
begin
  rw card_image_eq,
  apply finset.card_le_of_subset,
  intros a,
  simp,
  rw spread_multiples,
  simp,
  intros m n hm hn ha,
  rw ← ha,
  rw set_of_multiples at hm,
  simp at hm,
  cases hm with hmx hm,
  have hmn: m - n ≤ m := nat.sub_le m n,
  apply lt_of_le_of_lt,
    exact hmn,
    exact hmx,
end

lemma set_of_multiples_bound_nat {i x: ℕ} : (set_of_multiples i x).card * primecount i ≤ x :=
begin
  convert set_of_multiples_bound_nat',
    simp,
    simp,
end

lemma set_of_multiples_bound {i x : ℕ} : (card (set_of_multiples i x):ℝ) ≤ (x:ℝ) / (primecount i) :=
begin 
  rw le_div_iff,
  {
    have htor: to_r((set_of_multiples i x).card * primecount i) ≤ to_r(x),
    {
      apply to_r_monotone_le,
      exact 0,
      apply set_of_multiples_bound_nat,
    },
    rw to_r at htor,
    rw to_r at htor,
    simp at htor,
    exact htor,
  },
  {
    simp,
    apply lt_of_lt_of_le,
      have h02: 0 < 2 := by norm_num,
      exact h02,
      apply nat.prime.two_le,
      apply primecount_prime,
  },
end

lemma covercard {n x: ℕ} {x': ℝ} (hxx': x' = ↑x) (H: (finset.filter (λ m, ¬ (m ∈ (smooth_numbers n x))) (range x))\{0} = (finset.bUnion (finset.filter (λ y, n ≤ y) (range (x + n))) (λ y, set_of_multiples y x))): x' - (smooth_numbers n x).card ≤ (∑ i in (range x),card (set_of_multiples (i+n) x)+1:ℝ) :=
begin
  have hcovercard: to_r (x - (smooth_numbers n x).card) ≤ to_r(∑ i in (range x),card (set_of_multiples (i+n) x) +1),
  {
    apply to_r_monotone_le,
    exact 0,
    apply covercard_nat H,
  },
  rw to_r at hcovercard,
  rw to_r at hcovercard,
  convert hcovercard using 1,
  {
    rw hxx',
    rw sub_eq_of_eq_add,
    rw <- to_r,
    rw <- to_r,
    rw <- to_r,
    rw ← to_r_homo,
    have hsm := smooth_obvious_bound,
    have hc : x = x - (smooth_numbers n x).card + (smooth_numbers n x).card,
    {
      exact (nat.sub_eq_iff_eq_add hsm).mp rfl,
    },
    rw ← hc,
  },
  {
    apply eq.symm,
    simp,
    convert to_r_homo' using 1,
  }
end

lemma lower_estimate (n x: ℕ) (x' : ℝ) (HH: summable primerec) (H : ∑' (i : ℕ), primerec (i + n) < 1/2) (hxx': x' = ↑x) (h0x: 0 < x): x'/2 < card (smooth_numbers n x) + 1 :=
begin 
  have h: x' - (smooth_numbers n x).card < x'/2 + 1,
  {
    have hleft: x' - (smooth_numbers n x).card < ∑' (i : ℕ), x' * primerec (i + n) + 1,
    {
      rw primerec,
      simp,
      have h := rough_numbers_cover,
      have hcutk: x' - (smooth_numbers n x).card ≤ ∑ i in (range x), x' * primerec (i + n) +1,
      {
        apply le_trans,
          apply covercard hxx',
          apply h,
          simp,
          apply sum_le_sum,
          intros i hik,
          convert set_of_multiples_bound,
          rw primerec,
          simp,
      },
      apply lt_of_le_of_lt,
        exact hcutk,
        have hk1: ∑ (i : ℕ) in range x, x' * primerec (i + n) +1 < ∑ (i : ℕ) in range (x+1), x' * primerec (i + n) +1,
        {
          simp,
          have hn1: ∑ (i : ℕ) in range (x+1), x' * primerec (i + n) = ∑ (i : ℕ) in range x, x' * primerec (i + n) + x' * primerec (x + n),
          {
            rw sum_eq_fold,
            rw sum_eq_fold,
            rw fold,
            rw fold,
            simp,
            rw add_comm,
          },
          rw hn1,
          simp,
          apply mul_pos,
          {
            rw hxx',
            simp,
            exact h0x,
          },
          {
            rw primerec,
            simp,
            apply lt_of_lt_of_le,
              have h02: 0 < 2 := by norm_num,
              exact h02,
              apply nat.prime.two_le,
              apply primecount_prime,
          },
        },
        apply lt_of_lt_of_le,
          exact hk1,
          rw primerec,
          simp,
          apply sum_le_tsum,
          {
            intros b hb,
            apply mul_nonneg,
            {
              rw hxx',
              simp,
            },
              simp,
          },
          {
            rw <- summable_mul_left_iff,
            {
              have hsumn: summable (λ (b : ℕ), primerec (b + n)),
              {
                rw summable_nat_add_iff,
                exact HH,
              },
              convert hsumn,
              rw primerec,
              simp,
            },
            {
              rw hxx',
              intro hx0,
              simp at hx0,
              linarith,
            },
          },
    },
    apply lt_trans hleft,
    rw tsum_mul_left,
    rw div_eq_mul_one_div x' 2,
    simp,
    have h2: (2:ℝ)⁻¹ = 1/2 := by norm_num,
    rw h2,
    refine (mul_lt_mul_left _).mpr H,
    rw hxx',
    have htorx: to_r 0 < to_r x,
    {
      apply to_r_monotone_lt,
      exact 0,
      exact h0x,
    },
    rw to_r at htorx,
    rw to_r at htorx,
    exact htorx,
  },
  have h': x' - x'/2 < (smooth_numbers n x).card + 1 := by linarith,
  have hxx : x' - x'/2 = x'/2 := by linarith,
  rw hxx at h',
  exact h',
end

theorem prime_reciprocal_diverges : ¬ summable primerec :=
begin
  by_contra H,
  have Hn := picking_a_cutoff H,
  cases Hn with n hn,
  set x := 2^(2*n+4) with hx,
  set x':ℝ := ↑ x with hx',
  have hx : (x = 2^(2*n+4)) := by refl,
  have Eup := upper_estimate n x,
  have Eup' : to_r((smooth_numbers n x).card) ≤ to_r(((2:ℕ) ^ n) * nat.sqrt x),
  {
    apply to_r_monotone_le,
    exact 0,
    exact Eup,
  },
  rw to_r at Eup',
  rw to_r at Eup',
  simp at Eup',
  have Elo := lower_estimate n x x' H hn,
  specialize Elo hx',
  have Est : x' / 2 <  (2 ^ n) * ↑ (nat.sqrt(x)) + 1,
  {
    apply lt_of_lt_of_le,
    apply Elo,
    {
      rw hx,
      norm_num,
    },
    simp,
    exact Eup',
  },
  rw hx at Est,
  have f : 2*n+4 = 2*(n+2) := by ring,
  rw f at Est,
  rw pow_mul' at Est,
  rw pow_two (2^(n+2)) at Est,
  rw nat.sqrt_eq at Est,
  simp at Est,
  have Est': x' < (2 ^ n * 2 ^ (n + 2)) * 2 + 2 := by linarith,
  have Est'': x' < (2 ^ (n + 1) * 2 ^ (n + 2)) + 2,
  {
    convert Est' using 1,
    simp,
    apply eq.symm,
    rw mul_comm,
    rw ← mul_assoc,
    simp,
    refl,
  },
  rw <- pow_add at Est'',
  rw hx' at Est'',
  rw hx at Est'',
  simp at Est'',
  have h2n: n + 1 + (n + 2) = 2*n + 3 := by linarith,
  rw h2n at Est'',
  rw lt_iff_not_ge' at Est'',
  apply Est'',
  have h2nn: (2:ℝ) ^ (2 * n + 3) + 2 ≤ 2 ^ (2 * n + 3) + 2 ^ (2 * n + 3),
  {
    simp,
    have h21: (2:ℝ) = 2^1:= by simp,
    rw h21,
    rw ← pow_mul',
    apply pow_mono,
      norm_num,
      norm_num,
      have hnpos: 0 ≤ n := zero_le n,
      linarith,
  },
  apply le_trans,
    exact h2nn,
  {
    rw ← mul_two,
    have h21: (2:ℝ) = 2^1:= by simp,
    rw h21,
    rw ← pow_mul',
    rw ← pow_mul',
    rw ← pow_add,
    simp,
  }
end