verification.lean

--- This is adapted solution to 3rd exercise from Project Euler
--- from https://codereview.stackexchange.com/questions/74587/project-euler-3-in-java/74792#74792
--- by Altinak

import Mathlib

lemma div_at_least_one {n f: ℕ} (Hn: 1 ≤ n) (Hf: 2 ≤ f) (H: f ∣ n): 1 ≤ n / f := by
  cases H with | intro w h =>
  rw [h, Nat.mul_div_cancel_left] <;> nlinarith

def repeatedDiv {n f: ℕ} (highest: ℕ) (Hn: 1 ≤ n) (Hf: 2 ≤ f): ℕ × ℕ :=
  if h: (f ∣ n)
  then @repeatedDiv (n / f) f (max f highest) (div_at_least_one Hn Hf h) Hf
  else (n, highest)
termination_by n
decreasing_by exact Nat.div_lt_self Hn Hf

lemma repeatedDiv_ge_one {n f: ℕ} (highest: ℕ) (Hn: 1 ≤ n) (Hf: 2 ≤ f):
    1 ≤ (repeatedDiv highest Hn Hf).1 := by
  revert highest
  induction n using Nat.strong_induction_on with | h n iH =>
  intro highest
  rw [repeatedDiv]
  split <;> rename_i h
  . have H: n / f < n := Nat.div_lt_self Hn Hf
    exact (iH _ H (div_at_least_one Hn Hf h) (max f highest))
  . simp; exact Hn

lemma repeatedDiv_le_n {n f: ℕ} (highest: ℕ) (Hn: 1 ≤ n) (Hf: 2 ≤ f):
    (repeatedDiv highest Hn Hf).1 ≤ n := by
  revert highest
  induction n using Nat.strong_induction_on with | h n iH =>
  intro highest
  rw [repeatedDiv]
  split <;> rename_i h
  . have H1: n / f < n := by
      apply Nat.div_lt_self <;> lia
    have H2 := iH _ H1 (div_at_least_one Hn Hf h) (max f highest)
    lia
  . simp

def find {n f: ℕ} (highest: ℕ) (Hn: 1 ≤ n) (Hf: 2 ≤ f): ℕ × ℕ :=
  if h: (f * f ≤ n)
  then let temp1 := repeatedDiv highest Hn Hf
       let temp2 := @repeatedDiv temp1.1 (f + 2) temp1.2 (by unfold temp1; apply repeatedDiv_ge_one) (by lia)
       @find temp2.1 (f + 6) temp2.2 (by unfold temp2; apply repeatedDiv_ge_one) (by lia)
  else (n, highest)
termination_by Nat.sqrt n + 6 - f
decreasing_by
  simp
  rw [<- Nat.le_sqrt] at h
  nth_rw 1 [repeatedDiv]; split <;> rename_i h1
  . have H := @repeatedDiv_le_n
                ((repeatedDiv highest Hn Hf).1 / (f + 2))
                (f + 2)
                (max (f + 2) (repeatedDiv highest Hn Hf).2)
                (div_at_least_one (repeatedDiv_ge_one highest Hn Hf) (by lia) h1)
    simp at *
    have H1 := repeatedDiv_le_n highest Hn Hf
    have H2 := repeatedDiv_ge_one highest Hn Hf
    have H3 := Nat.div_lt_self (k := f + 2) (n := (repeatedDiv highest Hn Hf).1) (by lia) (by lia)
    apply LT.lt.le at H3
    have H4 := (H.trans H3).trans H1
    apply Nat.sqrt_le_sqrt at H4
    lia
  . simp
    have H := repeatedDiv_le_n highest Hn Hf
    apply Nat.sqrt_le_sqrt at H
    lia

