gistfile1.txt

import tactic.norm_num
import data.nat.prime
import data.nat.modeq
import data.zmod.basic

namespace MATH2222.Assignment1
section Question4
open nat
open nat.modeq

lemma eq_of_modeq {n m k : ℕ} (w : n ≡ m [MOD k]) (h : m < k) : ∃ s, k*s+m = n :=
begin
  rcases exists_eq_mul_right_of_dvd (dvd_of_modeq w.symm) with ⟨s, g⟩,
  sorry
end

lemma modeq_of_eq {n m : ℕ} (h : n = m) (k : ℕ): n ≡ m [MOD k] :=
by rw h

-- @[simp] lemma zmod.cast_self_eq_zero' {n : ℕ} {h : n > 0} : (n : zmod ⟨n, h⟩) = 0 :=
-- zmod.cast_self_eq_zero

@[simp] lemma prod_zmod (n : ℕ+) : Π xs : list ℕ, (((list.prod xs) : ℕ) : zmod n) = list.prod (xs.map (λ x, (x : zmod n))) :=
begin
  sorry
end

lemma residue_3_has_residue_3_prime_factor (n : ℕ) : ∃ k : ℕ, prime (4*k+3) ∧ (4*k+3) ∣ (4*n+3) :=
begin
  have q : 4*n+3 > 0, sorry,
  -- by_cases (∃ k : ℕ, 4*k+3 ∈ factors), -- nope, not decidable!
  by_cases (∃ p ∈ factors (4*n+3), p ≡ 3 [MOD 4]),
  -- Either one of the factors is 3 mod 4, and we're done
  { rcases h with ⟨p, f, m⟩,
    rcases eq_of_modeq m (by norm_num) with ⟨w, rfl⟩,
    use w,
    have pp : prime (4 * w + 3), apply mem_factors f,
    split,
    exact pp,
    exact (mem_factors_iff_dvd q pp).1 f
  },
  -- Otherwise, all of the factors are 1 mod 4, and we get a contradiction
  exfalso,
  simp at h,
  have h' : ∀ x ∈ factors (4*n+3), x ≡ 1 [MOD 4], sorry,
  have h'' : ∀ x ∈ factors (4*n+3), (x : zmod 4) = 1, sorry,
  clear h h',
  have w := prod_factors q,
  replace w := congr_arg (λ n : ℕ, (n : zmod 4)) w,
  dsimp at w,
  rw prod_zmod at w,
  rw list.map_congr h'' at w,
  simp at w,
  erw [zero_mul] at w,
  simp at w,
  cases w,
end

end Question4

end MATH2222.Assignment1