n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ Nat.minFacProp n
    (if h : n < x✝ * x✝ then n
    else
      if x✝ ∣ n then x✝
      else
        let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝);
        minFacAux n (x✝ + 2))
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ Nat.minFacProp n (minFacAux n x✝)
rw [minFacAux]
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
⊢ Nat.minFacProp n n

case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
⊢ Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ Nat.minFacProp n
    (if h : n < x✝ * x✝ then n
    else
      if x✝ ∣ n then x✝
      else
        let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝);
        minFacAux n (x✝ + 2))
by_cases h : n < k * k <;> simp [h]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
⊢ Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
⊢ Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
have k2 : 2 ≤ k := by
  subst e
  apply Nat.le_add_left
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ Nat.minFacProp n x✝

case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ Nat.minFacProp n (minFacAux n (x✝ + 2))
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
⊢ Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
by_cases dk : k ∣ n <;> simp [dk]
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
pp : Prime n
⊢ Nat.minFacProp n n
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
⊢ Nat.minFacProp n n
have pp : Prime n :=
  prime_def_le_sqrt.2
    ⟨n2, fun m m2 l d => not_lt_of_ge l <| lt_of_lt_of_le (sqrt_lt.2 h) (a m m2 d)⟩
no goals
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
pp : Prime n
⊢ Nat.minFacProp n n
exact ⟨n2, dvd_rfl, fun m m2 d => le_of_eq ((dvd_prime_two_le pp m2).1 d).symm⟩
n : ℕ
n2 : 2 ≤ n
i : ℕ
k : ℕ := 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → 2 * i + 3 ≤ m
h : ¬n < k * k
⊢ 2 ≤ k
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
⊢ 2 ≤ k
subst e
no goals
n : ℕ
n2 : 2 ≤ n
i : ℕ
k : ℕ := 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → 2 * i + 3 ≤ m
h : ¬n < k * k
⊢ 2 ≤ k
apply Nat.le_add_left
no goals
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ Nat.minFacProp n x✝
exact ⟨k2, dk, a⟩
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ k + 2 ≤ m
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ Nat.minFacProp n (minFacAux n (x✝ + 2))
refine'
  have := minFac_lemma n k h
  minFacAux_has_prop n2 (k + 2) (i + 1) (by simp [e, left_distrib]) fun m m2 d => _
case neg.inl
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
me : x✝ = m
⊢ k + 2 ≤ m

case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ k + 2 ≤ m
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ k + 2 ≤ m
cases' Nat.eq_or_lt_of_le (a m m2 d) with me ml
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ ¬succ x✝ = m
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ k + 2 ≤ m
apply (Nat.eq_or_lt_of_le ml).resolve_left
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
me : succ x✝ = m
⊢ False
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ ¬succ x✝ = m
intro me
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
⊢ False
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
me : succ x✝ = m
⊢ False
rw [← me, e] at d
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
⊢ False
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
⊢ False
have d' : 2 * (i + 2) ∣ n := d
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
this : x✝ ≤ 2
⊢ False
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
⊢ False
have := a _ le_rfl (dvd_of_mul_right_dvd d')
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ False
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
this : x✝ ≤ 2
⊢ False
rw [e] at this
no goals
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ False
exact absurd this (by contradiction)
no goals
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
⊢ k + 2 = 2 * (i + 1) + 3
simp [e, left_distrib]
case neg.inl
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m2 : 2 ≤ x✝
d : x✝ ∣ n
⊢ k + 2 ≤ x✝
case neg.inl
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
me : x✝ = m
⊢ k + 2 ≤ m
subst me
no goals
case neg.inl
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m2 : 2 ≤ x✝
d : x✝ ∣ n
⊢ k + 2 ≤ x✝
contradiction
no goals
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ ¬2 * i + 3 ≤ 2
contradiction