def biggestDivisor (n: ℕ) (Hn: 1 ≤ n): ℕ :=
  let temp1 := @repeatedDiv n 2 1 Hn (by simp)
  let temp2 := @repeatedDiv temp1.1 3 temp1.2 (by unfold temp1; apply repeatedDiv_ge_one) (by simp)
  let (n3, highest3) := @find temp2.1 5 temp2.2 (by unfold temp2; apply repeatedDiv_ge_one) (by simp)
  if (n3 == 1) then highest3 else n3

def number: ℕ := 600851475143

#eval biggestDivisor number (by unfold number; simp)

-------------------------

def rep_div (n f: ℕ): ℕ × ℕ :=
  if (1 ≤ n ∧ 2 ≤ f ∧ f ∣ n)
  then let (i, k) := rep_div (n / f) f
       (i + 1, k)
  else (0, n)
termination_by n
decreasing_by apply Nat.div_lt_self <;> lia

def rep_rep_div (n i: ℕ): ℕ :=
  if (1 ≤ n)
  then if (2 ≤ i)
       then (rep_div (rep_rep_div n (i - 1)) i).2
       else n
  else 1

-------------------------

theorem rep_div_main_thm {n f: ℕ} (Hn: 1 ≤ n) (Hf: 2 ≤ f):
    n = f ^ (rep_div n f).1 * (rep_div n f).2 := by
  induction n using Nat.strong_induction_on with | h n iH =>
  rw [rep_div]
  split <;> rename_i h <;> simp
  obtain ⟨h1, h2, h3⟩ := h
  cases h3 with | intro w h =>
  rw [h, Nat.mul_div_cancel_left, Nat.pow_add_one, mul_comm _ f, mul_assoc] <;> try lia
  congr 1; apply iH <;> nlinarith

theorem one_le_rep_div {n} (Hn: 1 ≤ n) f: 1 ≤ (rep_div n f).2 := by
  by_cases H: (2 ≤ f)
  . induction n using Nat.strong_induction_on with | h n iH =>
    rw [rep_div]; simp [Hn, H]
    split <;> rename_i H1 <;> simp <;> try assumption
    exact iH _ (Nat.div_lt_self Hn H) (div_at_least_one Hn H H1)
  . rw [rep_div]; simp [Hn, H]

theorem rep_div_le_n {n} (Hn: 1 ≤ n) f: (rep_div n f).2 ≤ n := by
  by_cases H: (2 ≤ f)
  . induction n using Nat.strong_induction_on with | h n iH =>
    rw [rep_div]; simp [Hn, H]
    split <;> rename_i H1 <;> simp
    have H2 := Nat.div_lt_self Hn H
    have H3 := iH _ H2 (div_at_least_one Hn H H1)
    lia
  . rw [rep_div]; simp [Hn, H]

theorem no_div_after_rep_div {n f} (Hn: 1 ≤ n) (Hf: 2 ≤ f): ¬ (f ∣ (rep_div n f).2) := by
  induction n using Nat.strong_induction_on with | h n iH =>
  intro H; cases H with | intro w h =>
  rw [rep_div] at h; simp at *
  split_ifs at h <;> rename_i H <;> simp at *
  . apply (iH _ (Nat.div_lt_self Hn Hf) (div_at_least_one Hn Hf H.2.2))
    exists w
  . apply (H Hn Hf)
    exists w

theorem rep_div_snd_dvd_n {n f} (Hn: 1 ≤ n) (Hf: 2 ≤ f): (rep_div n f).2 ∣ n := by
  exists (f ^ (rep_div n f).1)
  rw [mul_comm]
  exact rep_div_main_thm Hn Hf

theorem rep_div_if_n_not_div_eq_n {n f} (Hf: ¬ f ∣ n): (rep_div n f).2 = n := by
  rw [rep_div]; simp [Hf]


theorem rep_div_fact_thm1 {n f} (Hn: 1 ≤ n) (Hf: f.Prime):
    (rep_div n f).2.factorization f = 0 :=
  Nat.factorization_eq_zero_of_not_dvd (no_div_after_rep_div Hn (Nat.Prime.two_le Hf))

