-- Mathlib/Data/Nat/Prime/Defs.lean
theorem minFacAux_has_prop {n : ℕ} (n2 : 2 ≤ n) :
    ∀ k i, k = 2 * i + 3 → (∀ m, 2 ≤ m → m ∣ n → k ≤ m) → minFacProp n (minFacAux n k)
  | k => fun i e a => by
    rw [minFacAux]
    by_cases h : n < k * k
    · 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)⟩
      simpa only [k, h] using
        ⟨n2, dvd_rfl, fun m m2 d => le_of_eq ((dvd_prime_two_le pp m2).1 d).symm⟩
    have k2 : 2 ≤ k

Proof state:
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ Nat.minFacProp n (n.minFacAux x✝)

Tactic:
rw [minFacAux]

Result:
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 n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Proof state:
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 (n.minFacAux (x✝ + 2))

Tactic:
refine
  have := minFac_lemma n k h
  minFacAux_has_prop n2 (k + 2) (i + 1) (by simp [k, e, Nat.left_distrib, add_right_comm])
    fun m m2 d => ?_

Result:
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 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ k + 2 ≤ m

Proof state:
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✝ : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x✝ < m
me : x✝.succ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ ¬2 * i + 3 ≤ 2

Tactic:
contradiction

Result:
no goals

Proof state:
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 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ k + 2 ≤ m

Tactic:
rcases Nat.eq_or_lt_of_le (a m m2 d) with me | ml

Result:
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 : n.sqrt - k < n.sqrt + 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 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ k + 2 ≤ m

Proof state:
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 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
me : x✝.succ = m
⊢ False

Tactic:
rw [← me, e] at d

Result:
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 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x✝ < m
me : x✝.succ = m
⊢ False

Proof state:
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 : n.sqrt - k < n.sqrt + 2 - k
m2 : 2 ≤ x✝
d : x✝ ∣ n
⊢ k + 2 ≤ x✝

Tactic:
contradiction

Result:
no goals

Proof state:
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 n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Tactic:
by_cases h : n < k * k

Result:
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 (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (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 n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Proof state:
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 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ k + 2 ≤ m

Tactic:
apply (Nat.eq_or_lt_of_le ml).resolve_left

Result:
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 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ ¬x✝.succ = m

Proof state:
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 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x✝ < m
me : x✝.succ = m
⊢ False

Tactic:
have d' : 2 * (i + 2) ∣ n := d

Result:
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 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x✝ < m
me : x✝.succ = m
d' : 2 * (i + 2) ∣ n
⊢ False

Proof state:
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

Tactic:
subst e

Result:
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

Proof state:
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✝

Tactic:
exact ⟨k2, dk, a⟩

Result:
no goals

Proof state:
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

Tactic:
apply Nat.le_add_left

Result:
no goals

Proof state:
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 : n.sqrt - k < n.sqrt + 2 - k
⊢ k + 2 = 2 * (i + 1) + 3

Tactic:
simp [k, e, Nat.left_distrib, add_right_comm]

Result:
no goals

Proof state:
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 (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Tactic:
simpa only [k, h] using
  ⟨n2, dvd_rfl, fun m m2 d => le_of_eq ((dvd_prime_two_le pp m2).1 d).symm⟩

Result:
no goals

Proof state:
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✝ : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x✝ < m
me : x✝.succ = m
d' : 2 * (i + 2) ∣ n
this : x✝ ≤ 2
⊢ False

Tactic:
rw [e] at this

Result:
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✝ : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x✝ < m
me : x✝.succ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ False

Proof state:
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 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ ¬x✝.succ = m

Tactic:
intro me

Result:
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 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
me : x✝.succ = m
⊢ False