n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
⊢ MinSqFacProp n
    (if h : n < k * k then none
    else
      let_fun this := (_ : sqrt n - k < sqrt n + 2 - k);
      if k ∣ n then
        let n' := n / k;
        let_fun this := (_ : sqrt n' - k < sqrt n + 2 - k);
        if k ∣ n' then some k else minSqFacAux n' (k + 2)
      else minSqFacAux n (k + 2))
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
⊢ MinSqFacProp n (minSqFacAux n k)
rw [minSqFacAux]
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
⊢ MinSqFacProp n none

case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
⊢ MinSqFacProp n
    (if h : n < k * k then none
    else
      let_fun this := (_ : sqrt n - k < sqrt n + 2 - k);
      if k ∣ n then
        let n' := n / k;
        let_fun this := (_ : sqrt n' - k < sqrt n + 2 - k);
        if k ∣ n' then some k else minSqFacAux n' (k + 2)
      else minSqFacAux n (k + 2))
by_cases h : n < k * k <;> simp [h]
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
have k2 : 2 ≤ k := by
  subst e
  linarith
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
have k0 : 0 < k := lt_of_lt_of_le (by decide) k2
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
pk : k ∣ n → Prime k
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
have pk : k ∣ n → Prime k := by
  refine' fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) _⟩
  exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk)
case neg.inl.inl
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : k ∣ n / k
⊢ MinSqFacProp n (some k)

case neg.inl.inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : ¬k ∣ n / k
⊢ MinSqFacProp n (minSqFacAux (n / k) (k + 2))

case neg.inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
pk : k ∣ n → Prime k
dk : ¬k ∣ n
⊢ MinSqFacProp n (minSqFacAux n (k + 2))
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
pk : k ∣ n → Prime k
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
split_ifs with dk dkk
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
⊢ False
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
⊢ MinSqFacProp n none
refine' squarefree_iff_prime_squarefree.2 fun p pp d => _
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
this : k ≤ p
⊢ False
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
⊢ False
have := ih p pp (dvd_trans ⟨_, rfl⟩ d)
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
this✝ : k ≤ p
this : k * k ≤ p * p
⊢ False
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
this : k ≤ p
⊢ False
have := Nat.mul_le_mul this this
no goals
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
this✝ : k ≤ p
this : k * k ≤ p * p
⊢ False
exact not_le_of_lt h (le_trans this (le_of_dvd n0 d))
n : ℕ
n0 : 0 < n
i : ℕ
ih : ∀ (m : ℕ), Prime m → m ∣ n → 2 * i + 3 ≤ m
h : ¬n < (2 * i + 3) * (2 * i + 3)
⊢ 2 ≤ 2 * i + 3
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ 2 ≤ k
subst e
no goals
n : ℕ
n0 : 0 < n
i : ℕ
ih : ∀ (m : ℕ), Prime m → m ∣ n → 2 * i + 3 ≤ m
h : ¬n < (2 * i + 3) * (2 * i + 3)
⊢ 2 ≤ 2 * i + 3
linarith
no goals
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
⊢ 0 < 2
decide
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
⊢ MinSqFacProp n' (minSqFacAux n' (k + 2))
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
⊢ ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
intro n' nd' nk
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
⊢ MinSqFacProp n' (minSqFacAux n' (k + 2))
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
⊢ MinSqFacProp n' (minSqFacAux n' (k + 2))
have hn' := le_of_dvd n0 nd'
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
⊢ k + 2 ≤ m
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
⊢ MinSqFacProp n' (minSqFacAux n' (k + 2))
refine'
  have : Nat.sqrt n' - k < Nat.sqrt n + 2 - k :=
    lt_of_le_of_lt (Nat.sub_le_sub_right (Nat.sqrt_le_sqrt hn') _) (Nat.minFac_lemma n k h)
  @minSqFacAux_has_prop n' (k + 2) (pos_of_dvd_of_pos nd' n0) (i + 1)
    (by simp [e, left_distrib]) fun m m2 d => _
case inl
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
me : k = m
⊢ k + 2 ≤ m

case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
⊢ k + 2 ≤ m
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
⊢ k + 2 ≤ m
cases' Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with me ml
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
⊢ ¬succ k = m
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
⊢ k + 2 ≤ m
apply (Nat.eq_or_lt_of_le ml).resolve_left
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
me : succ k = m
⊢ False
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
⊢ ¬succ k = m
intro me
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : succ (2 * i + 3) ∣ n'
ml : k < m
me : succ k = m
⊢ False
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
me : succ k = m
⊢ False
rw [← me, e] at d
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : succ k = m
d : 2 * (i + 2) ∣ n'
⊢ False
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : succ (2 * i + 3) ∣ n'
ml : k < m
me : succ k = m
⊢ False
change 2 * (i + 2) ∣ n' at d
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : succ k = m
d : 2 * (i + 2) ∣ n'
this : k ≤ 2
⊢ False
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : succ k = m
d : 2 * (i + 2) ∣ n'
⊢ False
have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd')
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : succ k = m
d : 2 * (i + 2) ∣ n'
this : 2 * i + 3 ≤ 2
⊢ False
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : succ k = m
d : 2 * (i + 2) ∣ n'
this : k ≤ 2
⊢ False
rw [e] at this
no goals
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : succ k = m
d : 2 * (i + 2) ∣ n'
this : 2 * i + 3 ≤ 2
⊢ False
exact absurd this (by linarith)
no goals
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
⊢ k + 2 = 2 * (i + 1) + 3
simp [e, left_distrib]
case inl
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m2 : Prime k
d : k ∣ n'
⊢ k + 2 ≤ k
case inl
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
me : k = m
⊢ k + 2 ≤ m
subst me
no goals
case inl
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m2 : Prime k
d : k ∣ n'
⊢ k + 2 ≤ k
contradiction
no goals
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : succ k = m
d : 2 * (i + 2) ∣ n'
this : 2 * i + 3 ≤ 2
⊢ ¬2 * i + 3 ≤ 2
linarith
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
dk : k ∣ n
⊢ k ≤ minFac k
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
⊢ k ∣ n → Prime k
refine' fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) _⟩
no goals
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
dk : k ∣ n
⊢ k ≤ minFac k
exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk)
no goals
case neg.inl.inl
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : k ∣ n / k
⊢ MinSqFacProp n (some k)
exact ⟨pk dk, (Nat.dvd_div_iff dk).1 dkk, fun p pp d => ih p pp (dvd_trans ⟨_, rfl⟩ d)⟩
case neg.inl.inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : ¬k ∣ n / k
IH : MinSqFacProp (n / k) (minSqFacAux (n / k) (k + 2))
⊢ MinSqFacProp n (minSqFacAux (n / k) (k + 2))
case neg.inl.inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : ¬k ∣ n / k
⊢ MinSqFacProp n (minSqFacAux (n / k) (k + 2))
specialize IH (n / k) (div_dvd_of_dvd dk) dkk
no goals
case neg.inl.inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : ¬k ∣ n / k
IH : MinSqFacProp (n / k) (minSqFacAux (n / k) (k + 2))
⊢ MinSqFacProp n (minSqFacAux (n / k) (k + 2))
exact minSqFacProp_div _ (pk dk) dk (mt (Nat.dvd_div_iff dk).2 dkk) IH
no goals
case neg.inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
pk : k ∣ n → Prime k
dk : ¬k ∣ n
⊢ MinSqFacProp n (minSqFacAux n (k + 2))
exact IH n (dvd_refl _) dk