theorem rep_div_fact_thm2 {n f a} (Hn: 1 ≤ n) (Hf: f.Prime) (Ha: f ≠ a):
    (rep_div n f).2.factorization a = n.factorization a := by
  by_cases H1:(a.Prime)
  . have H2: 2 ≤ f := by exact Nat.Prime.two_le Hf
    nth_rw 2 [rep_div_main_thm Hn H2]
    rw [Nat.factorization_mul]
    . simp
      right
      rw [Nat.Prime.factorization Hf]
      exact Finsupp.single_eq_of_ne Ha.symm
    . exact pow_ne_zero (rep_div n f).1 (Nat.ne_zero_of_lt H2)
    . exact Nat.ne_zero_of_lt (one_le_rep_div Hn f)
  . rw [Nat.factorization_eq_zero_of_not_prime (rep_div n f).2 H1]
    rw [Nat.factorization_eq_zero_of_not_prime n H1]

theorem rep_div_fact_thm3 {n f} (Hn: 1 ≤ n) (Hf: f.Prime):
    (rep_div n f).1 = n.factorization f := by
  have H1 := Nat.Prime.two_le Hf
  nth_rw 2 [rep_div_main_thm Hn H1]
  rw [Nat.factorization_mul_apply_of_coprime]
  . simp
    rw [Nat.Prime.factorization_self Hf, rep_div_fact_thm1 Hn Hf]
    simp
  . refine Nat.Coprime.pow_left (rep_div n f).1 ?_
    exact (Nat.Prime.coprime_iff_not_dvd Hf).mpr (no_div_after_rep_div Hn H1)


theorem one_le_rep_rep_div {n} (Hn: 1 ≤ n) i: 1 ≤ rep_rep_div n i := by
  have H:(¬ 2 ≤ i ∨ 2 ≤ i) := by lia
  obtain H | H := H
  . rw [rep_rep_div]
    simp [Hn, H]
  . induction i using Nat.strong_induction_on with | h i iH =>
    rw [rep_rep_div]
    simp [Hn, H]
    have H0:(i = 2 ∨ 2 ≤ i - 1) := by lia
    obtain H0 | H0 := H0
    . subst H0; simp
      rw [rep_rep_div]
      simp [Hn]
      exact one_le_rep_div Hn 2
    . have H1 := iH (i - 1) (by simp; lia) H0
      exact one_le_rep_div H1 i

theorem no_div_after_rep_rep_div {n i} (Hn: 1 ≤ n) (Hi: 2 ≤ i):
    i ∣ rep_rep_div n i → False := by
  intros H
  rw [rep_rep_div] at H
  simp [Hn, Hi] at H
  exact (no_div_after_rep_div (one_le_rep_rep_div Hn (i - 1)) Hi H)

theorem no_div_after_rep_rep_div'_aux {n i} (Hn: 1 ≤ n) (Hi: 2 ≤ i) w:
    i ∣ rep_rep_div n (i + w) → False := by
  revert n Hn
  induction w with
  | zero => exact fun {n} Hn ↦ no_div_after_rep_rep_div Hn Hi
  | succ w iH =>
    intros n Hn H
    rw [rep_rep_div] at H
    have H1: 2 ≤ i + (w + 1) := Nat.le_add_right_of_le Hi
    simp [Hn, H1] at H
    have H2 := one_le_rep_rep_div Hn (i + w)
    have H3 := rep_div_snd_dvd_n H2 H1
    exact iH Hn (Nat.dvd_trans H H3)

theorem no_div_after_rep_rep_div' {n x i} (Hn: 1 ≤ n) (Hx: 2 ≤ x) (Hi: x ≤ i):
    x ∣ rep_rep_div n i → False := by
  rw [<- @Nat.add_sub_of_le x i Hi]
  exact no_div_after_rep_rep_div'_aux Hn Hx (i - x)

theorem rep_rep_div_by_one {n} (Hn: 1 ≤ n):
    rep_rep_div n 1 = n := by
  rw [rep_rep_div]; simp [Hn]

