/-
OEIS A060841, Robert G. Wilson v's conjecture (2015):
`1/det(M)` is an integer only for `n = 1, …, 34, 36, 38`,
where `M` is the `n × n` matrix with `M[i,j] = 1/lcm(i,j)`.

Statement: `OeisA60841.conjecture1` of google-deepmind/formal-conjectures
(`FormalConjectures/OEIS/60841.lean`, commit e6d1743831c2), tagged `research open` there.

Proof outline.
* Smith's determinant gives `1/det(M) = ∏_{k ≤ n} k² / φ(k) = (n!)² / ∏_{k ≤ n} φ(k)`.
* For `n ≤ 38` the divisibility `∏ φ(k) ∣ (n!)²` is decided by computation.
* For all other `n` the 2-adic valuation of `∏ φ(k)` exceeds that of `(n!)²`:
  `v₂(φ(k)) + [2 ∣ k] ≥ v₂(k) + ∑_{p ∣ k, p odd prime} v₂(p - 1)`, and summing over `k ≤ n`
  with the odd primes `p ≤ 61` gives `v₂(∏ φ(k)) + ⌊n/2⌋ ≥ v₂(n!) + wSum(n)` where
  `wSum(n) = ∑_{3 ≤ p ≤ 61} v₂(p - 1) ⌊n/p⌋`.  Since `wSum(n) ≥ n + ⌊n/2⌋ > v₂(n!) + ⌊n/2⌋`
  for `n ≥ 128`, and the same strict inequality holds for the remaining `n < 128` by a finite
  check, `∏ φ(k)` cannot divide `(n!)²`.

The determinant section (`divMatrix` … `lcmMatrix_det`) is adapted from
anatoliiohorodnyk/lean-fc-proofs, `Proofs/T_OeisA60841_conjecture2.lean` (Apache-2.0),
which proves the sibling statement `conjecture2`.
-/
import FormalConjectures.OEIS.«60841»

namespace OeisA60841

/-! ### Closed form of the determinant (Smith) -/

/-- Divisor-incidence matrix. -/
def divMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℚ :=
  Matrix.of fun i k : Fin n => if (k.val + 1) ∣ (i.val + 1) then 1 else 0

lemma divMatrix_det (n : ℕ) : (divMatrix n).det = 1 := by
  rw [Matrix.det_of_isLowerTriangular]
  · simp only [divMatrix, Matrix.of_apply, dvd_refl, if_true, Finset.prod_const_one]
  · intro i k hik
    simp only [divMatrix, Matrix.of_apply]
    rw [if_neg]
    intro hdvd
    have := Nat.le_of_dvd (Nat.succ_pos _) hdvd
    have hik' : i < k := hik
    have : i.val < k.val := hik'
    omega

lemma sum_totient_dvd (n a b : ℕ) (ha : 1 ≤ a) (han : a ≤ n) (_hb : 1 ≤ b) :
    ∑ k : Fin n, (if (k.val + 1) ∣ a ∧ (k.val + 1) ∣ b then (Nat.totient (k.val + 1) : ℚ) else 0)
      = Nat.gcd a b := by
  rw [Fin.sum_univ_eq_sum_range (fun k => if (k + 1) ∣ a ∧ (k + 1) ∣ b then
    (Nat.totient (k + 1) : ℚ) else 0) n, ← Finset.sum_filter]
  have hg : Nat.gcd a b ≠ 0 := Nat.gcd_ne_zero_left (by omega)
  have : ((Finset.range n).filter fun k => (k + 1) ∣ a ∧ (k + 1) ∣ b).map (addRightEmbedding 1)
      = (Nat.gcd a b).divisors := by
    ext d
    simp only [Finset.mem_map, Finset.mem_filter, Finset.mem_range, addRightEmbedding_apply,
      Nat.mem_divisors, Nat.dvd_gcd_iff]
    constructor
    · rintro ⟨k, ⟨hk, h1, h2⟩, rfl⟩
      exact ⟨⟨h1, h2⟩, hg⟩
    · rintro ⟨⟨h1, h2⟩, -⟩
      have hd : 1 ≤ d := Nat.pos_of_dvd_of_pos h1 (by omega)
      refine ⟨d - 1, ⟨?_, ?_, ?_⟩, by omega⟩
      · have := Nat.le_of_dvd (by omega) h1; omega
      · rwa [Nat.sub_add_cancel hd]
      · rwa [Nat.sub_add_cancel hd]
  have hsum := congrArg (fun s => ∑ d ∈ s, (Nat.totient d : ℚ)) this
  simp only [Finset.sum_map, addRightEmbedding_apply] at hsum
  rw [hsum]
  exact_mod_cast Nat.sum_totient (Nat.gcd a b)