theorem div_after_rep_rep_div_div_before {n i} (Hn: 1 ≤ n) (Hi: 1 ≤ i) x:
    x ∣ rep_rep_div n i → x ∣ n := by
  induction i with
  | zero => lia
  | succ i iH =>
    have H: i = 0 ∨ 1 ≤ i := by lia
    obtain H | H := H
    . subst H
      rw [rep_rep_div_by_one Hn]
      simp
    . rw [rep_rep_div]
      simp [Hn, H]
      intro H1
      apply iH H
      have H2 := one_le_rep_rep_div Hn i
      have H3 := rep_div_main_thm (f := i + 1) H2 (Nat.le_add_of_sub_le H)
      rw [H3]
      exact Dvd.dvd.mul_left H1 ?_

theorem rep_rep_div_main_thm_aux1 {n i} (Hn: 1 ≤ n) (Hi: 1 ≤ i):
    (i + 1 ∣ rep_rep_div n i) → (i + 1).Prime ∧ (i + 1) ∣ n := by
  intros H
  constructor
  . by_contra H1
    have H2 := @Nat.minFac_prime (i + 1) (by lia)
    rw [Nat.not_prime_iff_minFac_lt] at H1 <;> try lia
    have H3 := Nat.minFac_dvd (i + 1)
    have H4 := Nat.dvd_trans H3 H
    exact no_div_after_rep_rep_div' Hn (Nat.Prime.two_le H2) (Nat.le_of_lt_succ H1) H4
  . exact div_after_rep_rep_div_div_before Hn Hi (i + 1) H

theorem rep_rep_div_main_thm_aux2 {n i W} (Hn: 1 ≤ n) (Hi: 1 ≤ i) (Hw: i < W):
    Nat.Prime W → W ∣ n → W ∣ rep_rep_div n i := by
  intros H1 H2
  have H3: 2 ≤ W := Nat.Prime.two_le H1
  have H4 := @Nat.coprime_of_lt_prime
  induction i with
  | zero => linarith
  | succ i iH =>
    rw [rep_rep_div]
    simp [Hn]
    split <;> rename_i H5
    . have H6 := iH H5 (Nat.lt_of_succ_lt Hw)
      have H7: W ∣ (i + 1) ^ (rep_div (rep_rep_div n i) (i + 1)).1 *
                  (rep_div (rep_rep_div n i) (i + 1)).2 := by
        rw [<- rep_div_main_thm (one_le_rep_rep_div Hn i) (Nat.le_add_of_sub_le H5)]
        exact H6
      apply Nat.Coprime.dvd_of_dvd_mul_left (m := (i + 1) ^ (rep_div (rep_rep_div n i) (i + 1)).1)
      . exact Nat.Coprime.pow_right (rep_div (rep_rep_div n i) (i + 1)).1 (H4 (by linarith) Hw H1)
      . exact H7
    . exact H2

theorem rep_rep_div_main_thm {n i} (Hn: 1 ≤ n) (Hi: 1 ≤ i):
    (i + 1 ∣ rep_rep_div n i) ↔ Nat.Prime (i + 1) ∧ (i + 1 ∣ n) := by
  constructor <;> intro H
  . exact rep_rep_div_main_thm_aux1 Hn Hi H
  . exact rep_rep_div_main_thm_aux2 Hn Hi (lt_add_one i) H.1 H.2


theorem rep_rep_div_nonprime_not_div {n i} (Hn: 1 ≤ n) (Hi:2 ≤ i):
    (¬ i.Prime) → (¬ i ∣ rep_rep_div n (i - 1)) := by
  intro H H1; apply H
  have H2: i = (i - 1) + 1 := by lia
  rw [H2]; nth_rw 1 [H2] at H1
  rw [rep_rep_div_main_thm Hn (Nat.le_sub_one_of_lt Hi)] at H1
  tauto