lemma gcd_factor (n : ℕ) (i j : Fin n) :
    (divMatrix n * Matrix.diagonal (fun k : Fin n => (Nat.totient (k.val + 1) : ℚ)) *
      (divMatrix n).transpose) i j = Nat.gcd (i.val + 1) (j.val + 1) := by
  rw [← sum_totient_dvd n (i.val + 1) (j.val + 1) (by omega) i.isLt (by omega), Matrix.mul_apply]
  refine Finset.sum_congr rfl fun x _ => ?_
  rw [Matrix.mul_diagonal, Matrix.transpose_apply]
  simp only [divMatrix, Matrix.of_apply]
  split_ifs <;> simp_all

lemma lcmMatrix_factor (n : ℕ) :
    lcmMatrix n = Matrix.diagonal (fun i : Fin n => 1 / ((i.val + 1 : ℕ) : ℚ)) *
      (divMatrix n * Matrix.diagonal (fun k : Fin n => (Nat.totient (k.val + 1) : ℚ)) *
        (divMatrix n).transpose) *
      Matrix.diagonal (fun j : Fin n => 1 / ((j.val + 1 : ℕ) : ℚ)) := by
  ext i j
  rw [Matrix.mul_diagonal, Matrix.diagonal_mul, gcd_factor]
  simp only [lcmMatrix, Matrix.of_apply]
  have hl := Nat.gcd_mul_lcm (i.val + 1) (j.val + 1)
  have hl' : ((Nat.gcd (i.val + 1) (j.val + 1) : ℕ) : ℚ) * (Nat.lcm (i.val + 1) (j.val + 1) : ℕ)
      = ((i.val + 1 : ℕ) : ℚ) * ((j.val + 1 : ℕ) : ℚ) := by exact_mod_cast hl
  have hlcm : ((Nat.lcm (i.val + 1) (j.val + 1) : ℕ) : ℚ) ≠ 0 := by
    exact_mod_cast Nat.lcm_ne_zero (by omega) (by omega)
  have hi : ((i.val + 1 : ℕ) : ℚ) ≠ 0 := by exact_mod_cast (by omega : i.val + 1 ≠ 0)
  have hj : ((j.val + 1 : ℕ) : ℚ) ≠ 0 := by exact_mod_cast (by omega : j.val + 1 ≠ 0)
  have hg : ((Nat.gcd (i.val + 1) (j.val + 1) : ℕ) : ℚ) ≠ 0 := by
    exact_mod_cast Nat.gcd_ne_zero_left (by omega)
  field_simp
  linear_combination (-1 : ℚ) * hl'

lemma lcmMatrix_det (n : ℕ) : (lcmMatrix n).det =
    ∏ i : Fin n, ((Nat.totient (i.val + 1) : ℚ) / ((i.val + 1 : ℕ) : ℚ) ^ 2) := by
  rw [lcmMatrix_factor, Matrix.det_mul, Matrix.det_mul, Matrix.det_mul, Matrix.det_mul,
    Matrix.det_transpose, divMatrix_det, Matrix.det_diagonal, Matrix.det_diagonal]
  simp only [one_mul, mul_one]
  rw [← Finset.prod_mul_distrib, ← Finset.prod_mul_distrib]
  refine Finset.prod_congr rfl fun i _ => ?_
  ring

/-! ### Reduction to a divisibility of natural numbers -/

/-- `sqProd n = ∏_{k=1}^n k²`. -/
def sqProd (n : ℕ) : ℕ := ∏ k ∈ Finset.range n, (k + 1) ^ 2

/-- `phiProd n = ∏_{k=1}^n φ(k)`. -/
def phiProd (n : ℕ) : ℕ := ∏ k ∈ Finset.range n, Nat.totient (k + 1)

lemma phiProd_ne_zero (n : ℕ) : phiProd n ≠ 0 :=
  Finset.prod_ne_zero_iff.mpr fun k _ => (Nat.totient_pos.mpr (Nat.succ_pos k)).ne'