theorem rep_rep_div_by_nonprime_decr {n i} (Hn: 1 ≤ n) (Hi: 2 ≤ i):
    (¬ i.Prime) → rep_rep_div n i = rep_rep_div n (i - 1) := by
  intros H
  apply rep_rep_div_nonprime_not_div Hn Hi at H
  nth_rw 1 [rep_rep_div]
  simp [Hn, Hi]
  exact rep_div_if_n_not_div_eq_n H

-------------------------

#check Nat.factorization

/- def divisors_under_i (i n: ℕ) : ℕ →₀ ℕ := n.factorization.filter (λ x => x ≤ i)
def divisors_bigger_than_i (i n: ℕ): ℕ →₀ ℕ := n.factorization.filter (λ x => i < x) -/

theorem rep_div_as_filter {n i} (Hn: 1 ≤ n) (Hi: i.Prime):
    (rep_div n i).2.factorization = n.factorization.filter (λ x => x ≠ i) := by
  have H: 2 ≤ i := Nat.Prime.two_le Hi
  ext a
  simp
  rw [Finsupp.filter_apply]
  split <;> rename_i H1
  . nth_rw 2 [rep_div_main_thm Hn H]
    rw [Nat.factorization_mul]; simp
    . right
      rw [Nat.Prime.factorization Hi]
      rw [Finsupp.single_apply]
      split <;> lia
    . have H2: i ≠ 0 := by linarith
      exact pow_ne_zero (rep_div n i).1 H2
    . have H2: 1 ≤ (rep_div n i).2 := one_le_rep_div Hn i
      exact Nat.ne_zero_of_lt H2
  . simp at H1; subst H1
    exact rep_div_fact_thm1 Hn Hi


theorem rep_rep_div_as_filter {i n} (Hn: 1 ≤ n) (Hi: 2 ≤ i):
    (rep_rep_div n i).factorization = n.factorization.filter (λ x => i < x) := by
  induction i using Nat.strong_induction_on with | h i iH =>
  have H: i = 2 ∨ 2 ≤ i - 1 := by lia
  obtain H | H := H
  . subst H; clear iH Hi
    rw [rep_rep_div]
    simp [Hn]
    rw [rep_rep_div_by_one Hn]
    ext a
    by_cases H: a.Prime
    rw [Finsupp.filter_apply]
    . by_cases H1: 2 = a
      . subst H1; simp
        exact rep_div_fact_thm1 Hn H
      . have H2: 2 ≤ a := by exact Nat.Prime.two_le H
        have H3: 2 < a := by lia
        simp [H3]
        rw [rep_div_fact_thm2 Hn Nat.prime_two H1]
    . rw [Nat.factorization_eq_zero_of_not_prime (rep_div n 2).2 H]
      rw [Finsupp.filter_apply]
      rw [Nat.factorization_eq_zero_of_not_prime n H]
      simp
  . ext a
    rw [Finsupp.filter_apply]
    by_cases H1: a.Prime
    . by_cases H2: i < a
      . simp [H2]
        by_cases H3: i.Prime
        . rw [rep_rep_div]
          simp [Hn, Hi]
          rw [rep_div_as_filter (one_le_rep_rep_div Hn (i -1)) H3]
          rw [iH _ (Nat.sub_one_lt_of_lt Hi) H]
          rw [Finsupp.filter_apply, Finsupp.filter_apply]
          have H4: a ≠ i := Ne.symm (Nat.ne_of_lt H2)
          have H5: i - 1 < a := tsub_lt_of_lt H2
          simp [H4, H5]
        . rw [rep_rep_div_by_nonprime_decr Hn Hi H3]
          rw [iH _ (Nat.sub_one_lt_of_lt Hi) H]
          rw [Finsupp.filter_apply]
          have H4: i - 1 < a := tsub_lt_of_lt H2
          simp [H4]
      . simp [H2]
        by_cases H3: i.Prime
        . rw [rep_rep_div]
          simp [Hn, Hi]
          rw [rep_div_as_filter (one_le_rep_rep_div Hn (i - 1)) H3]
          rw [Finsupp.filter_apply]
          split <;> rename_i H4 <;> try simp
          rw [iH _ (Nat.sub_one_lt_of_lt Hi) H]
          rw [Finsupp.filter_apply]
          split <;> rename_i H5 <;> try simp
          lia
        . rw [rep_rep_div_by_nonprime_decr Hn Hi H3]
          rw [iH _ (Nat.sub_one_lt_of_lt Hi) H]
          rw [Finsupp.filter_apply]
          have H5: a = i ∨ ¬ (i - 1 < a) := by lia
          obtain H5 | H5 := H5
          . subst H5; tauto
          . simp [H5]
    . rw [Nat.factorization_eq_zero_of_not_prime (rep_rep_div n i) H1]
      rw [Nat.factorization_eq_zero_of_not_prime n H1]
      simp

def max_divisor_le_i (n i: ℕ): ℕ :=
  match (n.factorization.filter (λ x => x ≤ i)).support.max with
  | some a => a
  | _ => 1


theorem step_0 {n} (Hn: 1 ≤ n):
    @repeatedDiv n 2 2 Hn (by simp) = ⟨rep_rep_div n 2, 2⟩ := by
  induction n using Nat.strong_induction_on with | h n iH =>
  have H: n = 1 ∨ 2 ≤ n := by lia
  obtain H | H := H
  . subst n
    rw [repeatedDiv]; simp
    rw [rep_rep_div]; simp
    rw [rep_rep_div_by_one Hn]
    rw [rep_div]; simp
  . rw [repeatedDiv]; simp
    rw [rep_rep_div]; simp [Hn]
    rw [rep_rep_div_by_one Hn, rep_div]; simp [Hn]
    split; rename_i H2
    . rw [iH _ (by lia)]; simp
      rw [rep_rep_div]; simp
      have H3: 1 ≤ n / 2 := div_at_least_one Hn (by simp) H2
      simp [H3]
      rw [rep_rep_div_by_one H3]
    . simp

theorem step_1 {n} (Hn: 1 ≤ n):
    @repeatedDiv n 2 1 Hn (by simp) = ⟨rep_rep_div n 2, max_divisor_le_i n 2⟩ := by
  induction n using Nat.strong_induction_on with | h n iH =>
  have H: n = 1 ∨ 2 ≤ n := by lia
  obtain H | H := H
  . subst n
    rw [repeatedDiv]; simp
    rw [rep_rep_div, rep_rep_div_by_one Hn]; simp
    rw [rep_div]; simp
    rw [max_divisor_le_i]; simp
  . rw [repeatedDiv]; simp
    rw [rep_rep_div]; simp [Hn]
    rw [rep_rep_div_by_one Hn]
    rw [rep_div]; simp [Hn]
    split <;> rename_i H1
    . simp
      rw [step_0]
      have H2: 1 ≤ n / 2 := div_at_least_one Hn (by simp) H1
      rw [rep_rep_div]; simp [H2]
      rw [rep_rep_div_by_one H2]; simp
      rw [max_divisor_le_i]
      have H3: 1 ≤ Finsupp.filter (λ x => x ≤ 2) n.factorization 2 := by
        rw [Finsupp.filter_apply]; simp
        apply Nat.Prime.factorization_pos_of_dvd Nat.prime_two (by lia) H1
      simp at H3
      have H4: (n.factorization.filter (λ x => x ≤ 2)).support.max = some 2 := by
        have H5: (n.factorization.filter (λ x => x ≤ 2)).support = {2} := by
          refine Finsupp.support_eq_singleton.mpr ?_
          constructor
          . simp; lia
          . simp; ext a
            rw [Finsupp.filter_apply]
            split <;> rename_i H6
            . interval_cases a <;> try simp
            . rw [MonoidAlgebra.single_apply]
              have H7: 2 ≠ a := by lia
              simp [H7]
        rw [H5]; simp; rfl
      have H5: Finsupp.filter (λ x => x ≤ 2) n.factorization ≠ 0 := by
        intro H5
        rw [@Finsupp.filter_eq_zero_iff] at H5
        have H6 := H5 2 (by simp)
        lia
      rw [H4]
    . simp
      rw [max_divisor_le_i]
      have H2: Finsupp.filter (λ x => x ≤ 2) n.factorization = 0 := by
        ext a
        rw [Finsupp.filter_apply]
        simp; intro H2
        interval_cases a <;> try simp
        exact Nat.factorization_eq_zero_of_not_dvd H1
      rw [H2]; simp