lemma sqProd_eq (n : ℕ) : sqProd n = n.factorial ^ 2 := by
  rw [sqProd, Finset.prod_pow, Finset.prod_range_add_one_eq_factorial]

lemma inv_det (n : ℕ) : ((lcmMatrix n).det)⁻¹ = (sqProd n : ℚ) / (phiProd n : ℚ) := by
  rw [lcmMatrix_det, sqProd, phiProd, Fin.prod_univ_eq_prod_range
    (fun i => ((Nat.totient (i + 1) : ℚ) / ((i + 1 : ℕ) : ℚ) ^ 2)) n,
    Nat.cast_prod, Nat.cast_prod, ← Finset.prod_div_distrib, ← Finset.prod_inv_distrib]
  refine Finset.prod_congr rfl fun i _ => ?_
  rw [inv_div, Nat.cast_pow]

lemma den_eq_one_iff_dvd (a b : ℕ) (hb : b ≠ 0) : ((a : ℚ) / (b : ℚ)).den = 1 ↔ b ∣ a := by
  have hb' : (b : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr hb
  constructor
  · intro h
    have hq := (Rat.den_eq_one_iff _).mp h
    have h2 : (((a : ℚ) / b).num : ℚ) * (b : ℚ) = (a : ℚ) := by
      rw [hq, div_mul_cancel₀ _ hb']
    have h3 : ((a : ℚ) / b).num * (b : ℤ) = (a : ℤ) := by exact_mod_cast h2
    exact Int.natCast_dvd_natCast.mp (Dvd.intro_left _ h3)
  · rintro ⟨c, rfl⟩
    rw [Nat.cast_mul, mul_div_cancel_left₀ _ hb']
    exact Rat.den_natCast c

/-! ### 2-adic valuations -/

lemma v2_prod {ι : Type*} (s : Finset ι) (f : ι → ℕ) (hf : ∀ i ∈ s, f i ≠ 0) :
    padicValNat 2 (∏ i ∈ s, f i) = ∑ i ∈ s, padicValNat 2 (f i) := by
  classical
  induction s using Finset.induction with
  | empty => rw [Finset.prod_empty, Finset.sum_empty, padicValNat_one_right]
  | insert a s ha ih =>
    rw [Finset.prod_insert ha, Finset.sum_insert ha]
    have hfa : f a ≠ 0 := hf a (Finset.mem_insert_self a s)
    have hfs : (∏ i ∈ s, f i) ≠ 0 :=
      Finset.prod_ne_zero_iff.mpr fun i hi => hf i (Finset.mem_insert_of_mem hi)
    rw [padicValNat.mul hfa hfs, ih fun i hi => hf i (Finset.mem_insert_of_mem hi)]

/-- Pointwise bound: `v₂(k) + ∑_{p ∈ S, p ∣ k} w(p) ≤ v₂(φ(k)) + [2 ∣ k]`. -/
lemma pointwise (S : Finset ℕ) (w : ℕ → ℕ)
    (hS : ∀ p ∈ S, p.Prime ∧ w p ≤ padicValNat 2 (p - 1)) (k : ℕ) (hk : k ≠ 0) :
    padicValNat 2 k + ∑ p ∈ S, (if p ∣ k then w p else 0)
      ≤ padicValNat 2 (Nat.totient k) + (if 2 ∣ k then 1 else 0) := by
  have hRdvd : (∏ p ∈ k.primeFactors, p) ∣ k := Nat.prod_primeFactors_dvd k
  have hRpos : 0 < ∏ p ∈ k.primeFactors, p :=
    Finset.prod_pos fun p hp => (Nat.prime_of_mem_primeFactors hp).pos
  have hQne : (∏ p ∈ k.primeFactors, (p - 1)) ≠ 0 :=
    Finset.prod_ne_zero_iff.mpr fun p hp => by
      have := (Nat.prime_of_mem_primeFactors hp).two_le; omega
  have hkR : k / (∏ p ∈ k.primeFactors, p) ≠ 0 := by
    have := Nat.div_pos (Nat.le_of_dvd (Nat.pos_of_ne_zero hk) hRdvd) hRpos; omega
  have h1 : padicValNat 2 (Nat.totient k) =
      padicValNat 2 (k / ∏ p ∈ k.primeFactors, p) +
        padicValNat 2 (∏ p ∈ k.primeFactors, (p - 1)) := by
    rw [Nat.totient_eq_div_primeFactors_mul k, padicValNat.mul hkR hQne]
  have h2 : padicValNat 2 (k / ∏ p ∈ k.primeFactors, p) =
      padicValNat 2 k - padicValNat 2 (∏ p ∈ k.primeFactors, p) :=
    padicValNat.div_of_dvd hRdvd
  have h3 : padicValNat 2 (∏ p ∈ k.primeFactors, p) ≤ (if 2 ∣ k then 1 else 0) := by
    rw [v2_prod _ _ (fun p hp => (Nat.prime_of_mem_primeFactors hp).ne_zero)]
    have hterm : ∀ p ∈ k.primeFactors, padicValNat 2 p = if p = 2 then 1 else 0 := by
      intro p hp
      have hpp := Nat.prime_of_mem_primeFactors hp
      split_ifs with h
      · subst h; exact padicValNat_self
      · have : Fact p.Prime := ⟨hpp⟩
        exact padicValNat_primes (Ne.symm h)
    rw [Finset.sum_congr rfl hterm, Finset.sum_ite_eq']
    split_ifs with h1 h2 h2
    · exact le_rfl
    · exact absurd (Nat.dvd_of_mem_primeFactors h1) h2
    · exact Nat.zero_le _
    · exact le_rfl
  have h4 : ∑ p ∈ S, (if p ∣ k then w p else 0) ≤
      padicValNat 2 (∏ p ∈ k.primeFactors, (p - 1)) := by
    rw [v2_prod _ _ (fun p hp => by
      have := (Nat.prime_of_mem_primeFactors hp).two_le; omega), ← Finset.sum_filter]
    calc ∑ p ∈ S.filter (· ∣ k), w p
        ≤ ∑ p ∈ S.filter (· ∣ k), padicValNat 2 (p - 1) :=
          Finset.sum_le_sum fun p hp => (hS p (Finset.mem_of_mem_filter p hp)).2
      _ ≤ ∑ p ∈ k.primeFactors, padicValNat 2 (p - 1) := by
          apply Finset.sum_le_sum_of_subset
          intro p hp
          rw [Finset.mem_filter] at hp
          exact Nat.mem_primeFactors.mpr ⟨(hS p hp.1).1, hp.2, hk⟩
  generalize (if 2 ∣ k then 1 else 0 : ℕ) = t at h3 ⊢
  omega

/-- Summed bound: `v₂(n!) + ∑_{p ∈ S} w(p) ⌊n/p⌋ ≤ v₂(∏_{k ≤ n} φ(k)) + ⌊n/2⌋`. -/
lemma key_bound (S : Finset ℕ) (w : ℕ → ℕ)
    (hS : ∀ p ∈ S, p.Prime ∧ w p ≤ padicValNat 2 (p - 1)) (n : ℕ) :
    padicValNat 2 n.factorial + ∑ p ∈ S, w p * (n / p) ≤ padicValNat 2 (phiProd n) + n / 2 := by
  have hP : padicValNat 2 (phiProd n) =
      ∑ k ∈ Finset.range n, padicValNat 2 (Nat.totient (k + 1)) :=
    v2_prod _ _ fun k _ => (Nat.totient_pos.mpr (Nat.succ_pos k)).ne'
  have hfac : padicValNat 2 n.factorial = ∑ k ∈ Finset.range n, padicValNat 2 (k + 1) := by
    rw [← Finset.prod_range_add_one_eq_factorial]
    exact v2_prod _ _ fun k _ => Nat.succ_ne_zero k
  have hhalf : n / 2 = ∑ k ∈ Finset.range n, (if 2 ∣ k + 1 then 1 else 0) := by
    rw [← Nat.card_multiples n 2, Finset.card_filter]
  have hW : ∑ p ∈ S, w p * (n / p) =
      ∑ k ∈ Finset.range n, ∑ p ∈ S, (if p ∣ k + 1 then w p else 0) := by
    rw [Finset.sum_comm]
    refine Finset.sum_congr rfl fun p _ => ?_
    rw [← Nat.card_multiples n p, Finset.card_filter, Finset.mul_sum]
    refine Finset.sum_congr rfl fun k _ => ?_
    split_ifs
    · rw [mul_one]
    · rw [mul_zero]
  rw [hP, hfac, hhalf, hW, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
  exact Finset.sum_le_sum fun k _ => pointwise S w hS (k + 1) (Nat.succ_ne_zero k)

/-! ### The explicit set of primes and the numerical inequalities -/

/-- The odd primes up to `61`. -/
def oddPrimes : Finset ℕ := {3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61}

/-- `wt p = v₂(p - 1)` for `p ∈ oddPrimes`. -/
def wt (p : ℕ) : ℕ :=
  if p = 17 then 4 else if p = 41 then 3
  else if p = 5 ∨ p = 13 ∨ p = 29 ∨ p = 37 ∨ p = 53 ∨ p = 61 then 2 else 1

lemma oddPrimes_spec : ∀ p ∈ oddPrimes, p.Prime ∧ wt p ≤ padicValNat 2 (p - 1) := by
  intro p hp
  simp only [oddPrimes, Finset.mem_insert, Finset.mem_singleton] at hp
  rcases hp with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl |
    rfl | rfl | rfl | rfl <;>
  exact ⟨by norm_num, (padicValNat_dvd_iff_le (by norm_num)).mp (by decide)⟩

/-- `wSum n = ∑_{p ∈ oddPrimes} wt p * ⌊n/p⌋`, written out. -/
abbrev wSum (n : ℕ) : ℕ :=
  n / 3 + 2 * (n / 5) + n / 7 + n / 11 + 2 * (n / 13) + 4 * (n / 17) + n / 19 + n / 23 +
  2 * (n / 29) + n / 31 + 2 * (n / 37) + 3 * (n / 41) + n / 43 + n / 47 + 2 * (n / 53) +
  n / 59 + 2 * (n / 61)

lemma wt_vals : wt 3 = 1 ∧ wt 5 = 2 ∧ wt 7 = 1 ∧ wt 11 = 1 ∧ wt 13 = 2 ∧ wt 17 = 4 ∧ wt 19 = 1 ∧
    wt 23 = 1 ∧ wt 29 = 2 ∧ wt 31 = 1 ∧ wt 37 = 2 ∧ wt 41 = 3 ∧ wt 43 = 1 ∧ wt 47 = 1 ∧
    wt 53 = 2 ∧ wt 59 = 1 ∧ wt 61 = 2 := by decide

lemma wSum_eq (n : ℕ) : ∑ p ∈ oddPrimes, wt p * (n / p) = wSum n := by
  obtain ⟨e3, e5, e7, e11, e13, e17, e19, e23, e29, e31, e37, e41, e43, e47, e53, e59, e61⟩ :=
    wt_vals
  unfold oddPrimes
  repeat rw [Finset.sum_insert (by decide)]
  rw [Finset.sum_singleton, e3, e5, e7, e11, e13, e17, e19, e23, e29, e31, e37, e41, e43, e47,
    e53, e59, e61]
  unfold wSum
  ring

lemma large_ineq (n : ℕ) (hn : 128 ≤ n) : n + n / 2 ≤ wSum n := by
  have h2 : 2 * (n / 2) ≤ n := Nat.mul_div_le n 2
  have h3 : n < 3 * (n / 3) + 3 := Nat.lt_mul_div_succ n (by norm_num)
  have h5 : n < 5 * (n / 5) + 5 := Nat.lt_mul_div_succ n (by norm_num)
  have h7 : n < 7 * (n / 7) + 7 := Nat.lt_mul_div_succ n (by norm_num)
  have h11 : n < 11 * (n / 11) + 11 := Nat.lt_mul_div_succ n (by norm_num)
  have h13 : n < 13 * (n / 13) + 13 := Nat.lt_mul_div_succ n (by norm_num)
  have h17 : n < 17 * (n / 17) + 17 := Nat.lt_mul_div_succ n (by norm_num)
  have h19 : n < 19 * (n / 19) + 19 := Nat.lt_mul_div_succ n (by norm_num)
  have h23 : n < 23 * (n / 23) + 23 := Nat.lt_mul_div_succ n (by norm_num)
  have h29 : n < 29 * (n / 29) + 29 := Nat.lt_mul_div_succ n (by norm_num)
  have h31 : n < 31 * (n / 31) + 31 := Nat.lt_mul_div_succ n (by norm_num)
  have h37 : n < 37 * (n / 37) + 37 := Nat.lt_mul_div_succ n (by norm_num)
  have h41 : n < 41 * (n / 41) + 41 := Nat.lt_mul_div_succ n (by norm_num)
  have h43 : n < 43 * (n / 43) + 43 := Nat.lt_mul_div_succ n (by norm_num)
  have h47 : n < 47 * (n / 47) + 47 := Nat.lt_mul_div_succ n (by norm_num)
  have h53 : n < 53 * (n / 53) + 53 := Nat.lt_mul_div_succ n (by norm_num)
  have h59 : n < 59 * (n / 59) + 59 := Nat.lt_mul_div_succ n (by norm_num)
  have h61 : n < 61 * (n / 61) + 61 := Nat.lt_mul_div_succ n (by norm_num)
  unfold wSum
  linarith

lemma small_ineq : ∀ n < 128, 1 ≤ n → ¬(n ≤ 34 ∨ n = 36 ∨ n = 38) →
    n / 2 + n / 4 + n / 8 + n / 16 + n / 32 + n / 64 + n / 2 < wSum n := by
  decide +kernel

lemma v2_fact_small (n : ℕ) (hn : n < 128) :
    padicValNat 2 n.factorial = n / 2 + n / 4 + n / 8 + n / 16 + n / 32 + n / 64 := by
  have hlog : Nat.log 2 n < 7 := by
    rcases Nat.eq_zero_or_pos n with rfl | h
    · rw [Nat.log_zero_right]; norm_num
    · exact Nat.log_lt_of_lt_pow (by omega) (by norm_num; omega)
  rw [padicValNat_factorial hlog]
  have hI : Finset.Ico 1 7 = {1, 2, 3, 4, 5, 6} := by decide
  rw [hI]
  repeat rw [Finset.sum_insert (by decide)]
  rw [Finset.sum_singleton]
  simp only [Nat.reducePow]
  ring

lemma small_dvd : ∀ n < 39, 1 ≤ n → (n ≤ 34 ∨ n = 36 ∨ n = 38) → phiProd n ∣ sqProd n := by
  unfold phiProd sqProd; decide +kernel

/-! ### The conjecture -/

/-- Wilson's conjecture (first part): `1/det(M)` is an integer exactly for
`n ∈ {1, …, 34} ∪ {36, 38}`.  The type is the upstream statement `OeisA60841.conjecture1`. -/
theorem conjecture1_proved : type_of% @OeisA60841.conjecture1 := by
  intro n hn
  rw [inv_det, den_eq_one_iff_dvd _ _ (phiProd_ne_zero n)]
  have hmem : n ∈ integerDetN ↔ (n ≤ 34 ∨ n = 36 ∨ n = 38) := by
    simp only [integerDetN, Set.mem_union, Set.mem_Icc, Set.mem_insert_iff,
      Set.mem_singleton_iff]
    omega
  rw [hmem]
  constructor
  · intro hdvd
    by_contra hnot
    have h1 := key_bound oddPrimes wt oddPrimes_spec n
    rw [wSum_eq] at h1
    have hsq : sqProd n ≠ 0 := by rw [sqProd_eq]; exact pow_ne_zero 2 (Nat.factorial_ne_zero n)
    have h2 : padicValNat 2 (phiProd n) ≤ 2 * padicValNat 2 n.factorial := by
      have h := (padicValNat_dvd_iff_le (p := 2) hsq).mp (dvd_trans pow_padicValNat_dvd hdvd)
      rwa [sqProd_eq, padicValNat.pow] at h
    rcases Nat.lt_or_ge n 128 with hlt | hge
    · have h3 := v2_fact_small n hlt
      have h4 := small_ineq n hlt hn hnot
      omega
    · have h3 : padicValNat 2 n.factorial < n :=
        padicValNat_factorial_lt_of_ne_zero 2 (by omega)
      have h4 := large_ineq n hge
      omega
  · intro h
    exact small_dvd n (by omega) hn h

end OeisA60841

/-- The theorem the Cairn Commons Lean check inspects: the upstream statement
`OeisA60841.conjecture1` of Formal Conjectures. -/
theorem main : type_of% @OeisA60841.conjecture1 := OeisA60841.conjecture1_proved