def max_of_filtered_by_le_is_le (X: Finset ℕ) f:
    (X.filter (λ x => x ≤ f)).max ≤ ↑f := by
  unfold Finset.max; simp
  intros b Hb H
  exact (WithBot.coe_le rfl).mpr H

def max_divisor_le_i_aux {n f} (Hf: 2 ≤ f): max_divisor_le_i n f ≤ f := by
  unfold max_divisor_le_i; simp
  have H := max_of_filtered_by_le_is_le (n.primeFactors) f
  rw [@Finset.max_le_iff] at H
  split
  . rename_i x a heq
    have H1: a ∈ Finset.filter (λ x => x ≤ f) n.primeFactors := Finset.mem_of_max heq
    apply H at H1
    exact WithBot.coe_le_coe.mp H1
  . lia

def rep_rep_div_of_one {f} (Hf: 2 ≤ f): rep_rep_div 1 f = 1 := by
  induction f with
  | zero => lia
  | succ f iH =>
    have H: f = 1 ∨ 2 ≤ f := by lia
    obtain H | H := H
    . subst f; simp at *
      rw [rep_rep_div]; simp
      rw [rep_rep_div_by_one Nat.le.refl]
      rw [rep_div]; simp
    . rw [rep_rep_div]; simp [Hf]
      rw [rep_div, iH H]; simp [Hf]
      have H1: f ≠ 0 := by lia
      simp [H1]

def step_2 {n} (Hn: 1 ≤ n):
    @repeatedDiv (rep_rep_div n 2) 3 (max_divisor_le_i n 2) (one_le_rep_rep_div Hn 2) (by simp) =
    ⟨rep_rep_div n 3, max_divisor_le_i n 3⟩ := by
  induction n using Nat.strong_induction_on with | h n iH =>
  have H: n = 1 ∨ 2 ≤ n := by lia
  obtain H | H := H
  . subst n; simp at *
    rw [@rep_rep_div_of_one 3 (by simp)]
    rw [repeatedDiv]
    split <;> rename_i H1
    . rw [rep_rep_div_of_one (by simp)] at H1; simp at H1
    . rw [rep_rep_div_of_one (by simp)]
      ext <;> simp
      unfold max_divisor_le_i
      simp
  . rw [repeatedDiv]
    split <;> rename_i H1
    . have H2: max_divisor_le_i n 2 ≤ 2 := @max_divisor_le_i_aux n 2 (by simp)
      have H3: 3 ⊔ max_divisor_le_i n 2 = 3 := by
        apply Nat.max_eq_left
        lia
      simp [H3]
      
      sorry
    . simp
      refine ⟨?_, ?_⟩
      . nth_rw 2 [rep_rep_div]
        simp [Hn]
        rw [rep_div_if_n_not_div_eq_n H1]
      . simp [max_divisor_le_i]
        split
        . rename_i x a heq
          split
          . rename_i x' a' heq'

            sorry
          . sorry
        . sorry

-------------------------

theorem main_result (n : ℕ) (Hn : 2 ≤ n):
    IsGreatest {d | Nat.Prime d ∧ d ∣ n} (biggestDivisor n (by lia)) := by
  unfold IsGreatest upperBounds; simp
  refine ⟨⟨?_, ?_⟩, ?_⟩
  . sorry
  . sorry
  . sorry